integer_tail_tsum_le
plain-language theorem explainer
The bound asserts that for real α > 1 and natural N ≥ 1 the tail ∑_{n>N} n^{-α} is at most N^{1-α}/(α-1). Number theorists bounding prime-reciprocal tails inside the Riemann-hypothesis error budget cite it when discharging the PrimeTailBound predicate. The proof compares the decreasing function x^{-α} to its integral from N onward, first reducing the infinite sum to a finite sum via Summable.tsum_le_of_sum_le then invoking the antitone integral comparison AntitoneOn.sum_le_integral_Ico.
Claim. For real number $α > 1$ and natural number $N ≥ 1$, the tail sum satisfies $∑_{n > N} n^{-α} ≤ N^{1-α}/(α-1)$.
background
The module supplies explicit tail estimates for prime sums that appear in the attachment-with-margin error budget of the Riemann-hypothesis development. It records that ∑p p^{-α} converges for α > 1 and gives concrete upper bounds on the tail ∑{p>N} p^{-α} via partial summation and integral comparison. The present theorem supplies the integer analogue that is later compared to the prime tail. Upstream lemmas include antitoneOn_rpow_neg (which establishes that x ↦ x^{-α} is antitone on [1,∞) for α > 0) and summable_nat_rpow_neg_subtype (which guarantees summability of the restricted sequence). The integral evaluation integral_rpow_neg is taken from Mathlib and yields the exact antiderivative x^{1-α}/(1-α).
proof idea
The tactic proof first obtains positivity of α and defines f(x) = x^{-α}. It shows f is antitone on [N,∞) by monotonicity from antitoneOn_rpow_neg. Summability of the subtype sum is obtained from summable_nat_rpow_neg_subtype. Summable.tsum_le_of_sum_le reduces the claim to a finite-sum inequality over an arbitrary finite set s of indices > N. The proof constructs an upper index M ≥ N, shows the sum over s is bounded by the sum over Icc (N+1) M, then applies AntitoneOn.sum_le_integral_Ico to replace that sum by the integral from N to M of x^{-α}. The integral is evaluated by integral_rpow_neg and the resulting expression (N^{1-α} - M^{1-α})/(α-1) is bounded above by N^{1-α}/(α-1) using positivity of the missing term.
why it matters
This integer-tail bound is the direct predecessor of prime_tail_tsum_bound, which in turn discharges the PrimeTailBound hypothesis inside ErrorBudget. The module documentation states that these estimates instantiate the Christmas-route error budget decomposition referenced in Riemann-Christmas.tex. Within the Recognition framework the result supplies the concrete numerical control on prime tails needed to close the explicit error term in the prime-sum estimates that support the overall Riemann-hypothesis argument. It touches the open question of how tight the constant 1/(α-1) remains when the sum is restricted to primes rather than all integers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.