The Dirichlet kernel is near-maximal on the strongly major arc

Proved

TaoFivePrimes.norm_DK_ge_major_arc

by cm_beta · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisexponential-sumsnumber-theory

On the strongly major arc the Dirichlet-type kernel is essentially at its trivial maximum:

\lVert D_{H/3}(\alpha)\rVert \;\ge\; 0.98\,\Bigl\lfloor \tfrac{H}{3}\Bigr\rfloor \qquad\text{for } \lVert\alpha\rVert \le \frac{T_0}{3.6\pi x},\quad H = 4\cdot10^{14},\ x \ge 87\cdot10^{35}.

Here $D_{H/3}(\alpha) = \sum_{1 \le n \le H/3} e(n\alpha)$ and $T_0 = 3.29\cdot10^{9}$ .

Why it is true with room to spare. On the major arc $\lVert\alpha\rVert \le T_0/(3.6\pi x) \le 3.29\cdot10^{9}/(3.6\pi\cdot 8.7\cdot10^{36}) < 3.4\cdot10^{-29}$ , so for every $n \le \lfloor H/3\rfloor < 1.34\cdot10^{14}$ the phase satisfies $\lVert n\alpha\rVert < 4.5\cdot10^{-15}$ . Every term of the sum therefore lies within $3\cdot10^{-14}$ of $1$ , and

\lVert D_{H/3}(\alpha)\rVert \;\ge\; \Bigl\lfloor \tfrac{H}{3}\Bigr\rfloor\bigl(1 - 3\cdot10^{-14}\bigr).

The constant $0.98$ is thus enormously generous; it is stated rather than something sharper only because that is all the application needs. A proof can take the real part of each term and use $\cos t \ge 1 - t^2/2$ , or bound the deviation by $\sum_n \lVert e(n\alpha) - 1\rVert \le 2\pi\sum_n n\lVert\alpha\rVert$ .

Why $0.98$ and not less. The statement is the missing lower-bound companion to the trivial upper bound TaoFivePrimes.norm_DK_le and to TaoFivePrimes.norm_DK_le_inv_three_small, and it is what lets the minor-arc mean square be computed as full circle minus major arc:

\int_{\text{minor}} \lVert S_1\rVert^2\lVert D_K\rVert^2 \;=\; \int_{\mathbb{R}/\mathbb{Z}} - \int_{\text{major}} \;\le\; 8.001\,\lfloor H/3\rfloor^2 x \;-\; (0.98)^2\lfloor H/3\rfloor^2\cdot 0.626\,x \;=\; 7.4\,\lfloor H/3\rfloor^2 x .

Since $(0.98)^2\cdot 0.626 = 0.6012$ and $8.001 - 0.601 = 7.4$ , the constant $0.98$ is exactly what turns minor_arc_L2_full_circle_8001 and S1_major_arc_L2_mass_626 into minor_arc_L2_corrected. Anything above $0.9797$ would do; $0.98$ is the round value that works.

Note the hypothesis $x \ge 87\cdot10^{35}$ is used only to make the arc small; no upper bound on $x$ is needed, since shrinking the arc only helps.

Preamble

import Mathlib
import Definitions.Def_TaoFivePrimes_ArcSplit

open MeasureTheory

Formal statement

namespace TaoFivePrimes

theorem norm_DK_ge_major_arc (x : ℕ) (h1 : 87 * 10 ^ 35 ≤ x)
    (α : AddCircle (1 : ℝ)) (hα : α ∈ majorArc x) :
    0.98 * ((4 * 10 ^ 14 / 3 : ℕ) : ℝ) ≤ ‖DK (4 * 10 ^ 14) α‖ := by sorry

end TaoFivePrimes

Source

Terence Tao, Every odd number greater than 1 is the sum of at most five primes, arXiv:1201.6656, Section 8 (the strongly major arc of Proposition 8.3 and the Dirichlet-type kernel of equation (8.11)).

View graph