Haar Integrability Of Exponential Norm Decay

Proved

FunctionalInequalities.Probability.integrable_exp_sub_norm_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is a finite-dimensional Haar-integrability estimate for exponential norm decay.

Let $E$ be finite-dimensional with a real inner product and Borel measurable structure, let $dx$ be an additive Haar measure on $E$ , and let $c\in\mathbb R$ satisfy $c>0$ . For every $M\in\mathbb R$ ,

y\longmapsto\exp(M-c\|y\|)

is integrable with respect to $dx$ .

This supplies the integrable exponential envelope used in conjugate-mass estimates, including the zero-dimensional case.

Original Lean declaration header

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

theorem integrable_exp_sub_norm [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (dx : Measure E) [dx.IsAddHaarMeasure] {c : ℝ} (hc : 0 < c) (M : ℝ) :
    Integrable (fun y : E => Real.exp (M - c * ‖y‖)) dx

Module navigation

Module: Probability/MomentMeasure/ConjugateMass.

Next: limsup_density_legendre_le.

Source excerpt, lines 36–38 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_MomentMeasure_ConjugateMass

open MeasureTheory Filter Set
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]

Formal statement


theorem FunctionalInequalities.Probability.integrable_exp_sub_norm_readable [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (dx : Measure E) [dx.IsAddHaarMeasure] {c : ℝ} (hc : 0 < c) (M : ℝ) :
    Integrable (fun y : E => Real.exp (M - c * ‖y‖)) dx := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/MomentMeasure/ConjugateMass.lean#L34-L60 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.MomentMeasure.ConjugateMass`, declaration `FunctionalInequalities.Probability.integrable_exp_sub_norm`; the repository is private at upload time).

View graph