local_meromorphic_factorization

formal source

  82`meromorphicOrderAt_eq_int_iff`. The regular factor `g` is the actual
  83analytic nonvanishing part from the Weierstrass factorization, not a
  84dummy constant. -/
  85theorem local_meromorphic_factorization
  86    (f : ℂ → ℂ) (ρ : ℂ) (n : ℤ) (hf : MeromorphicAt f ρ)
  87    (hn : meromorphicOrderAt f ρ = ↑n) :
  88    ∃ w : LocalMeromorphicWitness, w.center = ρ ∧ w.order = n := by
  89  obtain ⟨g, hg_an, hg_ne, _⟩ := (meromorphicOrderAt_eq_int_iff hf).mp hn
  90  obtain ⟨r₁, hr₁, hg_ball⟩ := hg_an.exists_ball_analyticOnNhd
  91  obtain ⟨r₂, hr₂, hg_nz⟩ :=
  92    Metric.eventually_nhds_iff.mp (hg_an.continuousAt.eventually_ne hg_ne)
  93  refine ⟨{ center := ρ, order := n, radius := min r₁ r₂ / 2,
  94            radius_pos := by positivity,
  95            regularFactor := g,
  96            regularFactor_analytic := hg_an,
  97            regularFactor_diff := ?_,
  98            regularFactor_nz := ?_ }, rfl, rfl⟩
  99  · apply AnalyticOnNhd.differentiableOn
 100    intro z hz
 101    exact hg_ball z (Metric.mem_ball.mpr
 102      (lt_of_le_of_lt (Metric.mem_closedBall.mp hz)
 103        (by linarith [min_le_left r₁ r₂])))
 104  · exact fun z hz => hg_nz
 105      (lt_of_le_of_lt (Metric.mem_closedBall.mp hz)
 106        (by linarith [min_le_right r₁ r₂]))
 107
 108/-! ### §2. Phase charge equals negative order -/
 109
 110theorem meromorphic_phase_charge (w : LocalMeromorphicWitness)
 111    (r : ℝ) (hr : 0 < r) (_hrw : r < w.radius) :
 112    ∃ cpd : ContinuousPhaseData,
 113      cpd.center = w.center ∧ cpd.radius = r ∧ cpd.charge = -w.order := by
 114  simpa using zpow_phase_charge w.center r hr w.order
 115