Tao Section 5: the integral test for the Type I block sum
ProvedTaoFivePrimes.typeI_block_sum_boundLet , and be reals, and let be a natural number with . Then
This is the block sum that appears when the Type I sum of the source's minor-arc theorem is cut into blocks of length : on the -th block the weight is bounded by its value at the left endpoint, and what remains is exactly the sum above, with the length of the divisor range. The bound is the integral test applied to , whose partial sums are up to the first term.
Deviation from the source The source's display asserts the same bound without the additive , namely . That cannot hold in general: the term alone is , so the claimed right-hand side is already exceeded whenever , that is whenever . For a concrete instance take , , so that : the left-hand side is while the source's right-hand side is . The additive above is what the integral test actually gives, and the source's downstream estimate has room for it in its remaining terms; the correction is recorded here rather than propagated silently.
Formalization Note The summation index runs over Finset.range (J+1), i.e. , and the hypothesis is what the source's condition on the block index gives. No lower bound on is assumed: the hypothesis on already forces , so the logarithm is taken at a value .
import Mathlib open Finset
theorem TaoFivePrimes.typeI_block_sum_bound (x q M : ℝ) (hx : 0 ≤ x) (hq : 0 < q)
(J : ℕ) (hJ : (J : ℝ) ≤ M / (2 * q) - 1 / 4) :
(∑ j ∈ Finset.range (J + 1), x / (2 * (j : ℝ) * q + q / 2))
≤ (x / (2 * q)) * (Real.log (2 * M / q + 4) + 4) := by sorry