Prove2Me

Square-summability of η+\eta_+ von Mangoldt coefficients

Proved
Helfgott.minorArcPlusCoefficients_norm_sq_summable

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

circle-methodgoldbachhelfgottsummable

Let x>0x>0 and write

cn=Λ(n) η+(nx)c_n=\Lambda(n)\,\eta_+\Bigl(\frac n x\Bigr)

for the full (untruncated) minor-arc coefficient sequence. The series

∑n=1∞∣cn∣2=∑n=1∞Λ(n)2η+(nx)2\sum_{n=1}^\infty |c_n|^2 =\sum_{n=1}^\infty \Lambda(n)^2\eta_+\Bigl(\frac n x\Bigr)^2

converges.

The bound ∣η+(t)∣≤1.079955|\eta_+(t)|\le 1.079955 alone is not enough, since ∑Λ(n)2\sum\Lambda(n)^2 diverges. Convergence follows from the Gaussian factor in the definition of η+\eta_+: after controlling the band-limited major kernel by an HH-dependent constant one has

∣η+(t)∣≤K t e−t2/2,\bigl|\eta_+(t)\bigr|\le K\,t\,e^{-t^2/2},

and the comparison Λ(n)≤log⁡n\Lambda(n)\le\log n then reduces the claim to a standard super-exponentially decaying series.

Preamble
import Definitions.Def_Helfgott_MinorArcData
open scoped BigOperators Classical
Formal statement
namespace Helfgott

theorem minorArcPlusCoefficients_norm_sq_summable (x : ℝ) (hx : 0 < x) :
    Summable (fun n : ℕ => ‖minorArcPlusCoefficients x n‖^2) := by
  sorry

end Helfgott
Source
Helfgott, The ternary Goldbach conjecture is true, arXiv:1312.7748v2, §1.3.2 (Plancherel energy of S_η) and definition of η₊ via band-limited major kernel × Gaussian; cf. also the absolute convergence lemma etaPlus_vonMangoldt_summable on the platform.

View graph