Minor-arc $L^2$ mass $\le$ prime coefficient energy

Proved

Helfgott.minor_arc_prime_L2_le_energy

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

circle-methodhelfgottparseval

For every $x>0$ , the Haar integral of $|S_p|^2$ over the actual minor arcs is at most the full Parseval energy $\sum|p_n|^2$ . This is the Bessel/Plancherel comparison of a spectral subset against the complete orthonormal Fourier mass.

Preamble

import Definitions.Def_Helfgott_MinorArcData
open MeasureTheory
open scoped BigOperators Classical

Formal statement

namespace Helfgott

theorem minor_arc_prime_L2_le_energy (x : ℝ) (hx : 0 < x) :
    (∫ α in (majorArcs 8 150000 x)ᶜ,
      ‖expSum (minorArcPrimeCoefficients x) α‖^2
        ∂AddCircle.haarAddCircle) ≤ minorArcPrimeSquareEnergy x := by
  sorry

end Helfgott

Source

Parseval/Bessel step for Helfgott.actual_minor_arc_prime_L2_mass_upper.

View graph

Minor-arc L2L^2L2 mass ≤\le≤ prime coefficient energy

Minor-arc $L^2$ mass $\le$ prime coefficient energy