Compactly supported smooth diffusion images

Definition

KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Range

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

functional-inequalitiesklskls-conjecturekls-modularletwin2026log-concavemodule-context

Let $V$ be a finite-dimensional real inner-product space with its Borel measurable structure, let $ν$ be a probability measure on $V$ , and let $U : V \to \mathbb{R}$ be $C^1$ . compactSmoothDiffusionImage hU is the subset of $L^2(ν)$ consisting of the toLp representatives of $-L f$ , where $f : V \to \mathbb{R}$ is smooth of class $C^\infty$ and compactly supported and $L$ is the weighted Laplacian determined by $U$ . The module supplies auxiliary range-density infrastructure for these images; the definition itself imposes no centering or operator-domain condition on an arbitrary $L^2$ element.

Original module imports

import FunctionalInequalities.KLS.LogConcave.HeatSemigroup.InteriorRegularity
import FunctionalInequalities.KLS.LogConcave.HeatSemigroup.Generator
import FunctionalInequalities.KLS.LogConcave.WeightedGradient.Kernel
import FunctionalInequalities.Analysis.Semigroup.Generated.Convergence
import FunctionalInequalities.L2.MeanVariance

Original declaration excerpt

Shown in the original module context.

def compactSmoothDiffusionImage {ν : ProbabilityMeasure V} {U : V → ℝ}
    (hU : ContDiff ℝ 1 U) : Set (Lp ℝ 2 (ν : Measure V)) :=
  {w | ∃ (f : V → ℝ) (hf : ContDiff ℝ ∞ f) (hc : HasCompactSupport f),
    w = (memLp_neg_weightedLaplacian (ν := ν) hU hf hc).toLp
      (fun x => -weightedLaplacian U f x)}

Module navigation

Direct project imports: KLS/LogConcave/HeatSemigroup/InteriorRegularity, KLS/LogConcave/HeatSemigroup/Generator, KLS/LogConcave/WeightedGradient/Kernel, Analysis/Semigroup/Generated/Convergence, L2/MeanVariance.

Theorems in source order:

centered_mem_closure_compactSmoothDiffusionImage

Project result: The KLS conjecture.

Original module · FunctionalInequalities.KLS.LogConcave.HeatSemigroup.Range · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_InteriorRegularity
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Generator
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_WeightedGradient_Kernel
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Semigroup_Generated_Convergence
import Definitions.Def_KLSModular_FunctionalInequalities_L2_MeanVariance

noncomputable section
open MeasureTheory Filter Topology Set InnerProductSpace
open FunctionalInequalities
open FunctionalInequalities.L2
open FunctionalInequalities.KLS.LogConcave
open FunctionalInequalities.Analysis.Semigroup
open FunctionalInequalities.Analysis.Semigroup.Generated
open FunctionalInequalities.Analysis.BakryEmery
open scoped ContDiff RealInnerProductSpace LinearPMap
namespace FunctionalInequalities
namespace KLS
namespace LogConcave
namespace HeatSemigroup
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
/-- The literal compactly supported smooth diffusion images used in the range-density statement. -/
def compactSmoothDiffusionImage {ν : ProbabilityMeasure V} {U : V → ℝ}
    (hU : ContDiff ℝ 1 U) : Set (Lp ℝ 2 (ν : Measure V)) :=
  {w | ∃ (f : V → ℝ) (hf : ContDiff ℝ ∞ f) (hc : HasCompactSupport f),
    w = (memLp_neg_weightedLaplacian (ν := ν) hU hf hc).toLp
      (fun x => -weightedLaplacian U f x)}
end HeatSemigroup
end LogConcave
end KLS
end FunctionalInequalities

Source

Source: Letwin, The KLS constant is O(log^(1/4) n) (arXiv:2607.24164v1), item LA6. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/HeatSemigroup/Range.lean#L37-L42 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.HeatSemigroup.Range`, definition bundle `KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Range`; the repository is private at upload time).

View graph