Exponential Integrability of Linear Observables

Proved

FunctionalInequalities.Analysis.BakryEmery.inner_exp_weights_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is a weighted integrability consequence of one exponential norm moment.

Let $E$ be a finite-dimensional real inner-product space with Borel structure, let $\mu$ be a measure, and assume that for some $r\in\mathbb R$ ,

\int e^{r\|x\|}\,d\mu(x)<\infty.

For every $u\in E$ and every $t<r$ ,

\int e^{t\|x\|}\,|\langle u,x\rangle|\,d\mu(x)<\infty.

The strict inequality $t<r$ is essential to the stated conclusion. This lemma supplies integrability of linear observables needed for local cumulant and tilt calculations.

Original Lean declaration header

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

theorem inner_exp_weights {μ : Measure E} {r : ℝ}
    (hexp : Integrable (fun x => Real.exp (r * ‖x‖)) μ) (u : E) :
    ∀ t < r, Integrable (fun x => Real.exp (t * ‖x‖) * ‖⟪u, x⟫‖) μ

Module navigation

Module: Analysis/BakryEmery/Cumulant/Local.

Next: cumulant_three_eq_integral_of_integrable_exp.

Source excerpt, lines 82–84 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Cumulant_Local

open MeasureTheory Filter Topology
open scoped RealInnerProductSpace ContDiff
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]

Formal statement

theorem FunctionalInequalities.Analysis.BakryEmery.inner_exp_weights_readable {μ : Measure E} {r : ℝ}
    (hexp : Integrable (fun x => Real.exp (r * ‖x‖)) μ) (u : E) :
    ∀ t < r, Integrable (fun x => Real.exp (t * ‖x‖) * ‖⟪u, x⟫‖) μ := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/Cumulant/Local.lean#L82-L97 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.Cumulant.Local`, declaration `FunctionalInequalities.Analysis.BakryEmery.inner_exp_weights`; the repository is private at upload time).

View graph