Division of a power series without constant term by the coordinates

A series c with c(0) = 0 is ∑_i X_i · c_i, where c_i collects the monomials of c whose leading index (the first variable that occurs) is i, divided by X_i (divPart i c, sum_X_mul_divPart): Hadamard's lemma at the level of power series. The parts are as convergent as c (‖c_i‖_ρ · ρ_i ≤ ‖c‖_ρ, convNorm_divPart_mul_le, so Conv K n is stable, divPart_mem_conv), and they lose exactly one order: c ∈ 𝔪^(k+1) gives c_i ∈ 𝔪^k (divPart_mem_maximalIdeal_pow). The truncation of a series below a total degree (truncDeg) is a polynomial, hence convergent, and congruent to the series modulo 𝔪^k.

Not in the sources as such. This is the step that makes the Taylor homomorphism of a germ (the injective T_a : 𝒪_{M,a} → F_a[[X]] of [BM97, (0.3)]) reflect the powers of the maximal ideal, and gives 𝔪_a = (x_1 − a_1, …, x_n − a_n) for the germs at a point of a manifold (Hironaka/Manifold/Germ).

def Analytic.IsLeadIndex {n : ℕ} (i : Fin n) (d : Fin n →₀ ℕ) : Prop

i is the leading index of the exponent d: the first variable occurring in X^d.

Equations

• Analytic.IsLeadIndex i d = (d i ≠ 0 ∧ ∀ j < i, d j = 0)

theorem Analytic.IsLeadIndex.unique {n : ℕ} {i j : Fin n} {d : Fin n →₀ ℕ} (hi : IsLeadIndex i d) (hj : IsLeadIndex j d) : i = j

theorem Analytic.exists_isLeadIndex {n : ℕ} {d : Fin n →₀ ℕ} (hd : d ≠ 0) : ∃ (i : Fin n), IsLeadIndex i d

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

The i-th part of c: the monomials of c with leading index i, divided by X_i; coeff e (divPart i c) = coeff (e + e_i) c when i leads e + e_i, 0 otherwise.

Equations

• Analytic.divPart i c e = if Analytic.IsLeadIndex i (e + Finsupp.single i 1) then (MvPowerSeries.coeff (e + Finsupp.single i 1)) c else 0

theorem Analytic.coeff_divPart {K : Type u_1} [RCLike K] {n : ℕ} (i : Fin n) (c : MvPowerSeries (Fin n) K) (e : Fin n →₀ ℕ) : (MvPowerSeries.coeff e) (divPart i c) = if IsLeadIndex i (e + Finsupp.single i 1) then (MvPowerSeries.coeff (e + Finsupp.single i 1)) c else 0

theorem Analytic.coeff_X_mul' {K : Type u_1} [RCLike K] {n : ℕ} (i : Fin n) (φ : MvPowerSeries (Fin n) K) (d : Fin n →₀ ℕ) : (MvPowerSeries.coeff d) (MvPowerSeries.X i * φ) = if Finsupp.single i 1 ≤ d then (MvPowerSeries.coeff (d - Finsupp.single i 1)) φ else 0

The coefficients of X_i · φ.

theorem Analytic.sum_X_mul_divPart {K : Type u_1} [RCLike K] {n : ℕ} {c : MvPowerSeries (Fin n) K} (hc : MvPowerSeries.constantCoeff c = 0) : ∑ i : Fin n, MvPowerSeries.X i * divPart i c = c

Hadamard's lemma at the level of series: c = ∑_i X_i · divPart i c when c(0) = 0.

theorem Analytic.divPart_mem_maximalIdeal_pow {K : Type u_1} [RCLike K] {n : ℕ} {c : MvPowerSeries (Fin n) K} {k : ℕ} (hc : c ∈ IsLocalRing.maximalIdeal (MvPowerSeries (Fin n) K) ^ (k + 1)) (i : Fin n) : divPart i c ∈ IsLocalRing.maximalIdeal (MvPowerSeries (Fin n) K) ^ k

The parts lose one order: c ∈ 𝔪^(k+1) gives divPart i c ∈ 𝔪^k.

theorem Analytic.convNorm_divPart_mul_le {K : Type u_1} [RCLike K] {n : ℕ} (ρ : Fin n → NNReal) (i : Fin n) (c : MvPowerSeries (Fin n) K) : ConvNorm ρ (divPart i c) * ↑(ρ i) ≤ ConvNorm ρ c

‖divPart i c‖_ρ · ρ_i ≤ ‖c‖_ρ.

theorem Analytic.divPart_mem_conv {K : Type u_1} [RCLike K] {n : ℕ} {c : MvPowerSeries (Fin n) K} (hc : c ∈ Conv K n) (i : Fin n) : divPart i c ∈ Conv K n

The parts of a convergent series are convergent.

Constants are convergent (monomials and coordinates: monomial_mem_conv, X_mem_conv in

Hironaka/Analytic/Weierstrass/Normalize.lean)

theorem Analytic.C_mem_conv {K : Type u_1} [RCLike K] {n : ℕ} (a : K) : MvPowerSeries.C a ∈ Conv K n

Truncation below a total degree

noncomputable def Analytic.degreeBelow (n k : ℕ) : Finset (Fin n →₀ ℕ)

The exponents of total degree < k.

Equations

• Analytic.degreeBelow n k = (Finset.range k).biUnion (Analytic.degreeSet n)

theorem Analytic.mem_degreeBelow {n k : ℕ} {d : Fin n →₀ ℕ} : d ∈ degreeBelow n k ↔ Finsupp.degree d < k

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

The truncation of c below total degree k, a polynomial.

Equations

• Analytic.truncDeg k c = ∑ d ∈ Analytic.degreeBelow n k, (MvPowerSeries.monomial d) ((MvPowerSeries.coeff d) c)

theorem Analytic.coeff_truncDeg {K : Type u_1} [RCLike K] {n : ℕ} (k : ℕ) (c : MvPowerSeries (Fin n) K) (d : Fin n →₀ ℕ) : (MvPowerSeries.coeff d) (truncDeg k c) = if Finsupp.degree d < k then (MvPowerSeries.coeff d) c else 0

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

theorem Analytic.sub_truncDeg_mem_maximalIdeal_pow {K : Type u_1} [RCLike K] {n : ℕ} (k : ℕ) (c : MvPowerSeries (Fin n) K) : c - truncDeg k c ∈ IsLocalRing.maximalIdeal (MvPowerSeries (Fin n) K) ^ k

c ≡ truncDeg k c modulo 𝔪^k.