English
Under standard conditions with finite measure, adding X with sub-Gaussian MGF cX to Y with conditional sub-Gaussian MGF cY yields X+Y with parameter cX+cY.
Русский
При стандартных условиях с конечной мерой сложение X и Y даёт субгауссовскую MGФ с параметром cX+cY.
LaTeX
$$$\mathrm{HasSubgaussianMGF}(X,cX,\mu) \Rightarrow \mathrm{HasCondSubgaussianMGF}(m,hm,Y,cY,\mu) \Rightarrow \mathrm{HasSubgaussianMGF}(X+Y,cX+cY,\mu)$$$
Lean4
/-- A corollary of Hoeffding's lemma for bounded random variables. -/
theorem hasSubgaussianMGF_of_mem_Icc [IsProbabilityMeasure μ] {a b : ℝ} (hm : AEMeasurable X μ)
(hb : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc a b) : HasSubgaussianMGF (fun ω ↦ X ω - μ[X]) ((‖b - a‖₊ / 2) ^ 2) μ :=
by
rw [← sub_sub_sub_cancel_right b a μ[X]]
apply hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero (hm.sub_const _)
· filter_upwards [hb] with ω hab using by simpa using hab
· simp [integral_sub (Integrable.of_mem_Icc a b hm hb) (integrable_const _)]
