Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

(8.18), Dirichlet regime: KT0/(4πx)<∥α∥<32/N0KT_0/(4\pi x) < \|\alpha\| < 32/N_0KT0​/(4πx)<∥α∥<32/N0​

Proved
TaoFivePrimes.minor_arc_Linfty_dirichlet

by marwahaha · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

circle-methodexponential-sumsgoldbachnumber-theory

Estimate (8.18) in the Dirichlet regime. This is the substantive regime of the L∞L^\inftyL∞ bound: α\alphaα is far enough from the origin that the archimedean model is useless, but not so far that the crude kernel bound suffices,

KT04πx  <  ∥α∥R/Z  <  32N0,\frac{KT_0}{4\pi x} \;<\; \|\alpha\|_{\mathbb R/\mathbb Z} \;<\; \frac{32}{N_0},4πxKT0​​<∥α∥R/Z​<N0​32​,

with K=1000K = 1000K=1000, T0=3.29×109T_0 = 3.29\times10^9T0​=3.29×109, N0=4×1014N_0 = 4\times10^{14}N0​=4×1014.

Why it holds, following the paper. Here one uses the trivial kernel bound ∣DN0/3(α)∣≤N0/3|D_{N_0/3}(\alpha)| \le N_0/3∣DN0​/3​(α)∣≤N0​/3 and reduces to the pure exponential sum estimate

∣Sη0,x/K♯(x/K,α)∣  ≤  0.05 xK.|S_{\eta_0,\sqrt{x/K}\sharp}(x/K,\alpha)| \;\le\; 0.05\,\frac{x}{K}.∣Sη0​,x/K​♯​(x/K,α)∣≤0.05Kx​.

Dirichlet approximation writes 4α=1/q+O∗(1/q2)4\alpha = 1/q + O^*(1/q^2)4α=1/q+O∗(1/q2) with 14α−1≤q≤14α\frac{1}{4\alpha} - 1 \le q \le \frac{1}{4\alpha}4α1​−1≤q≤4α1​, so the upper bound on ∥α∥\|\alpha\|∥α∥ forces q≥N0/128−1>3×1012q \ge N_0/128 - 1 > 3\times10^{12}q≥N0​/128−1>3×1012, and the lower bound forces q≤πx/(KT0)q \le \pi x/(KT_0)q≤πx/(KT0​). Theorem 1.3 then applies in one of three forms according to the size of qqq relative to y:=x/Ky := x/Ky:=x/K, each with room against the budget: the weakly minor case y2/3≤qy^{2/3} \le qy2/3≤q via refinement (1.12); the intermediate case y1/3≤q≤y2/3y^{1/3} \le q \le y^{2/3}y1/3≤q≤y2/3 via the main estimate (1.9), which the paper bounds by 0.0130.0130.013; and the strongly minor case q≤y1/3q \le y^{1/3}q≤y1/3 via refinement (1.10), which it bounds by 0.00020.00020.0002. The paper notes explicitly that the weakly minor case fails if (1.9) or (1.11) is used in place of (1.12).

Inputs. Theorem 1.3 in the forms (1.9), (1.10) and (1.12), the Dirichlet approximation, and the trivial kernel bound. Published statements of the three Theorem 1.3 forms are available as exp_sum_estimate, exp_sum_estimate_small_q and exp_sum_estimate_large_q_unit.

Formalization note. S0, DK and T0 are those of the published arc-split module. The lower endpoint is the upper endpoint of the weakly major regime and the upper endpoint is the lower endpoint of the crude regime, so the three regimes cover ∥α∥>T0/(3.6πx)\|\alpha\| > T_0/(3.6\pi x)∥α∥>T0​/(3.6πx) exactly.

Preamble
import Mathlib
import Definitions.Def_TaoFivePrimes_ArcSplit
open TaoFivePrimes
Formal statement
namespace TaoFivePrimes

theorem minor_arc_Linfty_dirichlet (x : ℕ)
    (h1 : 87 * 10 ^ 35 ≤ x) (h2 : (x : ℝ) ≤ Real.exp 3100)
    (α : AddCircle (1 : ℝ))
    (hlo : 1000 * T0 / (4 * Real.pi * x) < ‖α‖)
    (hhi : ‖α‖ < 32 / (4 * 10 ^ 14)) :
    ‖S0 x α‖ * ‖DK (4 * 10 ^ 14) α‖ ≤ 0.05 * x * ((4 * 10 ^ 14 / 3 : ℕ) : ℝ) / 1000 := by
  sorry

end TaoFivePrimes
Source
Terence Tao, Every odd number greater than 1 is the sum of at most five primes, Mathematics of Computation 83 (2014), 997-1038, https://arxiv.org/abs/1201.6656, Section 8, the three Dirichlet-approximation cases in the proof of (8.18), pp. 42-43; regime boundary moved from 20/N_0 to 32/N_0 and constant sharpened to 0.05 as in minor_arc_Linfty_corrected.

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me