Exponential-Moment Bounds

Jensen and logarithmic moment-generating-function bounds for real random variables.

Main definitions

This module introduces no new definitions.

Main results

• jensen_exp: Jensen's inequality for the exponential function.
• mean_le_log_mgf: an expectation bound through a positive exponential moment.
• integrable_exp_add_and_integral_le: combines exponential-moment bounds for two summands without requiring independence.

theorem LeanPool.jensen_exp {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} (hX_int : MeasureTheory.Integrable X μ) (hexpX_int : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (X ω)) μ) : Real.exp (∫ (ω : Ω), X ω ∂μ) ≤ ∫ (ω : Ω), Real.exp (X ω) ∂μ

Jensen's inequality for exp: exp(E[X]) ≤ E[exp(X)]. This uses ConvexOn.map_integral_le from Mathlib.Analysis.Convex.Integral.

theorem LeanPool.mean_le_log_mgf {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} (hX_int : MeasureTheory.Integrable X μ) {t : ℝ} (ht : 0 < t) (hexpX_int : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ) : ∫ (ω : Ω), X ω ∂μ ≤ 1 / t * Real.log (∫ (ω : Ω), Real.exp (t * X ω) ∂μ)

MGF bound: E[X] ≤ (1/t) · log E[exp(tX)] for t > 0. This follows from Jensen's inequality for the convex function exp.

theorem LeanPool.integrable_of_integrable_exp_all {Ω : Type u_1} [MeasurableSpace Ω] {Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} (h : ∀ (t : ℝ), MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * Y ω)) μ) : MeasureTheory.Integrable Y μ

Integrability of all real exponential moments implies integrability of the variable.

theorem LeanPool.exp_add_le_average_exp_two (a b : ℝ) : Real.exp (a + b) ≤ (Real.exp (2 * a) + Real.exp (2 * b)) / 2

Convexity bounds the exponential of a sum by the average of doubled exponentials.

theorem LeanPool.integrable_exp_add_and_integral_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {Y Z : Ω → ℝ} {l B : ℝ} (hY_ae : AEMeasurable Y μ) (hZ_ae : AEMeasurable Z μ) (hY_int : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (2 * l * Y ω)) μ) (hZ_int : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (2 * l * Z ω)) μ) (hY_le : ∫ (ω : Ω), Real.exp (2 * l * Y ω) ∂μ ≤ B) (hZ_le : ∫ (ω : Ω), Real.exp (2 * l * Z ω) ∂μ ≤ B) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (l * (Y ω + Z ω))) μ ∧ ∫ (ω : Ω), Real.exp (l * (Y ω + Z ω)) ∂μ ≤ B

Combine equal exponential-moment bounds for two summands.

This is the integral form of exp_add_le_average_exp_two: integrability and an upper bound at the doubled parameter for each summand give the same upper bound for their sum at the original parameter. No independence assumption is needed.