The L2 mass of the trapezoidal cutoff is 2/3
ProvedTaoFivePrimes.eta1_sq_integralThe trapezoidal cutoff of Section 8 has mass exactly :
Here , so is the trapezoid that equals on , falls linearly to over and over , and vanishes outside .
The computation. The plateau contributes . Each ramp contributes, by the substitution on ,
and the two ramps are symmetric about , so together they give . Hence
Why the exact value is wanted. TaoFivePrimes.S1_major_arc_L2_mass_corollary49_limit bounds the major-arc mass of below by , and the form the minor-arc argument consumes is TaoFivePrimes.S1_major_arc_L2_mass_626, namely . The two match precisely because
with a margin of about one part in a thousand. So is not merely a convenient value: any estimate of accurate to worse than would fail to bridge the two nodes, and the exact evaluation is what makes the chain close.
The same appears in TaoFivePrimes.eta_cutoff_model_mass and in TaoFivePrimes.eta1_quadratic_prime_mass, where the sifted prime sum weighted by is — the arithmetic factor is on average, so the whole constant comes from this integral.
Note that no smoothness is needed: is piecewise linear and compactly supported, so the integral is a finite sum of elementary pieces, and the only care required is in handling Metric.infDist to the interval on each of the five regions.
import Mathlib import Definitions.Def_TaoFivePrimes_ArcSplit open MeasureTheory
namespace TaoFivePrimes theorem eta1_sq_integral : (∫ t : ℝ, TaoFivePrimes.eta1 t ^ 2) = 2 / 3 := by sorry end TaoFivePrimes