Prime-coefficient $L^2$ mass on actual minor arcs

Open

Helfgott.actual_minor_arc_prime_L2_mass_upper

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

circle-methodgoldbachhelfgottlarge-sieve

For every $x\ge49\cdot10^{25}$ , the retained-prime exponential sum $S_p$ obeys

\int_{\mathfrak M_{8,150000}(x)^{\mathsf c}}|S_p(\alpha)|^2\,d\alpha\le\frac{973913}{3500000}\,x.

Combined with the pointwise $\eta_*$ envelope $|S_{\eta_*}|\le7x/98$ , the product recovers the target prime-weighted minor-arc mass $\le0.973913\,x^2/49$ . The bound is the large-sieve / energy content of the minor arcs.

Preamble

import Definitions.Def_Helfgott_MinorArcData
open MeasureTheory
open scoped BigOperators Classical

Formal statement

namespace Helfgott

theorem actual_minor_arc_prime_L2_mass_upper (x : ℝ)
    (hx : (49 : ℝ)*10^25 ≤ x) :
    (∫ α in (majorArcs 8 150000 x)ᶜ,
      ‖expSum (minorArcPrimeCoefficients x) α‖^2
        ∂AddCircle.haarAddCircle) ≤ (973913 / 3500000 : ℝ) * x := by
  sorry

end Helfgott

Source

Reduction child for Helfgott.actual_minor_arc_prime_weighted_upper. Constant chosen so (7/2)*(x/49)*(973913/3500000)*x = (973913/1000000)*(x^2/49).

View graph

Prime-coefficient L2L^2L2 mass on actual minor arcs

Prime-coefficient $L^2$ mass on actual minor arcs