The complex analytic Weierstrass preparation and division theorems

Let f : E × ℂ → ℂ be jointly holomorphic at (x₀, w₀) on the product of a finite-dimensional complex normed space E with ℂ, and assume that the slice w ↦ f (x₀, w) has finite order of vanishing d at w₀. This file proves the local analytic Weierstrass preparation theorem and Weierstrass division theorem by Cauchy's contour-integral method and Newton's identities.

Main results

• AnalyticAt.exists_weierstrassPreparation: Weierstrass preparation. If f is analytic at (x₀, w₀) and analyticOrderAt (fun w ↦ f (x₀, w)) w₀ = d, there exist analytic coefficient functions c : Fin d → E → ℂ vanishing at x₀ and a nonvanishing analytic function u at (x₀, w₀) such that near (x₀, w₀), f (x, w) = (TauCeti.Polynomial.monicOfCoeff (fun i ↦ c i x)).eval (w - w₀) * u (x, w).
• AnalyticAt.exists_weierstrassDivision_monicOfCoeff: Weierstrass division by a Weierstrass polynomial. Given analytic functions c : Fin d → E → ℂ vanishing at x₀ and any g analytic at (x₀, w₀), there exist q analytic at (x₀, w₀) and r : Fin d → E → ℂ analytic at x₀ such that near (x₀, w₀), g (x, w) = (TauCeti.Polynomial.monicOfCoeff (fun i ↦ c i x)).eval (w - w₀) * q (x, w) + ∑ i : Fin d, r i x * (w - w₀) ^ (i : ℕ).
• AnalyticAt.exists_weierstrassDivision: Weierstrass division. Combining preparation and division by a Weierstrass polynomial divides any analytic g by any f whose slice has order d at w₀.

Proof outline

After translating (x₀, w₀) to (0, 0), choose R > 0 so that w ↦ f (0, w) has 0 as its unique zero on closedBall 0 R, and then δ > 0 so that f (x, ·) is analytic on closedBall 0 R and nonvanishing on sphere 0 R for x ∈ ball 0 δ. For each such x, the residue theorem applied to ζ ↦ ζ ^ k * logDeriv (f (x, ·)) ζ expresses the k-th power sum of the zero multiset of f (x, ·) in ball 0 R (counted with multiplicity) as a contour integral whose integrand is jointly analytic along ball 0 δ ×ˢ sphere 0 R. Parametric analyticity of contour integrals (TauCeti.analyticOnNhd_circleIntegral) makes every power sum — and for k = 0 the total multiplicity, which is therefore locally constant and equal to d — analytic on ball 0 δ. Newton's identities (TauCeti.analyticAt_esymm_of_forall_analyticAt_sum_map_pow) and Vieta's formula (Multiset.prod_X_sub_C_coeff) turn this into analyticity of the coefficients of the monic polynomial P_x whose roots are those zeros. For each x, dividing f (x, ·) by P_x cancels all zeros in closedBall 0 R, so its meromorphic normal form u₀_x is analytic and nonvanishing on closedBall 0 R and represented on ball 0 R by Cauchy's integral formula, which makes (x, w) ↦ u₀_x w jointly analytic at (0, 0).

For division by P_x(w) = w ^ d + ∑ i, c_i(x) w ^ i, choose R > 0 and δ > 0 so that P_x is nonvanishing on sphere 0 R for x ∈ ball 0 δ. Expanding (P_x(ζ) - P_x(w)) / (ζ - w) as a polynomial in w of degree < d via geom_sum₂_mul rewrites the Cauchy kernel (ζ - w)⁻¹ as P_x(w) / ((ζ - w) P_x(ζ)) plus a degree-< d polynomial in w; integrating against (2πi)⁻¹ g (x, ζ) over C(0, R) produces the analytic quotient and remainder coefficients.

References

• L. Hörmander, An Introduction to Complex Analysis in Several Variables, §6.1.
• H. Grauert, R. Remmert, Coherent Analytic Sheaves, Ch. 2, §1.

theorem AnalyticAt.exists_weierstrassPreparation {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {f : E × ℂ → ℂ} {x₀ : E} {w₀ : ℂ} {d : ℕ} (hf : AnalyticAt ℂ f (x₀, w₀)) (hd : analyticOrderAt (fun (w : ℂ) => f (x₀, w)) w₀ = ↑d) : ∃ (c : Fin d → E → ℂ) (u : E × ℂ → ℂ), (∀ (i : Fin d), AnalyticAt ℂ (c i) x₀) ∧ (∀ (i : Fin d), c i x₀ = 0) ∧ AnalyticAt ℂ u (x₀, w₀) ∧ u (x₀, w₀) ≠ 0 ∧ f =ᶠ[nhds (x₀, w₀)] fun (p : E × ℂ) => Polynomial.eval (p.2 - w₀) (TauCeti.Polynomial.monicOfCoeff fun (i : Fin d) => c i p.1) * u p

Complex analytic Weierstrass preparation theorem. Let f : E × ℂ → ℂ be analytic at (x₀, w₀) on the product of a finite-dimensional complex normed space E with ℂ, and suppose the vertical slice w ↦ f (x₀, w) has finite order of vanishing d at w₀. Then there exist analytic coefficient functions c : Fin d → E → ℂ vanishing at x₀ and an analytic function u nonvanishing at (x₀, w₀) such that near (x₀, w₀), f (x, w) = (TauCeti.Polynomial.monicOfCoeff (fun i ↦ c i x)).eval (w - w₀) * u (x, w).

theorem AnalyticAt.exists_weierstrassDivision_monicOfCoeff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {d : ℕ} {c : Fin d → E → ℂ} {g : E × ℂ → ℂ} {x₀ : E} {w₀ : ℂ} (hg : AnalyticAt ℂ g (x₀, w₀)) (hc : ∀ (i : Fin d), AnalyticAt ℂ (c i) x₀) (hc0 : ∀ (i : Fin d), c i x₀ = 0) : ∃ (q : E × ℂ → ℂ) (r : Fin d → E → ℂ), AnalyticAt ℂ q (x₀, w₀) ∧ (∀ (i : Fin d), AnalyticAt ℂ (r i) x₀) ∧ g =ᶠ[nhds (x₀, w₀)] fun (p : E × ℂ) => Polynomial.eval (p.2 - w₀) (TauCeti.Polynomial.monicOfCoeff fun (i : Fin d) => c i p.1) * q p + ∑ i : Fin d, r i p.1 * (p.2 - w₀) ^ ↑i

Complex analytic Weierstrass division by a Weierstrass polynomial. Let c : Fin d → E → ℂ be analytic at x₀ with c i x₀ = 0, and let g : E × ℂ → ℂ be analytic at (x₀, w₀). Then there exist q : E × ℂ → ℂ analytic at (x₀, w₀) and r : Fin d → E → ℂ analytic at x₀ such that near (x₀, w₀), g (x, w) = (TauCeti.Polynomial.monicOfCoeff (fun i ↦ c i x)).eval (w - w₀) * q (x, w) + ∑ i : Fin d, r i x * (w - w₀) ^ (i : ℕ).

theorem AnalyticAt.exists_weierstrassDivision {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {f g : E × ℂ → ℂ} {x₀ : E} {w₀ : ℂ} {d : ℕ} (hg : AnalyticAt ℂ g (x₀, w₀)) (hf : AnalyticAt ℂ f (x₀, w₀)) (hd : analyticOrderAt (fun (w : ℂ) => f (x₀, w)) w₀ = ↑d) : ∃ (q : E × ℂ → ℂ) (r : Fin d → E → ℂ), AnalyticAt ℂ q (x₀, w₀) ∧ (∀ (i : Fin d), AnalyticAt ℂ (r i) x₀) ∧ g =ᶠ[nhds (x₀, w₀)] fun (p : E × ℂ) => f p * q p + ∑ i : Fin d, r i p.1 * (p.2 - w₀) ^ ↑i

Complex analytic Weierstrass division theorem. Let f, g : E × ℂ → ℂ be analytic at (x₀, w₀) on the product of a finite-dimensional complex normed space E with ℂ, and suppose the vertical slice w ↦ f (x₀, w) has finite order of vanishing d at w₀. Then there exist q analytic at (x₀, w₀) and r : Fin d → E → ℂ analytic at x₀ such that near (x₀, w₀), g (x, w) = f (x, w) * q (x, w) + ∑ i : Fin d, r i x * (w - w₀) ^ (i : ℕ).