Laplacian Commutation with Mollification

Proved

FunctionalInequalities.Analysis.Mollification.laplacian_convolution_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This states that mollification commutes with the Laplacian for smooth compactly supported scalar functions.

Let $V$ be a finite-dimensional real inner-product space, let $m$ be an additive Haar measure, and let $\varphi$ be a smooth bump centered at $0$ . If $g:V\to\mathbb{R}$ is smooth and compactly supported, then for every $x\in V$ ,

\Delta\bigl((\varphi_{\mathrm{normed}}\ast g)(x)\bigr) =\bigl(\varphi_{\mathrm{normed}}\ast\Delta g\bigr)(x).

Here $\Delta$ is Laplacian.laplacian. This provides the second-order analogue of the gradient commutation identity.

Original Lean declaration header

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

theorem laplacian_convolution {g : V → ℝ} (hg : ContDiff ℝ ∞ g) (hgc : HasCompactSupport g)
    (x : V) :
    Laplacian.laplacian (φ.normed m ⋆[ContinuousLinearMap.lsmul ℝ ℝ, m] g) x =
      (φ.normed m ⋆[ContinuousLinearMap.lsmul ℝ ℝ, m] Laplacian.laplacian g) x

Module navigation

Module: Analysis/Mollification/Basic.

Previous: gradient_convolution · Next: integral_fderiv_kernel_eq.

Source excerpt, lines 389–392 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Mollification_Basic

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 (φ : ContDiffBump (0 : V))

Formal statement


theorem FunctionalInequalities.Analysis.Mollification.laplacian_convolution_readable {g : V → ℝ} (hg : ContDiff ℝ ∞ g) (hgc : HasCompactSupport g)
    (x : V) :
    Laplacian.laplacian (φ.normed m ⋆[ContinuousLinearMap.lsmul ℝ ℝ, m] g) x =
      (φ.normed m ⋆[ContinuousLinearMap.lsmul ℝ ℝ, m] Laplacian.laplacian g) x := by sorry

Source

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

View graph