English
The residue at s = 1 can be expressed via a limit of a Dirichlet-type sum: (s−1) ∑ 1/n^s tends to 1 as s→1 in Re(s) > 1, in complex form.
Русский
Резидуальный предел для (s−1) Σ 1/n^s выражает резидуа дзеты; т.е. (s−1) Σ n^{−s} → 1 при s→1 в области Re(s) > 1.
LaTeX
$$$\\\\lim_{s \\to 1, Re(s) > 1} (s-1) \\\\sum_{n=1}^{∞} n^{-s} = 1$$$
Lean4
/-- The residue of `ζ(s)` at `s = 1` is equal to 1, expressed using `tsum`. -/
theorem tendsto_sub_mul_tsum_nat_cpow :
Tendsto (fun s : ℂ ↦ (s - 1) * ∑' (n : ℕ), 1 / (n : ℂ) ^ s) (𝓝[{s | 1 < re s}] 1) (𝓝 1) :=
by
refine (tendsto_nhdsWithin_mono_left ?_ riemannZeta_residue_one).congr' ?_
· simp only [subset_compl_singleton_iff, mem_setOf_eq, one_re, not_lt, le_refl]
· filter_upwards [eventually_mem_nhdsWithin] with s hs using congr_arg _ <| zeta_eq_tsum_one_div_nat_cpow hs
