The majorant norms ‖f‖_ρ and the convergent series over K = ℝ or ℂ

The ring of germs of K-analytic functions at 0 ∈ K^m, K ∈ {ℝ, ℂ} ([RCLike K]), is modelled by the ring of convergent power series in m variables: a formal series f = ∑_ν a_ν x^ν ∈ MvPowerSeries (Fin m) K is convergent when for some radius vector ρ ∈ (0, ∞)^m its majorant norm ‖f‖_ρ = ∑_ν ‖a_ν‖ ρ^ν (an ℝ≥0∞-valued sum over Fin m →₀ ℕ) is finite. This is the classical construction of the local ring of convergent power series through the Banach algebras of series with finite majorant norm [GR71, Kapitel I]; for K = ℝ it models the local ring 𝒪_a of germs of analytic functions of [BM88, p. 23].

• ConvNorm ρ f is the norm, for a radius vector ρ : Fin m → ℝ≥0; it is subadditive, homogeneous, submultiplicative (ConvNorm_mul_le, the Cauchy-product bound through MvPowerSeries.coeff_mul), equal to 1 on 1, and monotone in ρ.
• BanachSeries K ρ (written B_ρ in the docstrings, for ρ : Radius m) is the subalgebra of series with ‖f‖_ρ < ∞; its Banach algebra structure is in Banach.lean.
• Conv K m is the union of the BanachSeries K ρ over all ρ : Radius m: the ring of convergent power series, a subalgebra of MvPowerSeries (Fin m) K because two radius vectors have a common smaller one and the norm is monotone. The monomials and the coordinates are convergent (convNorm_monomial, monomial_mem_conv, X_mem_conv).

Every proof is coefficientwise on the majorant norm. The field K is explicit in BanachSeries K ρ and Conv K m (no argument carries it) and implicit everywhere else. The real instances of these declarations, under the same names in namespace Hironaka.Analytic, are restated in Hironaka/Analytic/ConvSeries/ConvNorm.lean; the field-free material (radius vectors, exponents, monomials) is in Hironaka/Analytic/ConvSeries/Radius.lean.

noncomputable def Analytic.ConvNorm {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Fin m → NNReal) (f : MvPowerSeries (Fin m) K) : ENNReal

The majorant norm ‖f‖_ρ = ∑_ν ‖a_ν‖ ρ^ν of a formal power series, as an ℝ≥0∞-valued sum over all exponents [GR71, Kapitel I].

Equations

• Analytic.ConvNorm ρ f = ∑' (ν : Fin m →₀ ℕ), ‖(MvPowerSeries.coeff ν) f‖ₑ * ↑(Analytic.monomialEval ρ ν)

theorem Analytic.ConvNorm_zero {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Fin m → NNReal) : ConvNorm ρ 0 = 0

theorem Analytic.ConvNorm_one {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Fin m → NNReal) : ConvNorm ρ 1 = 1

theorem Analytic.ConvNorm_neg {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Fin m → NNReal) (f : MvPowerSeries (Fin m) K) : ConvNorm ρ (-f) = ConvNorm ρ f

theorem Analytic.ConvNorm_add_le {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Fin m → NNReal) (f g : MvPowerSeries (Fin m) K) : ConvNorm ρ (f + g) ≤ ConvNorm ρ f + ConvNorm ρ g

theorem Analytic.ConvNorm_smul {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Fin m → NNReal) (c : K) (f : MvPowerSeries (Fin m) K) : ConvNorm ρ (c • f) = ‖c‖ₑ * ConvNorm ρ f

theorem Analytic.ConvNorm_algebraMap {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Fin m → NNReal) (c : K) : ConvNorm ρ ((algebraMap K (MvPowerSeries (Fin m) K)) c) = ‖c‖ₑ

The scalar c, as the constant series, has norm ‖c‖.

theorem Analytic.ConvNorm_mono {K : Type u_1} [RCLike K] {m : ℕ} {ρ ρ' : Fin m → NNReal} (h : ∀ (k : Fin m), ρ k ≤ ρ' k) (f : MvPowerSeries (Fin m) K) : ConvNorm ρ f ≤ ConvNorm ρ' f

The norm is monotone in the radius vector.

theorem Analytic.ConvNorm_mul_le {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Fin m → NNReal) (f g : MvPowerSeries (Fin m) K) : ConvNorm ρ (f * g) ≤ ConvNorm ρ f * ConvNorm ρ g

The Cauchy-product bound ‖f g‖_ρ ≤ ‖f‖_ρ ‖g‖_ρ: the coefficient of x^ν in f g is the sum over the antidiagonal of ν (MvPowerSeries.coeff_mul), each term is bounded by ‖a_μ‖ ρ^μ · ‖b_{ν-μ}‖ ρ^{ν-μ}, and the double sum over all antidiagonals is the product of the two norms.

def Analytic.BanachSeries (K : Type u_1) [RCLike K] {m : ℕ} (ρ : Radius m) : Subalgebra K (MvPowerSeries (Fin m) K)

The series of finite ρ-norm form a subalgebra B_ρ of the formal series (closed under sums, products and scalars by the norm inequalities above).

Equations

• Analytic.BanachSeries K ρ = { carrier := {f : MvPowerSeries (Fin m) K | Analytic.ConvNorm (↑ρ) f ≠ ⊤}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯ }

theorem Analytic.mem_banachSeries {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} {f : MvPowerSeries (Fin m) K} : f ∈ BanachSeries K ρ ↔ ConvNorm (↑ρ) f ≠ ⊤

theorem Analytic.BanachSeries.mono {K : Type u_1} [RCLike K] {m : ℕ} {ρ ρ' : Radius m} (h : ∀ (k : Fin m), ↑ρ k ≤ ↑ρ' k) : BanachSeries K ρ' ≤ BanachSeries K ρ

def Analytic.Conv (K : Type u_1) [RCLike K] (m : ℕ) : Subalgebra K (MvPowerSeries (Fin m) K)

The ring Conv K m of convergent power series: the series with finite ρ-norm for some radius vector with positive entries, the model of the ring of germs of K-analytic functions at 0 ∈ K^m (for K = ℝ the local ring 𝒪_a of [BM88, p. 23]). It is a subalgebra because two radius vectors have a common lower bound and the norm is monotone in the radius.

Equations

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

theorem Analytic.mem_conv {K : Type u_1} [RCLike K] {m : ℕ} {f : MvPowerSeries (Fin m) K} : f ∈ Conv K m ↔ ∃ (ρ : Radius m), ConvNorm (↑ρ) f ≠ ⊤

theorem Analytic.BanachSeries.le_conv {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Radius m) : BanachSeries K ρ ≤ Conv K m

Monomials

theorem Analytic.convNorm_monomial {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Fin m → NNReal) (ν : Fin m →₀ ℕ) (a : K) : ConvNorm ρ ((MvPowerSeries.monomial ν) a) = ‖a‖ₑ * ↑(monomialEval ρ ν)

The majorant norm of a monomial a x^ν is ‖a‖ ρ^ν.

theorem Analytic.monomial_mem_conv {K : Type u_1} [RCLike K] {m : ℕ} (ν : Fin m →₀ ℕ) (a : K) : (MvPowerSeries.monomial ν) a ∈ Conv K m

Monomials are convergent.

theorem Analytic.X_mem_conv {K : Type u_1} [RCLike K] {m : ℕ} (k : Fin m) : MvPowerSeries.X k ∈ Conv K m

The coordinates are convergent.