Second derivative of the mollified logarithmic cutoff including jump terms

Proved

TaoFivePrimes.eta0_mollifier_second_derivative_identity

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

bounded-variationmollificationtao-five-primes

For any smooth compactly supported real mollifier $\varphi$ , the convolution $F=\eta_0*\varphi$ satisfies the exact formula

F''(x)=16\varphi(x-1/4)-16\varphi(x-1/2)+4\varphi(x-1)+\int_{1/2}^{1}\frac4{t^2}\varphi(x-t)\,dt-\int_{1/4}^{1/2}\frac4{t^2}\varphi(x-t)\,dt.

The three terms are the derivative jumps. Together with a nonnegative unit-mass mollifier this formula supplies the second-derivative mass bound48 required by the open fixed-support inward approximation theorem. The proof differentiates the smooth convolution and applies the proved weak second-derivative identity to the reflected translated mollifier. No positivity or normalization is needed for the identity itself.

Preamble

import Mathlib
import Definitions.Def_TaoFivePrimes_RepresentationCount
open MeasureTheory
open scoped Convolution

Formal statement

theorem TaoFivePrimes.eta0_mollifier_second_derivative_identity (φ : ℝ → ℝ)
    (hc : HasCompactSupport φ) (hs : ContDiff ℝ (⊤ : ℕ∞) φ) (x : ℝ) :
    deriv (deriv (TaoFivePrimes.eta0 ⋆ φ)) x =
      16 * φ (x-1/4) - 16 * φ (x-1/2) + 4 * φ (x-1) +
      (∫ t in (1/2:ℝ)..1, 4/t^2 * φ (x-t)) -
      (∫ t in (1/4:ℝ)..(1/2), 4/t^2 * φ (x-t)) := by sorry

Source

Tao arXiv1201.6656v4, distributional/mollification convention before (5.9)-(5.13), p26; explicit smoothing ingredient for eta0_smooth_inward_approximation and Proposition7.2. https://arxiv.org/pdf/1201.6656

View graph