English
If X has sub-Gaussian MGF under μ trim hm and Y is conditionally sub-Gaussian with respect to hm, then X+Y is sub-Gaussian with parameter cX+cY.
Русский
Если X субгауссово МGF относительно μ с усечением hm, а Y — условно субгауссов с параметром cY относительно hm, то X+Y субгауссов с параметром cX+cY.
LaTeX
$$$\mathrm{HasSubgaussianMGF}(X,cX,\mu\!\trim hm) \Rightarrow \mathrm{HasCondSubgaussianMGF}(m,hm,Y,cY,\mu) \Rightarrow \mathrm{HasSubgaussianMGF}(X+Y,cX+cY,\mu)$.$$
Lean4
protected theorem mgf_le_of_mem_Icc_of_integral_eq_zero [IsProbabilityMeasure μ] {a b t : ℝ} (hm : AEMeasurable X μ)
(hb : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc a b) (hc : μ[X] = 0) (ht : 0 < t) : mgf X μ t ≤ exp ((‖b - a‖₊ / 2) ^ 2 * t ^ 2 / 2) :=
by
have hi (u : ℝ) : Integrable (fun ω ↦ exp (u * X ω)) μ := integrable_exp_mul_of_mem_Icc hm hb
have hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ) := by simp [hi, integrableExpSet]
obtain ⟨u, h1, h2⟩ := exists_cgf_eq_iteratedDeriv_two_cgf_mul ht hc hs
rw [← exp_cgf (hi t), exp_le_exp, h2]
gcongr
calc
_ = Var[X; μ.tilted (u * X ·)] := by rw [← variance_tilted_mul (hs (Set.mem_Icc_of_Ioo h1))]
_ ≤ ((b - a) / 2) ^ 2 :=
by
convert variance_le_sq_of_bounded ((tilted_absolutelyContinuous μ (u * X ·)) hb) _
· exact isProbabilityMeasure_tilted (hi u)
· exact hm.mono_ac (tilted_absolutelyContinuous μ (u * X ·))
_ = (‖b - a‖₊ / 2) ^ 2 := by simp [field]
