Tao Section 5: the divisors contribute to the Type I envelope
ProvedTaoFivePrimes.typeI_small_divisor_contributionLet , let be an integer, let satisfy with , and let . Then
with the convention that the summand equals where the sine vanishes.
This is the contribution of the small divisors to the Type I envelope in the source's minor-arc theorem. The point is the factor of two: applying the odd-restricted Vinogradov-type lemma directly to would give , but the weight is even in , so the same application to a symmetric range of length — still short enough for the lemma's block count to be — bounds twice the sum above by that same quantity.
Quoted input The Vinogradov-type lemma of the source (its Lemma 3.4, for the modulus and the fixed truncation parameters ) appears here as the hypothesis hvino; the odd-restricted form actually used is the source's Corollary 3.5, which is public and proved and is applied to it.
Formalization Note The divisor range is written as the odd integers of . The frequency is written rather than so as to match the shape in which Corollary 3.5 consumes it. At the zeros of the sine the summand is set to , which is the source's convention and the mathematically correct value of the minimum there; the ambient division convention would instead make the quotient .
import Mathlib open Finset
theorem TaoFivePrimes.typeI_small_divisor_contribution
(A B alpha beta : ℝ) (a : ℤ) (q : ℕ) (hq : 2 ≤ q)
(hA : 0 ≤ A) (hB : 0 ≤ B)
(halpha : 4 * alpha = (a : ℝ) / q + beta) (hbeta : |beta| ≤ 1 / (q : ℝ) ^ 2)
(hvino : ∀ (alpha' beta' theta' u v : ℝ) (a' : ℤ),
alpha' = (a' : ℝ) / q + beta' → |beta'| ≤ 1 / (q : ℝ) ^ 2 → u < v →
(∑ n ∈ Finset.Ioc ⌊u⌋ ⌊v⌋,
(if Real.sin (Real.pi * alpha' * (n : ℝ) + theta') = 0 then A
else min A (B / |Real.sin (Real.pi * alpha' * (n : ℝ) + theta')|)))
≤ ((⌊(v - u) / (q : ℝ)⌋ : ℤ) + 1)
* (2 * A + (2 / Real.pi) * B * (q : ℝ) * Real.log (4 * q))) :
(∑ d ∈ (Finset.Ioc (0 : ℤ) ⌊(q : ℝ) / 2⌋).filter (fun d : ℤ => Odd d),
(if Real.sin (Real.pi * (2 * alpha) * (d : ℝ)) = 0 then A
else min A (B / |Real.sin (Real.pi * (2 * alpha) * (d : ℝ))|)))
≤ A + (1 / Real.pi) * B * (q : ℝ) * Real.log (4 * q) := by sorry