English
If f is meromorphic on U and x ∈ U, then on the ordinary neighborhood of x the global normal form equals the local normal form at x.
Русский
Если f мероморфна на U и x ∈ U, то в окрестности x глобальная нормальная форма равна локальной нормальной форме в x.
LaTeX
$$$toMeromorphicNFOn\ f\ U =^{{\mathcal{N}\ x}} toMeromorphicNFAt\ f\ x\ x$$
Lean4
/-- The order of a meromorphic function `f` at `z₀` equals an integer `n` iff `f` can locally be
written as `f z = (z - z₀) ^ n • g z`, where `g` is analytic and does not vanish at `z₀`. -/
theorem meromorphicOrderAt_eq_int_iff {n : ℤ} (hf : MeromorphicAt f x) :
meromorphicOrderAt f x = n ↔ ∃ g : 𝕜 → E, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ z in 𝓝[≠] x, f z = (z - x) ^ n • g z :=
by
simp only [meromorphicOrderAt, hf, ↓reduceDIte]
by_cases h : analyticOrderAt (fun z ↦ (z - x) ^ hf.choose • f z) x = ⊤
· rw [h, ENat.map_top, ← WithTop.coe_natCast, top_sub, eq_false_intro WithTop.top_ne_coe, false_iff]
rw [analyticOrderAt_eq_top] at h
refine fun ⟨g, hg_an, hg_ne, hg_eq⟩ ↦ hg_ne ?_
apply EventuallyEq.eq_of_nhds
rw [EventuallyEq, ← AnalyticAt.frequently_eq_iff_eventually_eq hg_an analyticAt_const]
apply Eventually.frequently
rw [eventually_nhdsWithin_iff] at hg_eq ⊢
filter_upwards [h, hg_eq] with z hfz hfz_eq hz
rwa [hfz_eq hz, ← mul_smul, smul_eq_zero_iff_right] at hfz
exact mul_ne_zero (pow_ne_zero _ (sub_ne_zero.mpr hz)) (zpow_ne_zero _ (sub_ne_zero.mpr hz))
· obtain ⟨m, h⟩ := ENat.ne_top_iff_exists.mp h
rw [← h, ENat.map_coe, ← WithTop.coe_natCast, ← coe_sub, WithTop.coe_inj]
obtain ⟨g, hg_an, hg_ne, hg_eq⟩ := hf.choose_spec.analyticOrderAt_eq_natCast.mp h.symm
replace hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ (↑m - ↑hf.choose : ℤ) • g z :=
by
rw [eventually_nhdsWithin_iff]
filter_upwards [hg_eq] with z hg_eq hz
rwa [← smul_right_inj <| zpow_ne_zero _ (sub_ne_zero.mpr hz), ← mul_smul, ← zpow_add₀ (sub_ne_zero.mpr hz), ←
add_sub_assoc, add_sub_cancel_left, zpow_natCast, zpow_natCast]
exact
⟨fun h ↦ ⟨g, hg_an, hg_ne, h ▸ hg_eq⟩, AnalyticAt.unique_eventuallyEq_zpow_smul_nonzero ⟨g, hg_an, hg_ne, hg_eq⟩⟩
