Coordinates and monomials as convergent series; division by a coordinate

The coordinate x_k and the monomials x^θ as elements of Conv K n, and the coefficient shift divX k c with coeff ν (divX k c) = coeff (ν + e_k) c, which divides a series with no monomials free of x_k by x_k (X_mul_divX) and satisfies the majorant bound ‖divX k c‖_ρ ≤ ρ_k⁻¹ ‖c‖_ρ, so that it stays convergent; for k = 0 it is the quotient operator wQ 1 of the Weierstrass theory. These are the elementary facts about the local ring of germs that Bierstone and Milman use without comment when they factor a germ into smooth factors and monomials [BM88, proof of Theorem 4.4, pp. 24–25]; not in the sources as such.

The coefficient field K is ℝ or ℂ ([RCLike K]). The field-free lemmas of the germ theory are in Hironaka/Analytic/Germ/Base.lean.

noncomputable def Analytic.convX (K : Type u_1) [RCLike K] {n : ℕ} (k : Fin n) : ↥(Conv K n)

The coordinate x_k as an element of Conv K n.

Equations

• Analytic.convX K k = ⟨MvPowerSeries.X k, ⋯⟩

noncomputable def Analytic.convMonomial (K : Type u_1) [RCLike K] {n : ℕ} (θ : Fin n →₀ ℕ) : ↥(Conv K n)

The monomial x^θ as an element of Conv K n.

Equations

• Analytic.convMonomial K θ = ⟨(MvPowerSeries.monomial θ) 1, ⋯⟩

@[simp]

theorem Analytic.coe_convX {K : Type u_1} [RCLike K] {n : ℕ} (k : Fin n) : ↑(convX K k) = MvPowerSeries.X k

theorem Analytic.coe_convMonomial {K : Type u_1} [RCLike K] {n : ℕ} (θ : Fin n →₀ ℕ) : ↑(convMonomial K θ) = (MvPowerSeries.monomial θ) 1

theorem Analytic.convMonomial_zero {K : Type u_1} [RCLike K] {n : ℕ} : convMonomial K 0 = 1

theorem Analytic.convMonomial_add {K : Type u_1} [RCLike K] {n : ℕ} (θ θ' : Fin n →₀ ℕ) : convMonomial K (θ + θ') = convMonomial K θ * convMonomial K θ'

theorem Analytic.convMonomial_single {K : Type u_1} [RCLike K] {n : ℕ} (k : Fin n) : convMonomial K (Finsupp.single k 1) = convX K k

theorem Analytic.convX_ne_zero {K : Type u_1} [RCLike K] {n : ℕ} (k : Fin n) : convX K k ≠ 0

Division by a coordinate

noncomputable def Analytic.divX {K : Type u_1} [RCLike K] {n : ℕ} (k : Fin n) (c : MvPowerSeries (Fin n) K) : MvPowerSeries (Fin n) K

The coefficient shift x_k⁻¹ · (terms divisible by x_k): coeff ν (divX k c) = coeff (ν + e_k) c.

Equations

• Analytic.divX k c ν = (MvPowerSeries.coeff (ν + Finsupp.single k 1)) c

theorem Analytic.coeff_divX {K : Type u_1} [RCLike K] {n : ℕ} (k : Fin n) (c : MvPowerSeries (Fin n) K) (ν : Fin n →₀ ℕ) : (MvPowerSeries.coeff ν) (divX k c) = (MvPowerSeries.coeff (ν + Finsupp.single k 1)) c

theorem Analytic.X_mul_divX {K : Type u_1} [RCLike K] {n : ℕ} (k : Fin n) {c : MvPowerSeries (Fin n) K} (h0 : ∀ (ν : Fin n →₀ ℕ), ν k = 0 → (MvPowerSeries.coeff ν) c = 0) : MvPowerSeries.X k * divX k c = c

A series without monomials free of x_k is x_k times its shift.

theorem Analytic.coeff_X_mul_divX {K : Type u_1} [RCLike K] {n : ℕ} (k : Fin n) (c : MvPowerSeries (Fin n) K) (ν : Fin n →₀ ℕ) : (MvPowerSeries.coeff ν) (MvPowerSeries.X k * divX k c) = if ν k = 0 then 0 else (MvPowerSeries.coeff ν) c

Every series is x_k · divX k c plus its x_k-free part.

theorem Analytic.convNorm_divX_le {K : Type u_1} [RCLike K] {n : ℕ} (ρ : Radius n) (k : Fin n) (c : MvPowerSeries (Fin n) K) : ConvNorm (↑ρ) (divX k c) ≤ ↑(↑ρ k)⁻¹ * ConvNorm (↑ρ) c

The majorant bound ‖divX k c‖_ρ ≤ ρ_k⁻¹ ‖c‖_ρ.

theorem Analytic.divX_mem_conv {K : Type u_1} [RCLike K] {n : ℕ} (k : Fin n) {c : MvPowerSeries (Fin n) K} (hc : c ∈ Conv K n) : divX k c ∈ Conv K n

theorem Analytic.convX_dvd_of_coeff {K : Type u_1} [RCLike K] {n : ℕ} {c : ↥(Conv K n)} (k : Fin n) (h0 : ∀ (ν : Fin n →₀ ℕ), ν k = 0 → (MvPowerSeries.coeff ν) ↑c = 0) : convX K k ∣ c

x_k ∣ c in MvPowerSeries iff the monomials free of x_k are absent; in that case the quotient divX k c is convergent when c is.