English
If x ∈ U, then the normal form on U and f agree on a punctured neighborhood of x.
Русский
Если x ∈ U, нормальная форма на U и f совпадают на пунктированной окрестности x.
LaTeX
$$$toMeromorphicNFOn\ f\ U =^{{\mathcal{N}_{\neq x}}}\ f$$$
Lean4
/-- The order of a meromorphic function `f` at a `z₀` is infinity iff `f` vanishes locally around
`z₀`. -/
theorem meromorphicOrderAt_eq_top_iff : meromorphicOrderAt f x = ⊤ ↔ ∀ᶠ z in 𝓝[≠] x, f z = 0 :=
by
by_cases hf : MeromorphicAt f x; swap
· simp only [hf, not_false_eq_true, meromorphicOrderAt_of_not_meromorphicAt, WithTop.zero_ne_top, false_iff]
contrapose! hf
exact (MeromorphicAt.const 0 x).congr (EventuallyEq.symm hf)
simp only [meromorphicOrderAt, hf, ↓reduceDIte, sub_eq_top_iff, ENat.map_eq_top_iff, WithTop.natCast_ne_top, or_false]
by_cases h : analyticOrderAt (fun z ↦ (z - x) ^ hf.choose • f z) x = ⊤
· simp only [h, eventually_nhdsWithin_iff, mem_compl_iff, mem_singleton_iff, true_iff]
rw [analyticOrderAt_eq_top] at h
filter_upwards [h] with z hf hz
rwa [smul_eq_zero_iff_right <| pow_ne_zero _ (sub_ne_zero.mpr hz)] at hf
· obtain ⟨m, hm⟩ := ENat.ne_top_iff_exists.mp h
simp only [← hm, ENat.coe_ne_top, false_iff]
contrapose! h
rw [analyticOrderAt_eq_top]
rw [← hf.choose_spec.frequently_eq_iff_eventually_eq analyticAt_const]
apply Eventually.frequently
filter_upwards [h] with z hfz
rw [hfz, smul_zero]
