Prime-weighted minor-arc mass from pointwise $\times L^2$

Proved

Helfgott.actual_minor_arc_prime_weighted_of_pointwise_L2

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

circle-methodgoldbachhelfgottmeasure-theory

Let $x\ge49\cdot10^{25}$ . Suppose $|S_{\eta_*}(\alpha,x)|\le M$ for every actual minor-arc frequency $\alpha$ , and

\int_{\mathfrak M^{\mathsf c}}|S_p(\alpha)|^2\,d\alpha\le E.

If $ME\le0.973913\,x^2/49$ , then the prime-weighted minor-arc mass satisfies the same upper bound. The proof is the elementary comparison $\int f g\le(\sup g)\int f$ for nonnegative integrands on a finite measure space, followed by the numerical hypothesis on $ME$ .

Preamble

import Definitions.Def_Helfgott_MinorArcData
open MeasureTheory
open scoped BigOperators Classical

Formal statement

namespace Helfgott

theorem actual_minor_arc_prime_weighted_of_pointwise_L2 (x : ℝ)
    (hx : (49 : ℝ)*10^25 ≤ x) (M E : ℝ)
    (hpt : ∀ α ∈ (majorArcs 8 150000 x)ᶜ,
      ‖coordinatedExpSum etaStar x α‖ ≤ M)
    (hL2 : (∫ α in (majorArcs 8 150000 x)ᶜ,
      ‖expSum (minorArcPrimeCoefficients x) α‖^2
        ∂AddCircle.haarAddCircle) ≤ E)
    (hME : M * E ≤ (973913 / 1000000 : ℝ) * (x ^ 2 / 49)) :
    (∫ α in (majorArcs 8 150000 x)ᶜ,
      ‖expSum (minorArcPrimeCoefficients x) α‖^2 *
        ‖coordinatedExpSum etaStar x α‖
        ∂AddCircle.haarAddCircle) ≤ (973913 / 1000000 : ℝ) * (x ^ 2 / 49) := by
  sorry

end Helfgott

Source

Abstract Hölder/L∞×L² bridge for Helfgott.actual_minor_arc_prime_weighted_upper.

View graph

Prime-weighted minor-arc mass from pointwise ×L2\times L^2×L2

Prime-weighted minor-arc mass from pointwise $\times L^2$