Mollifier Bumps and Tilted Densities

Definition

KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_InteriorRegularity

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

Under the finite-dimensional real inner-product-space assumptions on $V$ , mollifier n is a smooth compactly supported bump centered at $0$ whose inner and outer radii are respectively $1/(2(n+1))$ and $1/(n+1)$ , for $n\in\mathbb{N}$ ; the Haar-measure assumptions are omitted from this definition. For a measurable space $V$ , tiltedDensity m U is the real-valued function $x\mapsto \frac{\exp(-U(x))}{\int \exp(-U(y))\,dm(y)}$ associated with a measure $m$ on $V$ and a potential $U:V\to\mathbb{R}$ , whenever the displayed denominator is meaningful. These are auxiliary definitions used by the surrounding interior-regularity development.

Original module imports

import FunctionalInequalities.KLS.LogConcave.HeatSemigroup.OperatorCore
import FunctionalInequalities.Analysis.Mollification.Basic

Original declaration excerpt

Shown in the original module context.

private def mollifier (n : ℕ) : ContDiffBump (0 : V) where
  rIn := 1 / (2 * ((n : ℝ) + 1))
  rOut := 1 / ((n : ℝ) + 1)
  rIn_pos := by positivity
  rIn_lt_rOut := by
    have ha : (0 : ℝ) < 1 / ((n : ℝ) + 1) := by positivity
    rw [show (1 : ℝ) / (2 * ((n : ℝ) + 1)) = (1 / ((n : ℝ) + 1)) / 2 by field_simp]
    exact half_lt_self ha

Module navigation

Direct project imports: KLS/LogConcave/HeatSemigroup/OperatorCore, Analysis/Mollification/Basic.

Theorems in source order:

Project result: The KLS conjecture.

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

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_OperatorCore
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Mollification_Basic

noncomputable section
open MeasureTheory Filter Topology Metric InnerProductSpace
open FunctionalInequalities.Analysis.Semigroup FunctionalInequalities.Analysis.BakryEmery
open scoped ContDiff RealInnerProductSpace Convolution ENNReal
namespace FunctionalInequalities
namespace KLS
namespace LogConcave
open Energy Energy.WeightedGradient
section Haar
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (m : Measure V) [m.IsAddHaarMeasure]
omit [CompleteSpace V] [MeasurableSpace V] [BorelSpace V] [m.IsAddHaarMeasure] in
/-- The standard mollifier sequence: bumps of radii `1/(2(n+1)) < 1/(n+1)`. -/
 def mollifier (n : ℕ) : ContDiffBump (0 : V) where
  rIn := 1 / (2 * ((n : ℝ) + 1))
  rOut := 1 / ((n : ℝ) + 1)
  rIn_pos := by positivity
  rIn_lt_rOut := by
    have ha : (0 : ℝ) < 1 / ((n : ℝ) + 1) := by positivity
    rw [show (1 : ℝ) / (2 * ((n : ℝ) + 1)) = (1 / ((n : ℝ) + 1)) / 2 by field_simp]
    exact half_lt_self ha
end Haar
section Density
variable {V : Type*} [MeasurableSpace V] {ν : ProbabilityMeasure V} (m : Measure V) {U : V → ℝ}
/-- The normalised density `exp (-U) / ∫ exp (-U) dm` of `m.tilted (-U)`. -/
 def tiltedDensity (m : Measure V) (U : V → ℝ) (x : V) : ℝ :=
  Real.exp ((-U) x) / ∫ y, Real.exp ((-U) y) ∂m
end Density
end LogConcave
end KLS
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/HeatSemigroup/InteriorRegularity.lean#L116-L345 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.HeatSemigroup.InteriorRegularity`, definition bundle `KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_InteriorRegularity`; the repository is private at upload time).

View graph