Exponential Weighted Integrability of an $L^2$ Function

Proved

FunctionalInequalities.Analysis.BakryEmery.integrable_exp_mul_norm_of_memLp_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is an integrability lemma for square-integrable functions under exponential moment assumptions.

Let $E$ be a normed real space with a measurable Borel structure, let $\mu$ be a finite measure, and assume that every exponential norm weight is integrable:

\forall s\in\mathbb R, \quad \int e^{s\|x\|}\,d\mu(x)<\infty.

If $f:E\to\mathbb R$ belongs to $L^2(\mu)$ and $r\in\mathbb R$ , then

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

The hypothesis is MemLp f 2 μ; no inner-product, finite-dimensional, or completeness assumption is required. This result is used to control weighted tilt integrals.

Original Lean declaration header

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

theorem integrable_exp_mul_norm_of_memLp (μ : Measure E) [IsFiniteMeasure μ]
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) μ) {f : E → ℝ} (hf : MemLp f 2 μ)
    (r : ℝ) : Integrable (fun x => Real.exp (r * ‖x‖) * ‖f x‖) μ

Module navigation

Module: Analysis/BakryEmery/Tilt/SquareIntegrable.

Previous: iteratedFDeriv_integral_exp_inner_smul · Next: contDiff_tiltAverage_of_memLp.

Source excerpt, lines 253–255 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Tilt_SquareIntegrable

open MeasureTheory Filter Topology FunctionalInequalities.Analysis.Tensor
universe u
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
omit [CompleteSpace E]
omit [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]

Formal statement


theorem FunctionalInequalities.Analysis.BakryEmery.integrable_exp_mul_norm_of_memLp_readable (μ : Measure E) [IsFiniteMeasure μ]
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) μ) {f : E → ℝ} (hf : MemLp f 2 μ)
    (r : ℝ) : Integrable (fun x => Real.exp (r * ‖x‖) * ‖f x‖) μ := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/Tilt/SquareIntegrable.lean#L250-L277 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.Tilt.SquareIntegrable`, declaration `FunctionalInequalities.Analysis.BakryEmery.integrable_exp_mul_norm_of_memLp`; the repository is private at upload time).

View graph

Exponential Weighted Integrability of an L2L^2L2 Function

Exponential Weighted Integrability of an $L^2$ Function