$|S_{\eta_*}|\le$ star mass (triangle inequality)

Proved

Helfgott.coordinatedExpSum_etaStar_norm_le_starMass

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

circle-methodexponential-sumshelfgott

For every positive real $x$ and every frequency $\alpha$ on the unit circle,

\bigl|S_{\eta_*}(\alpha,x)\bigr|\le B(x)=\sum_{n\ge0}\Lambda(n)\eta_*(n/x).

This is the triangle inequality for the absolutely convergent exponential sum defining $S_{\eta_*}$ , using nonnegativity of $\Lambda\eta_*$ . Combined with actual_minor_arc_star_mass_sharp it yields the Chebyshev-scale pointwise minor-arc envelope.

Preamble

import Definitions.Def_Helfgott_MinorArcData
open MeasureTheory
open scoped BigOperators Classical

Formal statement

namespace Helfgott

theorem coordinatedExpSum_etaStar_norm_le_starMass (x : ℝ) (hx : 0 < x)
    (α : AddCircle (1 : ℝ)) :
    ‖coordinatedExpSum etaStar x α‖ ≤ minorArcStarMass x := by
  sorry

end Helfgott

Source

Reduction child for Helfgott.actual_minor_arc_etaStar_pointwise_upper via actual_minor_arc_star_mass_sharp.

View graph

∣Sη∗∣≤|S_{\eta_*}|\le∣Sη∗​​∣≤ star mass (triangle inequality)

$|S_{\eta_*}|\le$ star mass (triangle inequality)