theorem
exp_cauchy_schwarz_bound
{Ω : Type u_1}
[MeasurableSpace Ω]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(A B : Ω → ℝ)
(s : ℝ)
(hA_int : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (s * A ω)) μ)
(hB_int : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (-s * B ω)) μ)
:
Cauchy-Schwarz inequality for exponential expectations.
For random variables A, B and any real s, we have
𝔼[exp(s/2 · (A - B))] ≤ √(𝔼[exp(s·A)] · 𝔼[exp(-s·B)])
This follows from Hölder's inequality with p = q = 2 applied to
f = exp(s/2 · A) and g = exp(-s/2 · B), using the identities
f² = exp(s · A) and g² = exp(-s · B).