Full absolute convergence of actual principal zeta Goldbach weighted zero sums

Proved

Helfgott.actual_zeta_zero_strip_absolute_convergence

by raresbuhai · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

goldbachl-functionsmajor-arcszeros

Let $\eta$ be either actual Goldbach smoothing $\eta_+$ or $\eta_*$ , let $x>0$ , and let $\beta\in\mathbb R$ . Put $H(s)=(s-1)\zeta(s)$ with $H(1)=1$ . The complete weighted zero series in the strip is absolutely convergent:

\sum_{\substack{H(\rho)=0\\-1/2\le\Re\rho\le2}}\left|m_\rho x^\rho\mathcal M[\eta(t)e^{2\pi ix\beta t}](\rho)\right|<\infty.

Every zero and full positive analytic multiplicity is included. The norm series and complex weighted series both converge unconditionally. The pole at one is removed without adding a zero. This supplies order-independent principal zero sums for the Goldbach major arcs; numerical zero bounds remain separate.

Preamble

import Definitions.Def_Helfgott_Smoothings
import Definitions.Def_CircleMethod_char
import Mathlib.Analysis.MellinTransform
import Mathlib.NumberTheory.LSeries.DirichletContinuation
import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
import Mathlib.Analysis.Analytic.Order
open MeasureTheory Set Filter Complex
open scoped Topology

Formal statement

theorem Helfgott.actual_zeta_zero_strip_absolute_convergence (η : ℝ → ℝ) (hη : η=Helfgott.etaPlus ∨ η=Helfgott.etaStar) (x β : ℝ) (hx : 0 < x) :
    let H := DirichletCharacter.LFunctionTrivChar₁ 1
    let Z := {ρ : ℂ | -(1/2 : ℝ) ≤ ρ.re ∧ ρ.re ≤ 2 ∧ H ρ=0}
    let g : Z → ℂ := fun ρ => (analyticOrderNatAt H ρ : ℂ)*(x : ℂ)^(ρ : ℂ)*
      mellin (fun r : ℝ => (η r : ℂ)*CircleMethod.e (x*β*r)) ρ
    Summable (fun ρ : Z => ‖g ρ‖) ∧ Summable g := by sorry

Source

Helfgott, Major arcs for Goldbach’s problem, https://arxiv.org/abs/1305.2897 and https://arxiv.org/abs/1312.7748. Mathlib Fourier/Mellin and L-function contributors including David Loeffler; Jensen, analytic orders and divisors including Stefan Kebekus and contributors; gamma reflection, Euler inverse series, p-series and unconditional sum contributors. Complete original full strip-band multiplicity estimate and absolute convergence assembly. Written by Codex.

View graph