Existence of an Exponential Norm Moment

Proved

FunctionalInequalities.KLS.BorelLogConcave.exists_integrable_exp_norm_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This establishes an exponential moment for a Borel log-concave probability law.

Let $V$ be a real normed space with Borel measurable structure, and let $\nu$ be a BorelLogConcave probability measure on $V$ . Then there exists $t>0$ such that

\int_V e^{t\lVert v\rVert}\,d\nu(v)<\infty.

Equivalently, the function $v\mapsto e^{t\lVert v\rVert}$ is integrable with respect to $\nu$ . No finite-dimensionality assumption appears in the Lean type beyond the stated typeclass assumptions. This supplies exponential integrability for later moment arguments.

Original Lean declaration header

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

theorem exists_integrable_exp_norm {ν : ProbabilityMeasure V}
    (hν : BorelLogConcave ν) :
    ∃ t : ℝ, 0 < t ∧ Integrable (fun v ↦ Real.exp (t * ‖v‖)) (ν : Measure V)

Module navigation

Module: KLS/LogConcave/Density/BorellRepresentation/Moments.

Definition modules: KLS/LogConcave/Borel.

Source excerpt, lines 112–114 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Density_BorellRepresentation_Moments

open MeasureTheory Set Topology Filter
variable {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V] [MeasurableSpace V] [BorelSpace V]
  [FiniteDimensional ℝ V]
omit [FiniteDimensional ℝ V]

Formal statement


theorem FunctionalInequalities.KLS.BorelLogConcave.exists_integrable_exp_norm_readable {ν : ProbabilityMeasure V}
    (hν : BorelLogConcave ν) :
    ∃ t : ℝ, 0 < t ∧ Integrable (fun v ↦ Real.exp (t * ‖v‖)) (ν : Measure V) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/Density/BorellRepresentation/Moments.lean#L108-L193 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.Density.BorellRepresentation.Moments`, declaration `FunctionalInequalities.KLS.BorelLogConcave.exists_integrable_exp_norm`; the repository is private at upload time).

View graph