English
A real-analytic variant: (s−1) ∑ 1/n^s tends to 1 as s → 1+ in the real line.
Русский
Аналог в вещественных переменных: (s−1) Σ n^{−s} → 1 при s → 1+, на вещественной оси.
LaTeX
$$$\\\\lim_{s \\to 1^+} (s-1) \\\\sum_{n=1}^{∞} n^{-s} = 1$$$
Lean4
/-- The residue of `ζ(s)` at `s = 1` is equal to 1 expressed using `tsum` and for a
real variable. -/
theorem tendsto_sub_mul_tsum_nat_rpow : Tendsto (fun s : ℝ ↦ (s - 1) * ∑' (n : ℕ), 1 / (n : ℝ) ^ s) (𝓝[>] 1) (𝓝 1) :=
by
rw [← tendsto_ofReal_iff, ofReal_one]
have : Tendsto (fun s : ℝ ↦ (s : ℂ)) (𝓝[>] 1) (𝓝[{s | 1 < re s}] 1) :=
continuous_ofReal.continuousWithinAt.tendsto_nhdsWithin (fun _ _ ↦ by simp_all)
apply (tendsto_sub_mul_tsum_nat_cpow.comp this).congr fun s ↦ ?_
simp only [one_div, Function.comp_apply, ofReal_mul, ofReal_sub, ofReal_one, ofReal_tsum, ofReal_inv,
ofReal_cpow (Nat.cast_nonneg _), ofReal_natCast]
