Prove2Me

The cutoff η0\eta_0 is nonnegative

Proved
TaoFivePrimes.eta0_nonneg

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

circle-methodnumber-theory

Tao's logarithmic cutoff η0(t)=4(log⁡2−∣log⁡2t∣)+\eta_0(t) = 4(\log 2 - |\log 2t|)_+, extended by zero to t≤0t \leq 0, is nonnegative everywhere. This is immediate from its definition as four times a maximum with zero, but it is worth having available: η0\eta_0 appears as a weight in the third prime sum of equation (8.10) and in the exponential sum Sη0,q0S_{\eta_0,q_0} of Theorem 1.3, and nonnegativity of the weights is what makes the representation count nonnegative and hence makes its positivity equivalent to the existence of a representation.

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

theorem eta0_nonneg (t : ℝ) : 0 ≤ eta0 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, equation (1.7).

View graph