Division by a coordinate, at the function level

An analytic F on a polydisc vanishing on the hyperplane {x_k = 0} is x_k · G with G analytic on the same polydisc. Off the hyperplane G = F / x_k; on it G = ∂_k F. Analyticity of G at a point p of the hyperplane: expand F at p (Hironaka/Analytic/ConvSeries/Bridge.lean), F(p + y) = ∑ c_ν y^ν; the monomials free of y_k must vanish (the y_k-free part of c sums to zero on {y_k = 0}, hence everywhere by independence of y_k, hence is zero by uniqueness of coefficients), so c = y_k · divX k c and G(p + y) = ∑ (divX k c)_ν y^ν: for y_k ≠ 0 by division and for y_k = 0 by differentiating s ↦ s · (∑ (divX k c)_ν (y + s e_k)^ν) at s = 0. A coordinate subspace {x_k = 0, k ∈ I} inside {F = 0} on a polydisc gives F = ∑_{k ∈ I} x_k G_k by induction on I (division by x_k for F - F ∘ P_k, P_k setting x_k to 0; exists_sum_coord_mul_of_vanish_on_subspace). Not in the sources as such: it is the function-level form of the division by a coordinate that Bierstone and Milman use implicitly [BM88, proof of Theorem 4.4, pp. 24–25]. Used by the Taylor expansion of germs on a manifold (Hironaka/Manifold/Germ) and by the lifting of functions to a blow-up (Hironaka/Manifold/BlowUp).

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

@[simp]

theorem Analytic.evalSeries_zero {K : Type u_1} [RCLike K] {n : ℕ} (x : Fin n → K) : evalSeries 0 x = 0

theorem Analytic.isOpen_polydisc {K : Type u_1} [RCLike K] {n : ℕ} (ρ : Radius n) : IsOpen (polydisc K ρ)

The x_k-free part of a series

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

The monomials of c free of x_k.

Equations

• Analytic.freePart k c ν = if ν k = 0 then (MvPowerSeries.coeff ν) c else 0

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

theorem Analytic.convNorm_freePart_le {K : Type u_1} [RCLike K] {n : ℕ} (ρ : Fin n → NNReal) (k : Fin n) (c : MvPowerSeries (Fin n) K) : ConvNorm ρ (freePart k c) ≤ ConvNorm ρ c

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

theorem Analytic.monomialEval_update_zero_of_apply_eq_zero {K : Type u_1} [RCLike K] {n : ℕ} (x : Fin n → K) (k : Fin n) {ν : Fin n →₀ ℕ} (hν : ν k = 0) : monomialEval (Function.update x k 0) ν = monomialEval x ν

theorem Analytic.evalSeries_eq_freePart_of_apply_eq_zero {K : Type u_1} [RCLike K] {n : ℕ} (c : MvPowerSeries (Fin n) K) (k : Fin n) {x : Fin n → K} (hx : x k = 0) : evalSeries c x = evalSeries (freePart k c) x

On {x_k = 0} only the x_k-free monomials contribute.

theorem Analytic.evalSeries_freePart_update {K : Type u_1} [RCLike K] {n : ℕ} (c : MvPowerSeries (Fin n) K) (k : Fin n) (x : Fin n → K) : evalSeries (freePart k c) (Function.update x k 0) = evalSeries (freePart k c) x

The x_k-free part does not depend on x_k.

theorem Analytic.tendsto_update_zero {K : Type u_1} [RCLike K] {n : ℕ} (k : Fin n) : Filter.Tendsto (fun (x : Fin n → K) => Function.update x k 0) (nhds 0) (nhds 0)

theorem Analytic.coeff_eq_zero_of_eventually_vanish {K : Type u_1} [RCLike K] {n : ℕ} {c : MvPowerSeries (Fin n) K} (hc : c ∈ Conv K n) (k : Fin n) (hvan : ∀ᶠ (x : Fin n → K) in nhds 0, x k = 0 → evalSeries c x = 0) (ν : Fin n →₀ ℕ) : ν k = 0 → (MvPowerSeries.coeff ν) c = 0

A convergent series whose sum vanishes on {x_k = 0} near 0 has no monomials free of x_k.

Division by a coordinate

theorem Analytic.exists_eq_mul_coord_of_vanish {K : Type u_1} [RCLike K] {n : ℕ} (k : Fin n) {ρ : Radius n} {F : (Fin n → K) → K} (hF : AnalyticOnNhd K F (polydisc K ρ)) (h0 : ∀ x ∈ polydisc K ρ, x k = 0 → F x = 0) : ∃ (G : (Fin n → K) → K), AnalyticOnNhd K G (polydisc K ρ) ∧ ∀ x ∈ polydisc K ρ, F x = x k * G x

Division by a coordinate at function level: an analytic F on a polydisc vanishing on {x_k = 0} is x_k · G with G analytic on the same polydisc.

Coordinate subspaces inside the zero set

theorem Analytic.exists_polydisc_of_eventually {K : Type u_1} [RCLike K] {n : ℕ} {P : (Fin n → K) → Prop} (h : ∀ᶠ (y : Fin n → K) in nhds 0, P y) : ∃ (ρ : Radius n), ∀ y ∈ polydisc K ρ, P y

A statement true near 0 holds on some polydisc around 0.

noncomputable def Analytic.updateZeroCLM (K : Type u_1) [RCLike K] {n : ℕ} (k : Fin n) : (Fin n → K) →L[K] Fin n → K

Setting the coordinate k to 0, as a continuous linear map.

Equations

• Analytic.updateZeroCLM K k = ContinuousLinearMap.id K (Fin n → K) - ContinuousLinearMap.single K (fun (x : Fin n) => K) k ∘SL ContinuousLinearMap.proj k

theorem Analytic.updateZeroCLM_apply {K : Type u_1} [RCLike K] {n : ℕ} (k : Fin n) (x : Fin n → K) : (updateZeroCLM K k) x = Function.update x k 0

updateZeroCLM K k x is x with the coordinate k set to 0.

theorem Analytic.update_zero_mem_polydisc {K : Type u_1} [RCLike K] {n : ℕ} {ρ : Radius n} {x : Fin n → K} (hx : x ∈ polydisc K ρ) (k : Fin n) : Function.update x k 0 ∈ polydisc K ρ

Setting a coordinate to 0 stays in the polydisc.

theorem Analytic.exists_sum_coord_mul_of_vanish_on_subspace {K : Type u_1} [RCLike K] {n : ℕ} (I : Finset (Fin n)) {ρ : Radius n} {F : (Fin n → K) → K} (hF : AnalyticOnNhd K F (polydisc K ρ)) (hvan : ∀ x ∈ polydisc K ρ, (∀ k ∈ I, x k = 0) → F x = 0) : ∃ (G : Fin n → (Fin n → K) → K), (∀ k ∈ I, AnalyticOnNhd K (G k) (polydisc K ρ)) ∧ ∀ x ∈ polydisc K ρ, F x = ∑ k ∈ I, x k * G k x

A coordinate subspace inside the zero set on a polydisc gives F ∈ (x_k : k ∈ I) with analytic coefficients on the polydisc.