Mollified Weak Laplacian Equation

Proved

FunctionalInequalities.KLS.LogConcave.integral_laplacian_mul_convolution_eq_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This lemma transfers a weak weighted Laplacian equation through convolution.

Let $V$ be finite-dimensional and complete, let $m$ be an additive Haar measure, let $W:V\to\mathbb R$ and $F:V\to V$ . Assume that every smooth compactly supported test function $f$ satisfies

\int (\Delta f)W\,dm =\int \langle\nabla f,WF\rangle\,dm+\int fW\,dm.

Let $\eta$ be a smooth bump equal to $1$ on the closed ball of radius $R+1$ , assume $\eta W$ and $(\eta W)F$ are integrable, and let $\phi$ be a normalized smooth bump with outer radius at most $1$ . For every smooth compactly supported $g$ supported in the closed ball of radius $R$ , the convolutions satisfy

\int (\Delta g)\,\bigl(\phi\ast(\eta W)\bigr)\,dm = \int \left\langle\nabla g,\phi\ast(\eta WF)\right\rangle\,dm +\int g\,\bigl(\phi\ast(\eta W)\bigr)\,dm.

The convolution is the measure-dependent normalized convolution represented by convolution and ContDiffBump.normed. This is a technical mollification identity.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.LogConcave. Shown in its original module context. Proof omitted.

private theorem integral_laplacian_mul_convolution_eq {W : V → ℝ} {F : V → V}
    (hW : ∀ f : V → ℝ, ContDiff ℝ ∞ f → HasCompactSupport f →
      ∫ x, Laplacian.laplacian f x * W x ∂m =
        ∫ x, ⟪gradient f x, W x • F x⟫ ∂m + ∫ x, f x * W x ∂m)
    {R : ℝ} (η : ContDiffBump (0 : V)) (hη : R + 1 ≤ η.rIn)
    (hw : Integrable (fun x => η x * W x) m) (hG : Integrable (fun x => (η x * W x) • F x) m)
    (φ : ContDiffBump (0 : V)) (hφ : φ.rOut ≤ 1) {g : V → ℝ} (hg : ContDiff ℝ ∞ g)
    (hgc : HasCompactSupport g) (hgR : tsupport g ⊆ closedBall 0 R) :
    ∫ x, Laplacian.laplacian g x *
        (φ.normed m ⋆[ContinuousLinearMap.lsmul ℝ ℝ, m] fun y => η y * W y) x ∂m =
      ∫ x, ⟪gradient g x,
          (φ.normed m ⋆[ContinuousLinearMap.lsmul ℝ ℝ, m] fun y => (η y * W y) • F y) x⟫ ∂m +
        ∫ x, g x * (φ.normed m ⋆[ContinuousLinearMap.lsmul ℝ ℝ, m] fun y => η y * W y) x ∂m

Module navigation

Module: KLS/LogConcave/HeatSemigroup/InteriorRegularity.

Supporting theorems: gradient_convolution, integral_inner_convolution_eq, laplacian_convolution.

Previous: norm_toLp_smul_gradient_le · Next: integral_laplacian_mul_tiltedDensity_mul.

Source excerpt, lines 245–257 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_InteriorRegularity

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

Formal statement


 theorem FunctionalInequalities.KLS.LogConcave.integral_laplacian_mul_convolution_eq_readable {W : V → ℝ} {F : V → V}
    (hW : ∀ f : V → ℝ, ContDiff ℝ ∞ f → HasCompactSupport f →
      ∫ x, Laplacian.laplacian f x * W x ∂m =
        ∫ x, ⟪gradient f x, W x • F x⟫ ∂m + ∫ x, f x * W x ∂m)
    {R : ℝ} (η : ContDiffBump (0 : V)) (hη : R + 1 ≤ η.rIn)
    (hw : Integrable (fun x => η x * W x) m) (hG : Integrable (fun x => (η x * W x) • F x) m)
    (φ : ContDiffBump (0 : V)) (hφ : φ.rOut ≤ 1) {g : V → ℝ} (hg : ContDiff ℝ ∞ g)
    (hgc : HasCompactSupport g) (hgR : tsupport g ⊆ closedBall 0 R) :
    ∫ x, Laplacian.laplacian g x *
        (φ.normed m ⋆[ContinuousLinearMap.lsmul ℝ ℝ, m] fun y => η y * W y) x ∂m =
      ∫ x, ⟪gradient g x,
          (φ.normed m ⋆[ContinuousLinearMap.lsmul ℝ ℝ, m] fun y => (η y * W y) • F y) x⟫ ∂m +
        ∫ x, g x * (φ.normed m ⋆[ContinuousLinearMap.lsmul ℝ ℝ, m] fun y => η y * W y) x ∂m := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/HeatSemigroup/InteriorRegularity.lean#L238-L335 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.HeatSemigroup.InteriorRegularity`, declaration `_private.FunctionalInequalities.KLS.LogConcave.HeatSemigroup.InteriorRegularity.0.FunctionalInequalities.KLS.LogConcave.integral_laplacian_mul_convolution_eq`; the repository is private at upload time).

View graph