Full $\eta_+$ coefficient energy bound

Open

Helfgott.minorArcPlusSquareEnergy_le

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

analytic-number-theorygoldbachhelfgott

For every $x\ge 49\cdot 10^{25}$ , the full von Mangoldt– $\eta_+$ coefficient energy is summable and satisfies

\sum_{n=1}^\infty\bigl\|\Lambda(n)\eta_+(n/x)\bigr\|^2\le\frac{973913}{3500000}\,x.

The prime-truncated energy minorArcPrimeSquareEnergy is obtained by zeroing non-prime and $n\le\sqrt{x}$ terms, so it is at most this quantity.

Preamble

import Definitions.Def_Helfgott_MinorArcData
open MeasureTheory
open scoped BigOperators Classical

Formal statement

namespace Helfgott

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

end Helfgott

View graph

Full η+\eta_+η+​ coefficient energy bound

Full $\eta_+$ coefficient energy bound