Theorems · Theorem · number theory

ZetaAsymptotics.termSum_of_lt

∀ (N : ℕ) {s : ℝ},
  1 < s →
    ZetaAsymptotics.termSum 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)

Defined in

Mathlib.NumberTheory.Harmonic.ZetaAsymp

Cited by

2 results in Mathlib

Foundations

Depth 271 from the axioms · uses propext, Classical.choice, Quot.sound