prime_tail_le_integer_tail
plain-language theorem explainer
The tail sum over primes p > N of p to the power -α is at most the tail sum over all integers n > N of n to the power -α, for any real α > 1. Number theorists deriving explicit estimates for prime zeta tails or error budgets in the Riemann hypothesis would cite this comparison to reduce prime sums to integer sums. The argument exhibits the natural inclusion of large primes into large naturals, verifies injectivity and nonnegativity, then invokes the general monotonicity of summable nonnegative functions under injective reindexing.
Claim. For real $α > 1$, $∑_{p prime, p > N} p^{-α} ≤ ∑_{n > N} n^{-α}$.
background
The module supplies explicit tail bounds on prime sums for the attachment-with-margin error budget in the Riemann hypothesis argument. It records that ∑p p^{-α} converges for α > 1, then derives concrete upper bounds on the tail ∑{p > N} p^{-α} via partial summation and comparison with integer tails. The local setting is the Christmas-route decomposition that discharges the PrimeTailBound predicate from ErrorBudget.lean using these estimates, referencing Rosser–Schoenfeld and Dusart. Upstream results include the definition of the prime set as {n | Nat.Prime n} and the summability of n ↦ n^{-α} on the subtype of naturals exceeding N.
proof idea
The proof defines f on the subtype {n : ℕ // N < n} by f n := (n : ℝ)^(-α), constructs the inclusion map i that forgets the primality witness, proves injectivity by subtype extensionality, records nonnegativity via rpow_neg_nonneg', obtains summability via summable_nat_rpow_neg_subtype, and concludes by applying tsum_comp_le_tsum_of_inj.
why it matters
This comparison is the opening step of the calculation in prime_tail_tsum_bound, which supplies the explicit bound N^{1-α}/(α-1) and thereby discharges PrimeTailBound in the error-budget decomposition. It fills the prime-tail-bound lemma referenced in Riemann-Christmas.tex and supports the attachment of margin to prime-sum tails. In the Recognition Science framework it contributes to the number-theoretic estimates needed for the forcing-chain instantiation of the Riemann hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.