English
The normal-form operator equals the original function if and only if the function is meromorphic in normal form at x.
Русский
Оператор нормальной формы равен исходной функции тогда и только тогда, когда функция мероморфна в нормальной форме в x.
LaTeX
$$$toMeromorphicNFAt\ f\ x = f \iff MeromorphicNFAt\ f\ x$$$
Lean4
/-- If `f` has normal form at `x`, then `f` equals `f.toNF`. -/
@[simp]
theorem toMeromorphicNFAt_eq_self : toMeromorphicNFAt f x = f ↔ MeromorphicNFAt f x
where
mp
hf := by
rw [hf.symm]
exact meromorphicNFAt_toMeromorphicNFAt
mpr
hf := by
funext z
by_cases hz : z = x
· rw [hz]
simp only [toMeromorphicNFAt, hf.meromorphicAt, WithTop.coe_zero, ne_eq]
have h₀f := hf
rcases hf with h₁f | h₁f
· simpa [meromorphicOrderAt_eq_top_iff.2 (h₁f.filter_mono nhdsWithin_le_nhds)] using h₁f.eq_of_nhds.symm
· obtain ⟨n, g, h₁g, h₂g, h₃g⟩ := h₁f
rw [Filter.EventuallyEq.eq_of_nhds h₃g]
have : meromorphicOrderAt f x = n :=
by
rw [meromorphicOrderAt_eq_int_iff h₀f.meromorphicAt]
use g, h₁g, h₂g
exact eventually_nhdsWithin_of_eventually_nhds h₃g
by_cases h₃f : meromorphicOrderAt f x = 0
· simp only [Pi.smul_apply', Pi.pow_apply, sub_self, h₃f, ↓reduceDIte]
have hn : n = (0 : ℤ) := by
rw [h₃f] at this
exact WithTop.coe_eq_zero.mp this.symm
simp_rw [hn]
simp only [zpow_zero, one_smul]
have : g =ᶠ[𝓝 x] Classical.choose ((meromorphicOrderAt_eq_int_iff h₀f.meromorphicAt).1 h₃f) :=
by
obtain ⟨h₀, h₁, h₂⟩ := Classical.choose_spec ((meromorphicOrderAt_eq_int_iff h₀f.meromorphicAt).1 h₃f)
rw [← h₁g.continuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE h₀.continuousAt]
rw [hn] at h₃g
simp only [zpow_zero, one_smul, ne_eq] at h₃g h₂
exact (h₃g.filter_mono nhdsWithin_le_nhds).symm.trans h₂
simp only [Function.update_self]
exact Filter.EventuallyEq.eq_of_nhds this.symm
· rw [eq_comm]
simp only [Pi.smul_apply', Pi.pow_apply, sub_self, h₃f, ↓reduceDIte, smul_eq_zero, Function.update_self,
smul_eq_zero]
left
apply zero_zpow n
by_contra hn
rw [hn] at this
tauto
· exact (hf.meromorphicAt.eqOn_compl_singleton_toMeromorphicNFAt hz).symm
