English
For analytic f at z0, the existence of a representation f(z) = (z−z0)^n g(z) with g analytic and nonzero at z0 is equivalent to having not f vanishing identically near z0.
Русский
Для аналитической функции в z0 существование выражения f(z) = (z−z0)^n g(z) с аналитическим не нулевым g эквивалентно тому, что не
f≡0 в окрестности z0.
LaTeX
$$$\text{AnalyticAt } f z0 \Rightarrow (\exists n,g, AnalyticAt g z0 \wedge g(z0) \neq 0 \wedge \forall z\approx z0, f(z)=(z-z0)^n g(z)) \iff \neg \forall z\approx z0, f(z)=0$$$
Lean4
/-- For a function `f` on `𝕜`, and `z₀ ∈ 𝕜`, there exists at most one `n` such that on a punctured
neighbourhood of `z₀` we have `f z = (z - z₀) ^ n • g z`, with `g` analytic and nonvanishing at
`z₀`. We formulate this with `n : ℤ`, and deduce the case `n : ℕ` later, for applications to
meromorphic functions. -/
theorem unique_eventuallyEq_zpow_smul_nonzero {m n : ℤ}
(hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ z in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z)
(hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ z in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z) : m = n :=
by
wlog h_le : n ≤ m generalizing m n
· exact ((this hn hm) (not_le.mp h_le).le).symm
let ⟨g, hg_an, _, hg_eq⟩ := hm
let ⟨j, hj_an, hj_ne, hj_eq⟩ := hn
contrapose! hj_ne
have : ∃ᶠ z in 𝓝[≠] z₀, j z = (z - z₀) ^ (m - n) • g z :=
by
apply Filter.Eventually.frequently
rw [eventually_nhdsWithin_iff] at hg_eq hj_eq ⊢
filter_upwards [hg_eq, hj_eq] with z hfz hfz' hz
rw [← add_sub_cancel_left n m, add_sub_assoc, zpow_add₀ <| sub_ne_zero.mpr hz, mul_smul, hfz' hz,
smul_right_inj <| zpow_ne_zero _ <| sub_ne_zero.mpr hz] at hfz
exact hfz hz
rw [frequently_eq_iff_eventually_eq hj_an] at this
· rw [EventuallyEq.eq_of_nhds this, sub_self, zero_zpow _ (sub_ne_zero.mpr hj_ne), zero_smul]
conv => enter [2, z, 1]; rw [← Int.toNat_sub_of_le h_le, zpow_natCast]
exact ((analyticAt_id.sub analyticAt_const).pow _).smul hg_an
