zeta_limit_aux1 — Mathlib

English

For s > 1, sum_{n≥0} 1/(n+1)^s minus 1/(s-1) equals 1 - s·term_tsum(s).

Русский

Для s > 1 сумма_{n≥0} 1/(n+1)^s минус 1/(s-1) равна 1 - s·term_tsum(s).

LaTeX

$$$$\\\\left(\\\\sum_{n=0}^{\\\\infty} \\\\frac{1}{(n+1)^s}\\\\right) - \\\\frac{1}{s-1} = 1 - s \\\\cdot \\\\operatorname{term\\_tsum}(s)$$$$

Lean4

/-- Reformulation of `ZetaAsymptotics.term_tsum_of_lt` which is useful for some computations
below. -/
theorem zeta_limit_aux1 {s : ℝ} (hs : 1 < s) : (∑' n : ℕ, 1 / (n + 1 : ℝ) ^ s) - 1 / (s - 1) = 1 - s * term_tsum s :=
  by
  rw [term_tsum_of_lt hs]
  generalize (∑' n : ℕ, 1 / (n + 1 : ℝ) ^ s) = Z
  field_simp [(show s - 1 ≠ 0 by linarith)]
  ring_nf

Похожие утверждения