Generic linear changes and the order on the axis

"There are local coordinates x = (x_1, …, x_m) centered at a such that f_a(0, …, 0, x_m) ∼ x_m^e, where e = μ_a(f)" [BM88, proof of Theorem 4.4, p. 24]. The degree-e homogeneous part of a nonzero series of order e is a nonzero polynomial (homogeneousPoly of Hironaka/Analytic/ConvSeries/Bridge.lean), hence nonzero at some direction v since the field is infinite (MvPolynomial.funext); a linear automorphism L with L e_0 = v exists (a coordinate swap followed by x ↦ x + x_k (v - e_k)); and the restriction of f to the line K v is the one-variable series dirSeries f v whose degree-d coefficient is the degree-d part at v. Its leading term is t^e · h_e(v) with h_e(v) ≠ 0, which is the hypothesis form of the function-level preparation theorem.

Second, restricting to the x_0-axis (axis) never lowers the order, with equality iff the coefficient of x_0^{μ(f)} is nonzero; orders add under products on both sides (order_mul), so equality for a product forces equality for every factor: the printed "each ℓ_{i,a}(0, …, 0, x_m) ∼ x_m" of the same passage. Bierstone and Milman use both parts to choose the coordinates of that proof.

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

Linear changes sending e_0 to a given vector

noncomputable def Analytic.replaceBasis {K : Type u_1} [RCLike K] {n : ℕ} (k : Fin n) (v : Fin n → K) (hv : v k ≠ 0) : (Fin n → K) ≃ₗ[K] Fin n → K

x ↦ x + x_k • (v - e_k): fixes e_j for j ≠ k and sends e_k to v; a linear automorphism when v_k ≠ 0.

Equations

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

theorem Analytic.replaceBasis_single {K : Type u_1} [RCLike K] {n : ℕ} (k : Fin n) (v : Fin n → K) (hv : v k ≠ 0) : (replaceBasis k v hv) (Pi.single k 1) = v

noncomputable def Analytic.swapCoord (K : Type u_1) [RCLike K] {n : ℕ} (k : Fin (n + 1)) : (Fin (n + 1) → K) ≃ₗ[K] Fin (n + 1) → K

The coordinate swap 0 ↔ k as a linear automorphism of K^{n+1}.

Equations

• Analytic.swapCoord K k = LinearEquiv.funCongrLeft K K (Equiv.swap 0 k)

theorem Analytic.swapCoord_single_zero {K : Type u_1} [RCLike K] {n : ℕ} (k : Fin (n + 1)) : (swapCoord K k) (Pi.single 0 1) = Pi.single k 1

theorem Analytic.exists_continuousLinearEquiv_single_eq {K : Type u_1} [RCLike K] {n : ℕ} {v : Fin (n + 1) → K} (hv : v ≠ 0) : ∃ (L : (Fin (n + 1) → K) ≃L[K] Fin (n + 1) → K), L (Pi.single 0 1) = v

The linear change: every nonzero vector is L e_0 for a linear automorphism L.

The leading homogeneous part

theorem Analytic.exists_eval_homogeneousPoly_ne_zero {K : Type u_1} [RCLike K] {n : ℕ} {f : MvPowerSeries (Fin n) K} (hf : f ≠ 0) : ∃ (v : Fin n → K), (MvPolynomial.eval v) (homogeneousPoly f f.order.toNat) ≠ 0

The leading homogeneous part of a nonzero series is nonzero at some direction (the field is infinite).

theorem Analytic.monomialEval_smul {K : Type u_1} [RCLike K] {n : ℕ} (t : K) (v : Fin n → K) (ν : Fin n →₀ ℕ) : monomialEval (t • v) ν = t ^ Finsupp.degree ν * monomialEval v ν

Evaluating a monomial on a multiple of v: (t v)^ν = t^{|ν|} v^ν.

theorem Analytic.hasSum_evalSeries_smul {K : Type u_1} [RCLike K] {n : ℕ} {ρ : Radius n} {f : MvPowerSeries (Fin n) K} (hf : ConvNorm (↑ρ) f ≠ ⊤) {t : K} {v : Fin n → K} (h : ∀ (k : Fin n), ‖t * v k‖ ≤ ↑(↑ρ k)) : HasSum (fun (d : ℕ) => t ^ d * (MvPolynomial.eval v) (homogeneousPoly f d)) (evalSeries f (t • v))

The sum of a convergent series along the line t v, regrouped by degree.

The restriction of a series to a line

noncomputable def Analytic.dirSeries {K : Type u_1} [RCLike K] {n : ℕ} (f : MvPowerSeries (Fin n) K) (v : Fin n → K) : MvPowerSeries (Fin 1) K

The restriction of f to the line K v, as a series in one variable: its degree-d coefficient is the degree-d homogeneous part of f at v.

Equations

• Analytic.dirSeries f v μ = (MvPolynomial.eval v) (Analytic.homogeneousPoly f (μ 0))

theorem Analytic.coeff_dirSeries {K : Type u_1} [RCLike K] {n : ℕ} (f : MvPowerSeries (Fin n) K) (v : Fin n → K) (μ : Fin 1 →₀ ℕ) : (MvPowerSeries.coeff μ) (dirSeries f v) = (MvPolynomial.eval v) (homogeneousPoly f (μ 0))

theorem Analytic.coeff_single_dirSeries {K : Type u_1} [RCLike K] {n : ℕ} (f : MvPowerSeries (Fin n) K) (v : Fin n → K) (d : ℕ) : (MvPowerSeries.coeff (Finsupp.single 0 d)) (dirSeries f v) = (MvPolynomial.eval v) (homogeneousPoly f d)

theorem Analytic.evalSeries_dirSeries {K : Type u_1} [RCLike K] {n : ℕ} {ρ : Radius n} {f : MvPowerSeries (Fin n) K} (hf : ConvNorm (↑ρ) f ≠ ⊤) {t : K} {v : Fin n → K} (h : ∀ (k : Fin n), ‖t * v k‖ ≤ ↑(↑ρ k)) : (evalSeries (dirSeries f v) fun (x : Fin 1) => t) = evalSeries f (t • v)

theorem Analytic.nnnorm_monomialEval_mul_pow_le {K : Type u_1} [RCLike K] {n : ℕ} {ρ : Fin n → NNReal} {r : NNReal} {v : Fin n → K} (hrv : ∀ (k : Fin n), r * ‖v k‖₊ ≤ ρ k) {d : ℕ} {ν : Fin n →₀ ℕ} (hν : Finsupp.degree ν = d) : ‖monomialEval v ν‖₊ * r ^ d ≤ monomialEval ρ ν

|v^ν| r^{|ν|} ≤ ρ^ν when r |v_k| ≤ ρ_k for every k.

theorem Analytic.convNorm_dirSeries_le {K : Type u_1} [RCLike K] {n : ℕ} {ρ : Fin n → NNReal} {r : NNReal} {v : Fin n → K} (hrv : ∀ (k : Fin n), r * ‖v k‖₊ ≤ ρ k) (f : MvPowerSeries (Fin n) K) : ConvNorm (fun (x : Fin 1) => r) (dirSeries f v) ≤ ConvNorm ρ f

The restriction to a line converges on the radius r when r |v_k| ≤ ρ_k: ‖dirSeries f v‖_r ≤ ‖f‖_ρ.

theorem Analytic.exists_radius_smul_le {K : Type u_1} [RCLike K] {n : ℕ} (ρ : Radius n) (v : Fin n → K) : ∃ (r : NNReal), 0 < r ∧ ∀ (k : Fin n), r * ‖v k‖₊ ≤ ↑ρ k

A radius r > 0 with r |v_k| ≤ ρ_k for all k.

The generic linear change

theorem Analytic.homogeneousPoly_eq_zero_of_lt_order {K : Type u_1} [RCLike K] {n : ℕ} {f : MvPowerSeries (Fin n) K} {d : ℕ} (hd : ↑d < f.order) : homogeneousPoly f d = 0

theorem Analytic.eval_zero_homogeneousPoly_of_pos {K : Type u_1} [RCLike K] {n : ℕ} (f : MvPowerSeries (Fin n) K) {d : ℕ} (hd : 0 < d) : (MvPolynomial.eval 0) (homogeneousPoly f d) = 0

A homogeneous part of positive degree vanishes at the origin.

theorem Analytic.wR_dirSeries_eq_zero {K : Type u_1} [RCLike K] {n : ℕ} {f : MvPowerSeries (Fin n) K} (v : Fin n → K) : wR f.order.toNat (dirSeries f v) = 0

The remainder part of the line restriction below the order vanishes.

noncomputable def Analytic.constCLM (K : Type u_1) [RCLike K] : K →L[K] Fin 1 → K

The map t ↦ (t, …, t) : K → K^1 as a continuous linear map.

Equations

• Analytic.constCLM K = ContinuousLinearMap.pi fun (x : Fin 1) => ContinuousLinearMap.id K K

theorem Analytic.constCLM_apply {K : Type u_1} [RCLike K] (t : K) : (constCLM K) t = fun (x : Fin 1) => t

theorem Analytic.eventually_abs_lt_real {K : Type u_1} [RCLike K] (r : NNReal) (hr : 0 < r) : ∀ᶠ (t : K) in nhds 0, ‖t‖ < ↑r

theorem Analytic.exists_linearChange_axis_regular {K : Type u_1} [RCLike K] {m : ℕ} {f : MvPowerSeries (Fin (m + 1)) K} (hf : f ∈ Conv K (m + 1)) (hf0 : f ≠ 0) : ∃ (L : (Fin (m + 1) → K) ≃L[K] Fin (m + 1) → K) (e : K → K), AnalyticAt K e 0 ∧ e 0 ≠ 0 ∧ ∀ᶠ (t : K) in nhds 0, evalSeries f (L (Pi.single 0 t)) = t ^ f.order.toNat * e t

After a linear change, a nonzero convergent f of order e is x_0-regular of order e on the axis, in the hypothesis form of the function-level preparation theorem: the printed "there are local coordinates … such that f_a(0, …, 0, x_m) ∼ x_m^e" of BM88, proof of Theorem 4.4, p. 24.

The order on the axis

theorem Analytic.order_le_order_axis {K : Type u_1} [RCLike K] {m : ℕ} (f : MvPowerSeries (Fin (m + 1)) K) : f.order ≤ (axis f).order

The order does not drop under restriction to the axis.

theorem Analytic.eval_single_homogeneousPoly {K : Type u_1} [RCLike K] {m : ℕ} (f : MvPowerSeries (Fin (m + 1)) K) (e : ℕ) : (MvPolynomial.eval (Pi.single 0 1)) (homogeneousPoly f e) = (MvPowerSeries.coeff (Finsupp.single 0 e)) f

The degree-e homogeneous part at e_0 is the coefficient of x_0^e.

theorem Analytic.order_axis_eq_iff {K : Type u_1} [RCLike K] {m : ℕ} {f : MvPowerSeries (Fin (m + 1)) K} (hf : f ≠ 0) : (axis f).order = f.order ↔ (MvPowerSeries.coeff (Finsupp.single 0 f.order.toNat)) f ≠ 0

Equality of orders on the axis iff the coefficient of x_0^{μ(f)} is nonzero.

theorem Analytic.order_axis_eq_of_mul {K : Type u_1} [RCLike K] {m : ℕ} {f g : MvPowerSeries (Fin (m + 1)) K} (hf : f ≠ 0) (hg : g ≠ 0) (h : (axis (f * g)).order = (f * g).order) : (axis f).order = f.order ∧ (axis g).order = g.order

For two factors: if the order of f g is preserved on the axis, so are the orders of f and g (orders add on both sides).

theorem Analytic.order_axis_eq_of_prod {K : Type u_1} [RCLike K] {m : ℕ} {ι : Type u_2} (s : Finset ι) (f : ι → MvPowerSeries (Fin (m + 1)) K) (hne : ∀ i ∈ s, f i ≠ 0) (h : (axis (∏ i ∈ s, f i)).order = (∏ i ∈ s, f i).order) (i : ι) : i ∈ s → (axis (f i)).order = (f i).order

If the order of a product is preserved on the axis, so is the order of every factor: the printed "each ℓ_{i,a}(0, …, 0, x_m) ∼ x_m" of [BM88, proof of Theorem 4.4, p. 24].