Square-Integrable Functions Under Exponential Tilts

This theorem states that square-integrability is preserved as integrability under every exponential tilt.

Let $E$ be a real inner-product space, let $\mu$ be a finite measure on $E$ with all exponential moments, and let $G$ be a real normed space. If $g:E\to G$ belongs to $L^2(\mu)$, then for every $z\in E$,

The Lean statement uses MemLp g 2 μ and concludes Integrable g (expTilt μ z). This provides the integrability needed for tilt averages of square-integrable functions.

Original Lean declaration header

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

theorem integrable_expTilt_of_memLp
    (μ : Measure E) [IsFiniteMeasure μ]
    (hexp : ∀ r : ℝ, Integrable (fun x => Real.exp (r * ‖x‖)) μ) {g : E → G}
    (hg : MemLp g 2 μ) (z : E) : Integrable g (expTilt μ z)

Module navigation

Module: Analysis/BakryEmery/Tilt/SquareIntegrable.

Definition modules: Analysis/BakryEmery/Tilt/Basic.

Supporting theorems: integrable_exp_mul_norm_of_memLp.

Previous: exists_norm_coordTensor_taylorTensor_le · Next: taylorTensor_succ_of_eq_inner.

Source excerpt, lines 627–630 · Frozen source 408915f.