Weierstrass division: the distinguished variable, regularity and the splitting operators

The Weierstrass preparation theorem, in the form Bierstone and Milman use it, prepares a germ f with f(0, …, 0, x_m) ∼ x_m^e in a distinguished last variable [BM88, proof of Theorem 4.4, p. 24]. Here the distinguished variable is the coordinate 0 of Fin (m + 1) and the remaining variables are the Fin.succ j, because Mathlib's isomorphism MvPowerSeries.finSuccEquiv between MvPowerSeries (Fin (m + 1)) R and PowerSeries (MvPowerSeries (Fin m) R) singles out the first variable: the printed x_m is our x_0 and the printed x̃ our x_1, …, x_m. This relabelling of the coordinates is the convention of every module of the Weierstrass theory and of the germ theory built on it.

• splitFirst K m is that isomorphism; liftTail c embeds a series in the tail variables and liftFirst e a series in x_0 alone into the series in all variables.
• IsRegularIn g d: g(x_0, 0, …, 0) = x_0^d · e(x_0) with e(0) ≠ 0, stated as the hypothesis of Mathlib's Weierstrass division: the image of splitFirst K m g in the residue field of the tail ring MvPowerSeries (Fin m) K has PowerSeries.order exactly d.
• wQ d F and wR d F are the splitting operators: F = x_0^d · wQ d F + wR d F with wR d F of x_0-degree < d, coefficientwise (the norm bounds are in Splitting.lean). They are the operators of the Banach-algebra proof of the division theorem [GR71, Kapitel I].
• weierstrassPoly d c = x_0^d + ∑_{j < d} c_j x_0^{d - 1 - j} for coefficients c_j in the tail variables, the printed x_m^d + ∑_{j=1}^d c_j(x̃) x_m^{d-j}.
• polydisc K ρ is the open polydisc {x | ∀ k, ‖x_k‖ < ρ_k} of a radius vector (mem_polydisc_iff; it contains a neighbourhood of 0, eventually_abs_lt), and TailVanishes h says that h has no pure x_0-monomials, i.e. h(x_0, 0, …, 0) = 0.

The coefficient field K is ℝ or ℂ ([RCLike K]).

@[reducible, inline]

noncomputable abbrev Analytic.splitFirst (K : Type u_1) [RCLike K] (m : ℕ) : MvPowerSeries (Fin (m + 1)) K ≃ₐ[K] PowerSeries (MvPowerSeries (Fin m) K)

The split of the distinguished variable x_0 (Mathlib's finSuccEquiv).

Equations

• Analytic.splitFirst K m = MvPowerSeries.finSuccEquiv K m

noncomputable def Analytic.liftTail {K : Type u_1} [RCLike K] {m : ℕ} (c : MvPowerSeries (Fin m) K) : MvPowerSeries (Fin (m + 1)) K

A series in the tail variables x_1, …, x_m, as a series in all variables.

Equations

• Analytic.liftTail c = (MvPowerSeries.rename Fin.succ) c

def Analytic.IsRegularIn {K : Type u_1} [RCLike K] {m : ℕ} (g : MvPowerSeries (Fin (m + 1)) K) (d : ℕ) : Prop

g is x_0-regular of order d: g(x_0, 0, …, 0) = x_0^d e(x_0) with e(0) ≠ 0, i.e. the image of splitFirst K m g in the residue field of the tail ring MvPowerSeries (Fin m) K has order exactly d (Mathlib's Weierstrass hypothesis g.map (IsLocalRing.residue A) ≠ 0 with the order made explicit). This is the printed condition f_a(0, …, 0, x_m) ∼ x_m^e of [BM88, proof of Theorem 4.4, p. 24].

Equations

• Analytic.IsRegularIn g d = (((PowerSeries.map (IsLocalRing.residue (MvPowerSeries (Fin m) K))) ((Analytic.splitFirst K m) g)).order = ↑d)

noncomputable def Analytic.wQ {K : Type u_1} [RCLike K] {m : ℕ} (d : ℕ) (F : MvPowerSeries (Fin (m + 1)) K) : MvPowerSeries (Fin (m + 1)) K

The quotient part of the splitting F = x_0^d · wQ d F + wR d F: the terms of x_0-degree ≥ d, divided by x_0^d.

Equations

• Analytic.wQ d F ν = (MvPowerSeries.coeff (ν + Finsupp.single 0 d)) F

noncomputable def Analytic.wR {K : Type u_1} [RCLike K] {m : ℕ} (d : ℕ) (F : MvPowerSeries (Fin (m + 1)) K) : MvPowerSeries (Fin (m + 1)) K

The remainder part of the splitting: the terms of x_0-degree < d.

Equations

• Analytic.wR d F ν = if ν 0 < d then (MvPowerSeries.coeff ν) F else 0

theorem Analytic.coeff_wQ {K : Type u_1} [RCLike K] {m : ℕ} (d : ℕ) (F : MvPowerSeries (Fin (m + 1)) K) (ν : Fin (m + 1) →₀ ℕ) : (MvPowerSeries.coeff ν) (wQ d F) = (MvPowerSeries.coeff (ν + Finsupp.single 0 d)) F

theorem Analytic.coeff_wR {K : Type u_1} [RCLike K] {m : ℕ} (d : ℕ) (F : MvPowerSeries (Fin (m + 1)) K) (ν : Fin (m + 1) →₀ ℕ) : (MvPowerSeries.coeff ν) (wR d F) = if ν 0 < d then (MvPowerSeries.coeff ν) F else 0

theorem Analytic.X_pow_mul_wQ_add_wR {K : Type u_1} [RCLike K] {m : ℕ} (d : ℕ) (F : MvPowerSeries (Fin (m + 1)) K) : MvPowerSeries.X 0 ^ d * wQ d F + wR d F = F

The splitting identity F = x_0^d · wQ d F + wR d F.

theorem Analytic.coeff_wR_of_le {K : Type u_1} [RCLike K] {m : ℕ} (d : ℕ) (F : MvPowerSeries (Fin (m + 1)) K) {ν : Fin (m + 1) →₀ ℕ} (h : d ≤ ν 0) : (MvPowerSeries.coeff ν) (wR d F) = 0

wR d F has x_0-degree < d: its coefficients vanish where ν 0 ≥ d.

noncomputable def Analytic.weierstrassPoly {K : Type u_1} [RCLike K] {m : ℕ} (d : ℕ) (c : Fin d → MvPowerSeries (Fin m) K) : MvPowerSeries (Fin (m + 1)) K

The Weierstrass polynomial x_0^d + ∑_{j < d} c_j x_0^{d - 1 - j} with coefficients in the tail variables: the printed x_m^d + ∑_{j=1}^d c_j(x̃) x_m^{d-j} of BM88, Theorem 4.4, proof, p. 24.

Equations

• Analytic.weierstrassPoly d c = MvPowerSeries.X 0 ^ d + ∑ j : Fin d, Analytic.liftTail (c j) * MvPowerSeries.X 0 ^ (d - 1 - ↑j)

noncomputable def Analytic.liftFirst {K : Type u_1} [RCLike K] {m : ℕ} (e : MvPowerSeries (Fin 1) K) : MvPowerSeries (Fin (m + 1)) K

A series in the single variable x_0, as a series in all variables.

Equations

• Analytic.liftFirst e = (MvPowerSeries.rename fun (x : Fin 1) => 0) e

def Analytic.polydisc (K : Type u_1) [RCLike K] {m : ℕ} (ρ : Radius m) : Set (Fin m → K)

The open polydisc {x | ∀ k, ‖x_k‖ < ρ_k} of a radius vector.

Equations

• Analytic.polydisc K ρ = {x : Fin m → K | ∀ (k : Fin m), ‖x k‖ < ↑(↑ρ k)}

def Analytic.TailVanishes {K : Type u_1} [RCLike K] {m : ℕ} (h : MvPowerSeries (Fin (m + 1)) K) : Prop

A series h in all variables with h(x_0, 0, …, 0) = 0: no pure x_0-monomials.

Equations

• Analytic.TailVanishes h = ∀ (k : ℕ), (MvPowerSeries.coeff (Finsupp.single 0 k)) h = 0

theorem Analytic.eventually_abs_lt {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Radius m) : ∀ᶠ (y : Fin m → K) in nhds 0, ∀ (k : Fin m), ‖y k‖ < ↑(↑ρ k)

Every radius vector bounds the coordinates of the points near 0.

@[simp]

theorem Analytic.mem_polydisc_iff {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} {x : Fin m → K} : x ∈ polydisc K ρ ↔ ∀ (k : Fin m), ‖x k‖ < ↑(↑ρ k)

Membership in the open polydisc, unfolded.