English
The residue of Λ at s = k is ε · g₀, i.e., (s − k) Λ(s) tends to ε g₀ as s → k with s ≠ k.
Русский
Резидуa Λ при s = k равна ε · g₀, то есть (s − k) Λ(s) стремится к ε g₀ при s → k, s ≠ k.
LaTeX
$$$\\displaystyle \\lim_{s \\to k,\\ s \\neq k} (s - k) \\Lambda(s) = \\varepsilon \\cdot g_0$$$
Lean4
/-- The residue of `Λ` at `s = k` is equal to `ε • g₀`. -/
theorem Λ_residue_k : Tendsto (fun s : ℂ ↦ (s - P.k) • P.Λ s) (𝓝[≠] P.k) (𝓝 (P.ε • P.g₀)) :=
by
simp_rw [Λ, smul_sub, (by simp : 𝓝 (P.ε • P.g₀) = 𝓝 (0 - 0 - -P.ε • P.g₀))]
refine ((Tendsto.sub ?_ ?_).mono_left nhdsWithin_le_nhds).sub ?_
· rw [(by rw [sub_self, zero_smul] : 𝓝 0 = 𝓝 ((P.k - P.k : ℂ) • P.Λ₀ P.k))]
apply ((continuous_sub_right _).smul P.differentiable_Λ₀.continuous).tendsto
· rw [(by rw [sub_self, zero_smul] : 𝓝 0 = 𝓝 ((P.k - P.k : ℂ) • (1 / P.k : ℂ) • P.f₀))]
refine (continuous_sub_right _).continuousAt.smul (ContinuousAt.smul ?_ continuousAt_const)
exact continuousAt_const.div continuousAt_id (ofReal_ne_zero.mpr P.hk.ne')
· refine (tendsto_const_nhds.mono_left nhdsWithin_le_nhds).congr' ?_
refine eventually_nhdsWithin_of_forall (fun s (hs : s ≠ P.k) ↦ ?_)
match_scalars
field_simp [sub_ne_zero.mpr hs.symm]
ring
