A clean constant bound for the p-series beyond exponent two

∑' m : ℕ, m ^ (-t) ≤ 2 for every real t ≥ 2. Mathlib supplies the exact value at the endpoint, ζ (2) = π ^ 2 / 6, and summability throughout t > 1, but no inequality valid across a range of exponents; that is what this file adds.

The bound is deliberately lossy. The supremum over t ≥ 2 is ζ (2) = 1.6449…, so 2 gives away about 18%. A round constant is the useful thing to expose: consumers carry it through chains of inequalities and none of them wants π in the goal.

Nothing here is specific to any application, and the file contains no number theory. The m = 0 term is 0, by the junk value of 0 ^ (-t).

Main results

• TauCeti.tsum_nat_rpow_neg_le_two — ∑' m : ℕ, m ^ (-t) ≤ 2 for 2 ≤ t.

theorem TauCeti.tsum_nat_rpow_neg_le_two {t : ℝ} (ht : 2 ≤ t) : ∑' (m : ℕ), ↑m ^ (-t) ≤ 2

The p-series over ℕ is at most 2 beyond exponent two. For 2 ≤ t, ∑' m : ℕ, m ^ (-t) ≤ 2, the case t = 2 being ζ(2) = π ^ 2 / 6 < 2. The m = 0 term is 0, by the junk value of 0 ^ (-t).