theorem
proved
tactic proof
local_meromorphic_factorization
show as:
view Lean formalization →
formal statement (Lean)
85theorem local_meromorphic_factorization
86 (f : ℂ → ℂ) (ρ : ℂ) (n : ℤ) (hf : MeromorphicAt f ρ)
87 (hn : meromorphicOrderAt f ρ = ↑n) :
88 ∃ w : LocalMeromorphicWitness, w.center = ρ ∧ w.order = n := by
proof body
Tactic-mode proof.
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