Pointwise Squared Norm Bound for Mollification

Proved

FunctionalInequalities.Analysis.Mollification.enorm_convolution_sq_le_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the pointwise Cauchy–Schwarz estimate for convolution with a normalized smooth bump.

Let $V$ be a finite-dimensional real inner-product space, let $m$ be an additive Haar measure on $V$ , and let $E$ be a normed real vector space. Let $\varphi$ be a smooth bump centered at $0$ , and let $f:V\to E$ be almost everywhere strongly measurable with respect to $m$ . For every $x\in V$ ,

\left\|(\varphi_{\mathrm{normed}}\ast f)(x)\right\|_e^2 \le \int_V \operatorname{ofReal}(\varphi_{\mathrm{normed}}(t))\,\|f(x-t)\|_e^2\,dm(t).

The quantity $\|\cdot\|_e$ is the extended norm with values in $[0,\infty]$ . This pointwise estimate is the local ingredient for $L^2$ contraction bounds.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis.Mollification. Shown in its original module context. Proof omitted.

theorem enorm_convolution_sq_le {f : V → E} (hf : AEStronglyMeasurable f m) (x : V) :
    ‖(φ.normed m ⋆[ContinuousLinearMap.lsmul ℝ ℝ, m] f) x‖ₑ ^ 2 ≤
      ∫⁻ t, ENNReal.ofReal (φ.normed m t) * ‖f (x - t)‖ₑ ^ 2 ∂m

Module navigation

Module: Analysis/Mollification/Basic.

Next: lintegral_enorm_convolution_sq_le.

Source excerpt, lines 57–59 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Mollification_Basic

open MeasureTheory Filter Topology Metric InnerProductSpace
open scoped Convolution ContDiff ENNReal RealInnerProductSpace
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
  [MeasurableSpace V] [BorelSpace V] {m : MeasureTheory.Measure V} [m.IsAddHaarMeasure]
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
variable (φ : ContDiffBump (0 : V))

Formal statement


theorem FunctionalInequalities.Analysis.Mollification.enorm_convolution_sq_le_readable {f : V → E} (hf : AEStronglyMeasurable f m) (x : V) :
    ‖(φ.normed m ⋆[ContinuousLinearMap.lsmul ℝ ℝ, m] f) x‖ₑ ^ 2 ≤
      ∫⁻ t, ENNReal.ofReal (φ.normed m t) * ‖f (x - t)‖ₑ ^ 2 ∂m := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Mollification/Basic.lean#L56-L94 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Mollification.Basic`, declaration `FunctionalInequalities.Analysis.Mollification.enorm_convolution_sq_le`; the repository is private at upload time).

View graph