4.4. LocalMultiplicity.AnalyticLocalFactorization🔗

Jacobians.LocalMultiplicity.AnalyticLocalFactorization — source

analytic_local_factorization

Local analytic factorization at a zero of finite order.

If g is analytic at x₀ with g x₀ = w₀ and the analytic order of g - w₀ at x₀ equals k ∈ ℕ with k ≥ 1, then on a closed disk closedBall x₀ R (R > 0) there is a non-vanishing analytic factor u realising g z - w₀ = (z - x₀) ^ k * u z.

theorem analytic_local_factorization
    {g : ℂ → ℂ} {x₀ w₀ : ℂ} {k : ℕ}
    (_hk : 1 ≤ k)
    (hg : AnalyticAt ℂ g x₀)
    (_h_w₀ : g x₀ = w₀)
    (hord : analyticOrderAt (fun z => g z - w₀) x₀ = (k : ℕ∞)) :
    ∃ R : ℝ, 0 < R ∧ ∃ u : ℂ → ℂ,
      AnalyticOnNhd ℂ u (Metric.closedBall x₀ R) ∧ u x₀ ≠ 0 ∧
        ∀ z ∈ Metric.closedBall x₀ R, g z - w₀ = (z - x₀) ^ k * u z