Retained-prime square energy bound

Open

Helfgott.minorArcPrimeSquareEnergy_le

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

circle-methodhelfgottlarge-sieve

For every $x\ge49\cdot10^{25}$ , the retained-prime coefficient energy satisfies

S(x)=\sum_n|p_n|^2\le\frac{973913}{3500000}\,x,

where $p_n=\Lambda(n)\eta_+(n/x)$ for primes $n>\sqrt{x}$ and $0$ otherwise. By Parseval, the minor-arc $L^2$ mass of $S_p$ is at most $S(x)$ , so this energy bound implies actual_minor_arc_prime_L2_mass_upper.

Preamble

import Definitions.Def_Helfgott_MinorArcData
open MeasureTheory
open scoped BigOperators Classical

Formal statement

namespace Helfgott

theorem minorArcPrimeSquareEnergy_le (x : ℝ)
    (hx : (49 : ℝ)*10^25 ≤ x) :
    minorArcPrimeSquareEnergy x ≤ (973913 / 3500000 : ℝ) * x := by
  sorry

end Helfgott

Source

Energy input for Helfgott.actual_minor_arc_prime_L2_mass_upper via Parseval.

View graph