English
Let f be meromorphic in normal form at x. Then the order of f at x is zero if and only if f(x) ≠ 0.
Русский
Пусть f мероморфна в нормальной форме в точке x. Тогда порядок f в точке x равен нулю тогда, когда f(x) ≠ 0.
LaTeX
$$$MeromorphicNFAt\ (f\,x) \Rightarrow (meromorphicOrderAt\ (f)\ (x) = 0 \iff f(x) \neq 0)$$$
Lean4
/-- If `f` is meromorphic in normal form at `x`, then `f` has order zero iff it does not vanish at
`x`.
See `AnalyticAt.order_eq_zero_iff` for an analogous statement about analytic functions. -/
theorem meromorphicOrderAt_eq_zero_iff (hf : MeromorphicNFAt f x) : meromorphicOrderAt f x = 0 ↔ f x ≠ 0 :=
by
constructor
· intro h₁f
have h₂f := hf.meromorphicOrderAt_nonneg_iff_analyticAt.1 (le_of_eq h₁f.symm)
rw [← h₂f.analyticOrderAt_eq_zero, ← ENat.map_natCast_eq_zero (α := ℤ)]
rwa [h₂f.meromorphicOrderAt_eq] at h₁f
· intro h
rcases id hf with h₁ | ⟨n, g, h₁g, h₂g, h₃g⟩
· have := h₁.eq_of_nhds
tauto
· have : n = 0 := by
by_contra hContra
have := h₃g.eq_of_nhds
simp only [Pi.smul_apply', Pi.pow_apply, sub_self, zero_zpow n hContra, zero_smul] at this
tauto
simp only [this, zpow_zero] at h₃g
apply (meromorphicOrderAt_eq_int_iff hf.meromorphicAt).2
use g, h₁g, h₂g
simp only [zpow_zero]
exact h₃g.filter_mono nhdsWithin_le_nhds
