Tao Theorem 5.1, Type I half, as its proof gives it
ProvedTaoFivePrimes.theorem51_typeI_envelope_as_provedThe Type I half of Tao's Theorem 5.1, with the constants its proof gives. Let with , let with , and let with , and . Let be any complex coefficients with on the positive odd , and let . Then
These are the first two terms of Theorem 5.1 with the two changes the source's own Type I argument forces.
The factor 2. Each block is bounded by the odd-restricted Vinogradov lemma. That block has length exactly , so the lemma's prefactor is , giving with and . The source's display uses prefactor . Carrying the correct one doubles both the harmonic term and the block bookkeeping, and becomes .
The additive 4. The integral test compares a decreasing summand with the integral over the preceding block, which covers but not ; the uncovered term is . At , the sum is and the printed bound .
Neither change costs anything downstream: Theorem 1.3 still follows with its printed constants, at .
Formalization Note The Type I sum, the divisor set and the smoothed cutoff are the platform definitions imported from Def_TaoFivePrimes_Theorem51Sums.
import Mathlib import Definitions.Def_TaoFivePrimes_Theorem51Sums open Finset
theorem TaoFivePrimes.theorem51_typeI_envelope_as_proved
(x alpha beta : ℝ) (a : ℤ) (q : ℕ) (hq : 4 ≤ q)
(haq : Nat.Coprime a.natAbs q)
(halpha : 4 * alpha = (a : ℝ) / q + beta)
(hbeta : |beta| ≤ 1 / (q : ℝ) ^ 2)
(U V : ℝ) (hU40 : 40 ≤ U) (hV40 : 40 ≤ V) (hUx : U < x) (hVx : V < x)
(hUV : U * V ≤ x / 4) (hUV2 : x ≤ U * V ^ 2)
(c : ℕ → ℂ) (hc : ∀ d ∈ TaoFivePrimes.theorem51Divisors U V, ‖c d‖ ≤ 1) :
TaoFivePrimes.theorem51TypeI x alpha U V c ≤
(x / q) * Real.log x * (Real.log (2 * U * V / q + 4) + 4)
+ 1.78 * (U * V + (5 / 2) * q) * (8 + Real.log q) * Real.log (2 * x) := by sorry