Energy bound from $L^\infty(\eta_+)$ on $n\le 2x$ plus Gaussian tail

Proved

Helfgott.minorArcPlusSquareEnergy_le_of_abs_support

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

circle-methodgoldbachhelfgott

Let $x\\ge 2$ . Split the Plancherel energy $\\sum_n\\Lambda(n)^2\\eta_+(n/x)^2$ into the range $n\\le 2x$ and the complementary tail. On the finite range the pointwise bound $|\\eta_+|\\le 1079955/1000000$ together with the Chebyshev-type estimate

\\sum_{n\\le 2x}\\Lambda(n)^2\\le(\\log 4+4)\\cdot(2x)\\log(2x+1)

(available on the platform as vonMangoldt_sq_le_const_mul_log) yields the displayed main term. The remaining sum is the genuine Gaussian tail of $\\eta_+$ for $n>2x$ .

This is a correct (if soft) $O(x\\log x)$ upper bound on the coefficient energy, in contrast to the false $O(x)$ claim in minorArcPlusSquareEnergy_bound.

Preamble

import Definitions.Def_Helfgott_MinorArcData
open scoped BigOperators Classical

Formal statement

namespace Helfgott

theorem minorArcPlusSquareEnergy_le_of_abs_support (x : ℝ) (hx : 2 ≤ x) :
    (∑' n : ℕ, ‖minorArcPlusCoefficients x n‖^2) ≤
      (Real.log 4 + 4) * (1079955 / 1000000 : ℝ) ^ 2 *
        (2 * x) * Real.log (2 * x + 1) +
      (∑' n : ℕ, if (n : ℝ) ≤ 2 * x then (0 : ℝ) else
        ‖minorArcPlusCoefficients x n‖^2) := by
  sorry

end Helfgott

Source

Helfgott arXiv:1312.7748v2 §1.3.2 (|S|_2^2 ∼ x log x); platform lemmas vonMangoldt_sq_le_const_mul_log and etaPlus_abs_le.

View graph

Energy bound from L∞(η+)L^\infty(\eta_+)L∞(η+​) on n≤2xn\le 2xn≤2x plus Gaussian tail

Energy bound from $L^\infty(\eta_+)$ on $n\le 2x$ plus Gaussian tail