English
If f is meromorphic at x, then the trailing coefficient at x is the limit of the scaled function (y − x)^{−(order at x for f).untop₀} · f(y) as y tends to x through points y ≠ x.
Русский
Если f мероморфна в точке x, то хвостовой коэффициент в x равен пределy масштаированной функции (y − x)^{−(порядок в x)} · f(y) при приближении y к x через точки y ≠ x.
LaTeX
$$$$\lim_{y \to x,\; y \neq x} (y - x)^{-(\mathrm{meromorphicOrderAt}(f,x)).untop_0} \cdot f(y) = \mathrm{meromorphicTrailingCoeffAt}(f,x).$$$$
Lean4
/-- If `f` is meromorphic at `x`, then the trailing coefficient of `f` at `x` is the limit of the
function `(· - x) ^ (-order) • f`.
-/
theorem tendsto_nhds_meromorphicTrailingCoeffAt (h : MeromorphicAt f x) :
Tendsto ((· - x) ^ (-(meromorphicOrderAt f x).untop₀) • f) (𝓝[≠] x) (𝓝 (meromorphicTrailingCoeffAt f x)) :=
by
by_cases h₂ : meromorphicOrderAt f x = ⊤
· simp_all only [WithTop.untop₀_top, neg_zero, zpow_zero, one_smul, meromorphicTrailingCoeffAt_of_order_eq_top]
apply Tendsto.congr' (f₁ := 0)
· filter_upwards [meromorphicOrderAt_eq_top_iff.1 h₂] with y hy
simp_all
· apply Tendsto.congr' (f₁ := 0) (by rfl) continuousWithinAt_const.tendsto
obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_ne_top_iff h).1 h₂
apply Tendsto.congr' (f₁ := g)
· filter_upwards [h₃g, self_mem_nhdsWithin] with y h₁y h₂y
rw [zpow_neg, Pi.smul_apply', Pi.inv_apply, Pi.pow_apply, h₁y, ← smul_assoc, smul_eq_mul, ← zpow_neg, ← zpow_add',
neg_add_cancel, zpow_zero, one_smul]
left
simp_all [sub_ne_zero]
· rw [h₁g.meromorphicTrailingCoeffAt_of_eq_nhdsNE h₃g]
apply h₁g.continuousAt.continuousWithinAt
