Tight $O(x)$ upper bound on $\eta_+$ coefficient energy

Open

Helfgott.minorArcPlusSquareEnergy_bound

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

circle-methodgoldbachhelfgottpossibly-false

Assume $x\ge 49\cdot 10^{25}$ and that

\sum_n\Bigl\|\Lambda(n)\eta_+\bigl(n/x\bigr)\Bigr\|^2

converges. The claim is that the sum is at most $(973913/3500000)\,x$ .

Analytically the Plancherel identity and the prime number theorem give

\sum_n\Lambda(n)^2\eta_+\bigl(n/x\bigr)^2\sim x\log x\int_{\mathbb R}\eta_+(u)^2\,du,

and the platform lemma etaPlus_regularity supplies $\int\eta_+^2\le 321/500$ , so the left-hand side is asymptotic to a positive multiple of $x\log x$ . For $x\ge 49\cdot 10^{25}$ one has $x\log x\gg (973913/3500000)\,x$ , so this tight $O(x)$ bound is expected to be false. It is isolated here so that it can be disproved (or replaced by a correct large-sieve bound on the minor-arc $L^2$ mass) without blocking the summable half of minorArcPlusSquareEnergy_le.

Preamble

import Definitions.Def_Helfgott_MinorArcData
open scoped BigOperators Classical

Formal statement

namespace Helfgott

theorem minorArcPlusSquareEnergy_bound (x : ℝ)
    (hx : (49 : ℝ)*10^25 ≤ x)
    (hsum : Summable (fun n : ℕ => ‖minorArcPlusCoefficients x n‖^2)) :
    (∑' n : ℕ, ‖minorArcPlusCoefficients x n‖^2) ≤
      (973913 / 3500000 : ℝ) * x := by
  sorry

end Helfgott

Source

Helfgott, arXiv:1312.7748v2, §1.3.2: |S|_2^2 ∼ x log x (not O(x)). The constant 973913/3500000 matches the platform formalization of actual_minor_arc_prime_L2_mass_upper, which likely confuses coefficient energy with the large-sieve minor-arc integral.

View graph

Tight O(x)O(x)O(x) upper bound on η+\eta_+η+​ coefficient energy

Tight $O(x)$ upper bound on $\eta_+$ coefficient energy