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