Existence of a Smooth-Gradient Local-Density Package

Proved

FunctionalInequalities.KLS.LogConcave.exists_smoothGradient_localDensity_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This auxiliary statement supplies a local-density package for a full-dimensional log-concave probability law.

Let $V$ be a finite-dimensional real inner product space with its Borel measurable structure and a second-countable topology. Let $m$ be an additive Haar measure on $V$ , and $\nu$ a probability measure. Assume:

$\nu$ is log-concave (KLS.LogConcave).
The interior of its measure support is nonempty: $\operatorname{int}(\operatorname{supp}\nu)\ne\varnothing$ .

Then the local-density structure is inhabited:

\operatorname{Nonempty}\bigl(\operatorname{Energy.SmoothGradient.LocalDensity}(\nu,m)\bigr).

The package provides an open full-measure region and density data, including positivity and local bounds for the reciprocal density, for use in smooth-core energy comparisons.

Formalization Note The conclusion is existence of the structure Energy.SmoothGradient.LocalDensity, not uniqueness or a canonical choice. Completeness is not an explicit hypothesis of this declaration.

Original Lean declaration header

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

theorem exists_smoothGradient_localDensity (hν : LogConcave ν)
    (hi : (interior (ν : Measure V).support).Nonempty) :
    Nonempty (Energy.SmoothGradient.LocalDensity ν m)

Module navigation

Module: KLS/LogConcave/WeightedGradient/Energy.

Definition modules: Probability/LogConcave, Energy/SmoothGradient/Core.

Source excerpt, lines 35–37 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_WeightedGradient_Energy

open MeasureTheory Filter Topology
universe u
variable {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
variable {ν : MeasureTheory.ProbabilityMeasure V} (m : MeasureTheory.Measure V) [m.IsAddHaarMeasure]
omit [CompleteSpace V]

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.exists_smoothGradient_localDensity_readable (hν : LogConcave ν)
    (hi : (interior (ν : Measure V).support).Nonempty) :
    Nonempty (Energy.SmoothGradient.LocalDensity ν m) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/WeightedGradient/Energy.lean#L32-L63 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.WeightedGradient.Energy`, declaration `FunctionalInequalities.KLS.LogConcave.exists_smoothGradient_localDensity`; the repository is private at upload time).

View graph