English
For N ∈ ℕ and s > 1, term_sum(s,N) equals a decomposition involving (s-1) and a partial sum of (n+1)^{-s}.
Русский
Для N ∈ ℕ и s > 1 term_sum(s,N) выражается через (s-1) и частичную сумму (n+1)^{-s}.
LaTeX
$$$$\\\\operatorname{term\\_sum}(s,N) = \\\\frac{1}{s-1}\\left(1 - \\frac{1}{(N+1)^{s-1}}\\\\right) - \\\\frac{1}{s}\\left( \\\\sum_{n=0}^{N-1} \\frac{1}{(n+1)^{s}} - \\frac{N}{(N+1)^{s}} \\\\right)$$$$
Lean4
theorem term_sum_of_lt (N : ℕ) {s : ℝ} (hs : 1 < s) :
term_sum s N =
1 / (s - 1) * (1 - 1 / (N + 1) ^ (s - 1)) -
1 / s * ((∑ n ∈ Finset.range N, 1 / (n + 1 : ℝ) ^ s) - N / (N + 1) ^ s) :=
by
simp only [term_sum]
conv => enter [1, 2, n]; rw [term_of_lt (by simp) hs]
rw [Finset.sum_sub_distrib]
congr 1
·
induction N with
| zero => simp
| succ N hN =>
rw [Finset.sum_range_succ, hN, Nat.cast_add_one]
ring_nf
· simp_rw [mul_comm (_ / _), ← mul_div_assoc, div_eq_mul_inv _ s, ← Finset.sum_mul, mul_one]
congr 1
induction N with
| zero => simp
| succ N hN =>
simp_rw [Finset.sum_range_succ, hN, Nat.cast_add_one, sub_eq_add_neg, add_assoc]
congr 1
ring_nf
