English
For real s > 1, lim_{s→1^+} (ζ(s) - 1/(s-1)) = γ.
Русский
Пусть s>1. Тогда предел ζ(s) - 1/(s-1) при s → 1^+ равен γ.
LaTeX
$$$$\\\\lim_{s \\to 1^+} \\,\\\\bigl(\\\\operatorname{riemannZeta}(s) - \\\\frac{1}{s-1}\\\\bigr) = \\\\gamma$$$$
Lean4
/-- First version of the limit formula, with a limit over real numbers tending to 1 from above. -/
theorem tendsto_riemannZeta_sub_one_div_nhds_right : Tendsto (fun s : ℝ ↦ riemannZeta s - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ) :=
by
suffices Tendsto (fun s : ℝ ↦ (∑' n : ℕ, 1 / (n + 1 : ℝ) ^ s) - 1 / (s - 1)) (𝓝[>] 1) (𝓝 γ)
by
apply ((Complex.continuous_ofReal.tendsto _).comp this).congr'
filter_upwards [self_mem_nhdsWithin] with s hs
simp only [Function.comp_apply, Complex.ofReal_sub, Complex.ofReal_div, Complex.ofReal_one, sub_left_inj,
Complex.ofReal_tsum]
rw [zeta_eq_tsum_one_div_nat_add_one_cpow (by simpa using hs)]
congr 1 with n
rw [Complex.ofReal_cpow (by positivity)]
norm_cast
suffices aux2 : Tendsto (fun s : ℝ ↦ (∑' n : ℕ, 1 / (n + 1 : ℝ) ^ s) - 1 / (s - 1)) (𝓝[>] 1) (𝓝 (1 - term_tsum 1))
by
have := term_tsum_one.tsum_eq
rw [← term_tsum, eq_sub_iff_add_eq, ← eq_sub_iff_add_eq'] at this
simpa only [this] using aux2
apply Tendsto.congr'
· filter_upwards [self_mem_nhdsWithin] with s hs using (zeta_limit_aux1 hs).symm
· apply tendsto_const_nhds.sub
rw [← one_mul (term_tsum 1)]
apply (tendsto_id.mono_left nhdsWithin_le_nhds).mul
have := continuousOn_term_tsum.continuousWithinAt left_mem_Ici
exact Tendsto.mono_left this (nhdsWithin_mono _ Ioi_subset_Ici_self)
