Integrability of $|S_p|^2$ on actual minor arcs

Proved

Helfgott.integrableOn_minor_arc_prime_square

by Ethan Cheung Wang · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

circle-methodhelfgottmeasure-theory

For every $x\ge49\cdot10^{25}$ , the squared modulus of the retained-prime exponential sum is Bochner-integrable on the actual minor arcs with respect to Haar measure on $\mathbb R/\mathbb Z$ . This is the $L^1$ membership needed to apply the elementary comparison $\int fg\le(\sup g)\int f$ in the prime-weighted minor-arc estimate; it follows from the $\ell^2$ finiteness of the prime coefficients (Parseval) together with the Gaussian decay of $\eta_+$ .

Preamble

import Definitions.Def_Helfgott_MinorArcData
open MeasureTheory
open scoped BigOperators Classical

Formal statement

namespace Helfgott

theorem integrableOn_minor_arc_prime_square (x : ℝ)
    (hx : (49 : ℝ)*10^25 ≤ x) :
    IntegrableOn (fun α : AddCircle (1 : ℝ) =>
      ‖expSum (minorArcPrimeCoefficients x) α‖^2)
      ((majorArcs 8 150000 x)ᶜ) AddCircle.haarAddCircle := by
  sorry

end Helfgott

Source

Integrability discharge for Helfgott.actual_minor_arc_prime_weighted_of_pointwise_L2.

View graph

Integrability of ∣Sp∣2|S_p|^2∣Sp​∣2 on actual minor arcs

Integrability of $|S_p|^2$ on actual minor arcs