Prove2Me

Tao Section 8: ∥η1∥L2(R)=2/3\|\eta_1\|_{L^2(\mathbb{R})} = \sqrt{2/3}

Proved
TaoFivePrimes.eta1_L2_sq

by Hartmann_Psi · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

analytic-number-theorygoldbachnumber-theory

Throughout, η1\eta_1 is the symmetric trapezoidal cutoff of Section 8 of the source,

η1(t)  =  (1−10 dist⁡(t,[0.2,0.8]))+,\eta_1(t)\;=\;\bigl(1-10\,\operatorname{dist}(t,[0.2,0.8])\bigr)_{+},

which is supported in [0.1,0.9][0.1,0.9], equals 11 on [0.2,0.8][0.2,0.8], and rises and falls linearly with slope ±10\pm10 in between.

Its L2L^2 norm satisfies

∥η1∥L2(R)2=∫Rη1(t)2 dt=23,so ∥η1∥L2(R)=2/3.\|\eta_1\|_{L^2(\mathbb R)}^2=\int_{\mathbb R}\eta_1(t)^2\,dt=\frac23,\qquad\text{so } \|\eta_1\|_{L^2(\mathbb R)}=\sqrt{2/3}.

The source records this together with the other norms of η1\eta_1 for repeated use in Section 8, where they are what is checked against the hypotheses of Corollary 4.9 and against the L2L^2 estimates of the final argument.

Formalization Note The squared norm is stated, since that is the quantity that occurs in the estimates; the source records the norm itself.

Preamble
import Mathlib
import Definitions.Def_TaoFivePrimes_RepresentationCount

open MeasureTheory
Formal statement
theorem TaoFivePrimes.eta1_L2_sq : (∫ t : ℝ, TaoFivePrimes.eta1 t ^ 2) = 2/3 := by sorry
Source
Terence Tao, "Every odd number greater than 1 is the sum of at most five primes", Mathematics of Computation 83 (2014), 997-1038; arXiv:1201.6656, https://arxiv.org/abs/1201.6656, Section 8, equation (8.2)

View graph