English
If g analytic at x and g(x) ≠ 0, trailingCoeff of a modification equals g(x) in nhdsNear x.
Русский
Если g аналитична в x и g(x) ≠ 0, trailing coefficient совпадает с g(x) в окрестности x.
LaTeX
$$$\\text{meromorphicTrailingCoeffAt}_f x = g x$ при $g(x) \\neq 0$ и $f$ близко к $(z-x)^n g(z)$.$$
Lean4
/-- Definition of the trailing coefficient in case where `f` is meromorphic and a presentation of the
form `f = (z - x) ^ order • g z` is given, with `g` analytic at `x`.
-/
theorem meromorphicTrailingCoeffAt_of_eq_nhdsNE (h₁g : AnalyticAt 𝕜 g x)
(h : f =ᶠ[𝓝[≠] x] fun z ↦ (z - x) ^ (meromorphicOrderAt f x).untop₀ • g z) : meromorphicTrailingCoeffAt f x = g x :=
by
have h₁f : MeromorphicAt f x := by
rw [MeromorphicAt.meromorphicAt_congr h]
fun_prop
by_cases h₃ : meromorphicOrderAt f x = ⊤
· simp only [h₃, WithTop.untop₀_top, zpow_zero, one_smul,
MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top] at ⊢ h
apply EventuallyEq.eq_of_nhds (f := 0)
rw [← ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE (by fun_prop) (by fun_prop)]
apply (h.symm.trans (meromorphicOrderAt_eq_top_iff.1 h₃)).symm
· unfold meromorphicTrailingCoeffAt
simp only [h₁f, reduceDIte, h₃, ne_eq]
obtain ⟨h'₁, h'₂, h'₃⟩ := ((meromorphicOrderAt_ne_top_iff h₁f).1 h₃).choose_spec
apply Filter.EventuallyEq.eq_of_nhds
rw [← h'₁.continuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE h₁g.continuousAt]
filter_upwards [h, h'₃, self_mem_nhdsWithin] with y h₁y h₂y h₃y
rw [← sub_eq_zero]
rwa [h₂y, ← sub_eq_zero, ← smul_sub, smul_eq_zero_iff_right] at h₁y
simp_all [zpow_ne_zero, sub_ne_zero]
