Prove2Me

The cutoff η1\eta_1 is nonnegative

Proved
TaoFivePrimes.eta1_nonneg

by marwahaha · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

circle-methodnumber-theory

The trapezoidal cutoff η1(t)=(1−10 dist(t,[1/5,4/5]))+\eta_1(t) = (1 - 10\,\mathrm{dist}(t,[1/5,4/5]))_+, used for the first two primes in Section 8, is nonnegative everywhere. Immediate from its definition as a maximum with zero. It is the companion to the nonnegativity of η0\eta_0, and together they give nonnegativity of every weight in the representation count of equation (8.10).

Preamble
import Mathlib
import Definitions.Def_TaoFivePrimes_RepresentationCount
open TaoFivePrimes
Formal statement
namespace TaoFivePrimes

theorem eta1_nonneg (t : ℝ) : 0 ≤ eta1 t := by
  sorry

end TaoFivePrimes
Source
Terence Tao, Every odd number greater than 1 is the sum of at most five primes, Mathematics of Computation 83 (2014), 997-1038, https://arxiv.org/abs/1201.6656, Section 8, the definition of eta_1 at the start of the section.

View graph