Tao Section 8: $\|\eta_1'\|_{L^\infty(\mathbb{R})} = 10$

Proved

TaoFivePrimes.eta1_lipschitz_ten

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

analytic-number-theorygoldbachnumber-theory

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

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

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

It is Lipschitz with constant

\|\eta_1'\|_{L^\infty(\mathbb R)}=10,

that is, $|\eta_1(s)-\eta_1(t)|\le 10|s-t|$ for all real $s,t$ .

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

Formalization Note Because $\eta_1$ has corners at $0.1,0.2,0.8,0.9$ , the sup-norm of its derivative is stated in the equivalent form of a Lipschitz bound with constant $10$ .

Preamble

import Mathlib
import Definitions.Def_TaoFivePrimes_RepresentationCount

open MeasureTheory

Formal statement

theorem TaoFivePrimes.eta1_lipschitz_ten : LipschitzWith 10 TaoFivePrimes.eta1 := 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.5)

View graph

Tao Section 8: ∥η1′∥L∞(R)=10\|\eta_1'\|_{L^\infty(\mathbb{R})} = 10∥η1′​∥L∞(R)​=10

Tao Section 8: $\|\eta_1'\|_{L^\infty(\mathbb{R})} = 10$