Smooth eta0 approximants with fixed support and controlled derivative masses

Proved

TaoFivePrimes.eta0_smooth_inward_approximation

by xuanji · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

bounded-variationmollificationtao-five-primes

The logarithmic triangular cutoff admits smooth, nonnegative approximants $w_n$ , all supported on the same interval $[1/4,1]$ , such that

\|w_n-\eta_0\|_\infty\le\frac1{n+1},\qquad \int w_n\le1,\qquad\int|w_n'|\le8\log2,\qquad\int|w_n''|\le48+\frac1{n+1}.

The second-derivative bound includes the jump mass of the first derivative. Keeping the support fixed is essential when applying Proposition 7.2 at the endpoint scale $y=4000$ or the endpoint phase bound: an ordinary convolution would enlarge the support and would not preserve those hypotheses. This statement is the controlled inward version of the paper's mollification convention.

Preamble

import Mathlib
import Definitions.Def_TaoFivePrimes_ArcSplit
import Definitions.Def_TaoFivePrimes_SmoothedExpSum

open MeasureTheory

Formal statement

theorem TaoFivePrimes.eta0_smooth_inward_approximation :
    ∃ w : ℕ → ℝ → ℝ, ∀ n : ℕ,
      ContDiff ℝ (⊤ : ℕ∞) (w n) ∧
      (∀ t, 0 ≤ w n t) ∧
      (∀ t, w n t ≠ 0 → t ∈ Set.Icc (1 / 4 : ℝ) 1) ∧
      (∫ t : ℝ, w n t) ≤ 1 ∧
      (∫ t : ℝ, |deriv (w n) t|) ≤ 8 * Real.log 2 ∧
      (∫ t : ℝ, |deriv (deriv (w n)) t|) ≤ 48 + 1 / ((n : ℝ) + 1) ∧
      (∀ t, |w n t - TaoFivePrimes.eta0 t| ≤ 1 / ((n : ℝ) + 1)) := by sorry

Source

T. Tao, arXiv:1201.6656v4, mollification/distributional convention preceding equations(5.9)-(5.13), printed p.26. Fixed-support version: contract η0 about5/8 by λ<1 before convolution with a nonnegative compactly supported smooth unit-mass mollifier; the masses are λ,≤8log2,≤48/λ, and λ→1. https://arxiv.org/pdf/1201.6656

View graph