English
For s > 1, term_tsum(s) equals 1/(s-1) minus ζ(s)/s.
Русский
Для s > 1 term_tsum(s) равно 1/(s-1) минус ζ(s)/s.
LaTeX
$$$$\\\\operatorname{term\\_tsum}(s) = \\\\frac{1}{s-1} - \\\\frac{\\\\zeta(s)}{s}$$$$
Lean4
/-- For `1 < s`, the topological sum of `ZetaAsymptotics.term (n + 1) s` over all `n : ℕ` is
`1 / (s - 1) - ζ s / s`.
-/
theorem term_tsum_of_lt {s : ℝ} (hs : 1 < s) : term_tsum s = (1 / (s - 1) - 1 / s * ∑' n : ℕ, 1 / (n + 1 : ℝ) ^ s) :=
by
apply HasSum.tsum_eq
rw [hasSum_iff_tendsto_nat_of_nonneg (fun n ↦ term_nonneg (n + 1) s)]
change Tendsto (fun N ↦ term_sum s N) atTop _
simp_rw [term_sum_of_lt _ hs]
apply Tendsto.sub
· rw [show 𝓝 (1 / (s - 1)) = 𝓝 (1 / (s - 1) - 1 / (s - 1) * 0) by simp]
simp_rw [mul_sub, mul_one]
refine tendsto_const_nhds.sub (Tendsto.const_mul _ ?_)
refine tendsto_const_nhds.div_atTop <| (tendsto_rpow_atTop (by linarith)).comp ?_
exact tendsto_atTop_add_const_right _ _ tendsto_natCast_atTop_atTop
· rw [← sub_zero (tsum _)]
apply (((Summable.hasSum ?_).tendsto_sum_nat).sub ?_).const_mul
· exact_mod_cast (summable_nat_add_iff 1).mpr (summable_one_div_nat_rpow.mpr hs)
· apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
· change Tendsto (fun n : ℕ ↦ (1 / ↑(n + 1) : ℝ) ^ (s - 1)) ..
rw [show 𝓝 (0 : ℝ) = 𝓝 (0 ^ (s - 1)) by rw [zero_rpow]; linarith]
refine Tendsto.rpow_const ?_ (Or.inr <| by linarith)
exact (tendsto_const_div_atTop_nhds_zero_nat _).comp (tendsto_add_atTop_nat _)
· intro n
positivity
· intro n
dsimp only
transitivity (n + 1) / (n + 1) ^ s
· gcongr
linarith
· apply le_of_eq
rw [rpow_sub_one, ← div_mul, div_one, mul_comm, one_div, inv_rpow, ← div_eq_mul_inv]
· norm_cast
all_goals positivity
