Unit positive mollification preserves eta0 first variation bound

Proved

TaoFivePrimes.eta0_mollifier_first_variation_bound

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

bounded-variationmollificationtao-five-primes

For a smooth compactly supported nonnegative real mollifier $\varphi$ of integral one, the smoothed logarithmic cutoff satisfies

\int_{\mathbb R}|(\eta_0*\varphi)'(x)|\,dx\le8\log2.

Together with the second-variation bound48, this supplies controlled derivative masses for the fixed-support smooth approximants used to extend the positive-parameter Proposition7.2 estimate to the nonsmooth cutoff.

Preamble

import Mathlib
import Definitions.Def_TaoFivePrimes_RepresentationCount
open MeasureTheory
open scoped Convolution

Formal statement

theorem TaoFivePrimes.eta0_mollifier_first_variation_bound (φ : ℝ → ℝ)
    (hc : HasCompactSupport φ) (hs : ContDiff ℝ (⊤ : ℕ∞) φ)
    (hp : ∀ x, 0 ≤ φ x) (hm : (∫ x, φ x) = 1) :
    (∫ x, |deriv (TaoFivePrimes.eta0 ⋆ φ) x|) ≤ 8 * Real.log 2 := by sorry

Source

Tao arXiv1201.6656v4, (5.11) and mollification convention, p26; first-variation ingredient in eta0_smooth_inward_approximation. https://arxiv.org/pdf/1201.6656

View graph