Pointwise $\eta_*$ bound on actual minor arcs

Proved

Helfgott.actual_minor_arc_etaStar_pointwise_upper

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

circle-methodgoldbachhelfgottminor-arcs

For every $x\ge49\cdot10^{25}$ and every frequency $\alpha$ outside the actual major arcs $\mathfrak M_{8,150000}(x)$ ,

\bigl|S_{\eta_*}(\alpha,x)\bigr|\le\frac{7x}{98}.

This is the pointwise minor-arc envelope at the trivial Chebyshev scale of actual_minor_arc_star_mass_sharp. Strengthening it on nested arcs is the analytic heart of Helfgott's minor-arc argument; the present node isolates that estimate for the prime-weighted mass reduction.

Preamble

import Definitions.Def_Helfgott_MinorArcData
open MeasureTheory
open scoped BigOperators Classical

Formal statement

namespace Helfgott

theorem actual_minor_arc_etaStar_pointwise_upper (x : ℝ)
    (hx : (49 : ℝ)*10^25 ≤ x) :
    ∀ α ∈ (majorArcs 8 150000 x)ᶜ,
      ‖coordinatedExpSum etaStar x α‖ ≤ (7 / 2 : ℝ) * (x / 49) := by
  sorry

end Helfgott

Source

Reduction child for Helfgott.actual_minor_arc_prime_weighted_upper. Scale matches actual_minor_arc_star_mass_sharp.

View graph

Pointwise η∗\eta_*η∗​ bound on actual minor arcs

Pointwise $\eta_*$ bound on actual minor arcs