B_ρ is a Banach algebra over K = ℝ or ℂ

The series of finite majorant norm ‖f‖_ρ = ∑_ν ‖a_ν‖ ρ^ν, for a radius vector ρ : Radius m with positive entries, form a normed algebra over K under the norm ‖f‖ = (‖f‖_ρ).toReal (subadditive, homogeneous and submultiplicative by the inequalities of ConvNorm.lean; definite because every ρ^ν is positive), and it is complete: the weighted coefficient family ν ↦ a_ν ρ^ν is a K-linear isometry onto the sequence space ℓ¹(Fin m →₀ ℕ; K) (lp (fun _ => K) 1), which Mathlib knows to be complete. The real weights ρ^ν enter K through RCLike.ofReal. These are the Banach algebras of [GR71, Kapitel I]; the Weierstrass division theorem needs their completeness (the contraction T q = Q f + Q (h q) on B_ρ in Hironaka/Analytic/Weierstrass/Contraction.lean), and the evaluation of series (Eval.lean) uses their norm.

theorem Analytic.BanachSeries.convNorm_ne_top {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} (f : ↥(BanachSeries K ρ)) : ConvNorm ↑ρ ↑f ≠ ⊤

theorem Analytic.eq_zero_of_convNorm_eq_zero {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} {f : MvPowerSeries (Fin m) K} (h : ConvNorm (↑ρ) f = 0) : f = 0

A series of zero ρ-norm is zero (every ρ^ν is positive).

@[instance_reducible]

noncomputable instance Analytic.instNormedAddCommGroupSubtypeMvPowerSeriesFinMemSubalgebraBanachSeries {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} : NormedAddCommGroup ↥(BanachSeries K ρ)

The norm of B ρ: the real value of the majorant norm.

Equations

• One or more equations did not get rendered due to their size.

theorem Analytic.BanachSeries.norm_def {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} (f : ↥(BanachSeries K ρ)) : ‖f‖ = (ConvNorm ↑ρ ↑f).toReal

@[instance_reducible]

noncomputable instance Analytic.instNormedRingSubtypeMvPowerSeriesFinMemSubalgebraBanachSeries {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} : NormedRing ↥(BanachSeries K ρ)

B_ρ is a normed ring, ‖f g‖ ≤ ‖f‖ ‖g‖.

Equations

• One or more equations did not get rendered due to their size.

instance Analytic.instNormOneClassSubtypeMvPowerSeriesFinMemSubalgebraBanachSeries {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} : NormOneClass ↥(BanachSeries K ρ)

@[instance_reducible]

noncomputable instance Analytic.instNormedAlgebraSubtypeMvPowerSeriesFinMemSubalgebraBanachSeries {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} : NormedAlgebra K ↥(BanachSeries K ρ)

Equations

• Analytic.instNormedAlgebraSubtypeMvPowerSeriesFinMemSubalgebraBanachSeries = { toAlgebra := (Analytic.BanachSeries K ρ).algebra, norm_smul_le := ⋯ }

Completeness through ℓ¹

theorem Analytic.convNorm_eq_tsum_coe {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} (f : MvPowerSeries (Fin m) K) : ConvNorm (↑ρ) f = ∑' (ν : Fin m →₀ ℕ), ↑(‖(MvPowerSeries.coeff ν) f‖₊ * monomialEval (↑ρ) ν)

The majorant norm as a sum of nonnegative reals coerced to ℝ≥0∞.

theorem Analytic.norm_coe_monomialEval {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Fin m → NNReal) (ν : Fin m →₀ ℕ) : ‖↑↑(monomialEval ρ ν)‖ = ↑(monomialEval ρ ν)

The real weight ρ^ν, coerced into K, has norm ρ^ν.

theorem Analytic.nnnorm_coe_monomialEval {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Fin m → NNReal) (ν : Fin m →₀ ℕ) : ‖↑↑(monomialEval ρ ν)‖₊ = monomialEval ρ ν

theorem Analytic.coe_monomialEval_ne_zero {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Radius m) (ν : Fin m →₀ ℕ) : ↑↑(monomialEval (↑ρ) ν) ≠ 0

theorem Analytic.BanachSeries.summable_weighted {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} (f : ↥(BanachSeries K ρ)) : Summable fun (ν : Fin m →₀ ℕ) => ‖(MvPowerSeries.coeff ν) ↑f * ↑↑(monomialEval (↑ρ) ν)‖

The weighted coefficient family ν ↦ a_ν ρ^ν of a series of finite norm is summable.

noncomputable def Analytic.BanachSeries.toLp {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} (f : ↥(BanachSeries K ρ)) : ↥(lp (fun (x : Fin m →₀ ℕ) => K) 1)

The weighted coefficient family, as an element of ℓ¹.

Equations

• Analytic.BanachSeries.toLp f = ⟨fun (ν : Fin m →₀ ℕ) => (MvPowerSeries.coeff ν) ↑f * ↑↑(Analytic.monomialEval (↑ρ) ν), ⋯⟩

theorem Analytic.BanachSeries.toLp_apply {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} (f : ↥(BanachSeries K ρ)) (ν : Fin m →₀ ℕ) : ↑(toLp f) ν = (MvPowerSeries.coeff ν) ↑f * ↑↑(monomialEval (↑ρ) ν)

theorem Analytic.BanachSeries.norm_toLp {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} (f : ↥(BanachSeries K ρ)) : ‖toLp f‖ = ‖f‖

noncomputable def Analytic.ofLpSeries (K : Type u_1) [RCLike K] {m : ℕ} (ρ : Radius m) (g : ↥(lp (fun (x : Fin m →₀ ℕ) => K) 1)) : MvPowerSeries (Fin m) K

The series with coefficients g ν / ρ^ν attached to an ℓ¹ family g.

Equations

• Analytic.ofLpSeries K ρ g ν = ↑g ν / ↑↑(Analytic.monomialEval (↑ρ) ν)

theorem Analytic.coeff_ofLpSeries {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} (g : ↥(lp (fun (x : Fin m →₀ ℕ) => K) 1)) (ν : Fin m →₀ ℕ) : (MvPowerSeries.coeff ν) (ofLpSeries K ρ g) = ↑g ν / ↑↑(monomialEval (↑ρ) ν)

theorem Analytic.convNorm_ofLpSeries_ne_top {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} (g : ↥(lp (fun (x : Fin m →₀ ℕ) => K) 1)) : ConvNorm (↑ρ) (ofLpSeries K ρ g) ≠ ⊤

The inverse: an ℓ¹ family g gives a series of finite ρ-norm, namely ‖g‖₁.

noncomputable def Analytic.BanachSeries.ofLp {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} (g : ↥(lp (fun (x : Fin m →₀ ℕ) => K) 1)) : ↥(BanachSeries K ρ)

The series with coefficients g ν / ρ^ν, in B ρ.

Equations

• Analytic.BanachSeries.ofLp g = ⟨Analytic.ofLpSeries K ρ g, ⋯⟩

noncomputable def Analytic.BanachSeries.toLpEquiv {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} : ↥(BanachSeries K ρ) ≃ₗᵢ[K] ↥(lp (fun (x : Fin m →₀ ℕ) => K) 1)

B_ρ is isometric to ℓ¹(Fin m →₀ ℕ; K) through the weighted coefficients.

Equations

• Analytic.BanachSeries.toLpEquiv = { toFun := Analytic.BanachSeries.toLp, map_add' := ⋯, map_smul' := ⋯, invFun := Analytic.BanachSeries.ofLp, left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }

instance Analytic.instCompleteSpaceSubtypeMvPowerSeriesFinMemSubalgebraBanachSeries {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} : CompleteSpace ↥(BanachSeries K ρ)

B_ρ is complete (a Banach algebra), by the isometry with ℓ¹.

@[reducible, inline]

noncomputable abbrev Analytic.banachSeries_normedRing (K : Type u_1) [RCLike K] {m : ℕ} (ρ : Radius m) : NormedRing ↥(BanachSeries K ρ)

The normed-ring structure of B_ρ, as a named declaration (the instance above).

Equations

• Analytic.banachSeries_normedRing K ρ = inferInstance

The real case

theorem Analytic.banachSeries_completeSpace {m : ℕ} (ρ : Radius m) : CompleteSpace ↥(BanachSeries ℝ ρ)

B ρ is complete, as a named declaration.