English
For a family X: ι → Ω → ℝ that is independent, and a family of parameters c: ι → ℝ≥0, the finite sum ∑ i∈s X_i has sub-Gaussian MGF with parameter ∑ i∈s c_i.
Русский
Для семейства случайных величин X_i, взаимно независимого, и параметров c_i, сумма по конечному подмножеству s имеет субгауссову MGФ с параметром суммы этих c_i.
LaTeX
$$$\mathrm{HasSubgaussianMGF}(X,c,\mu) \land \mathrm{iIndepFun}(X,\mu) \Rightarrow \mathrm{HasSubgaussianMGF}(\lambda i. X_i, \sum_i c_i)$$$
Lean4
theorem add_of_indepFun {Y : Ω → ℝ} {cX cY : ℝ≥0} (hX : HasSubgaussianMGF X cX μ) (hY : HasSubgaussianMGF Y cY μ)
(hindep : IndepFun X Y μ) : HasSubgaussianMGF (fun ω ↦ X ω + Y ω) (cX + cY) μ
where
integrable_exp_mul
t := by
simp_rw [mul_add, exp_add]
convert MemLp.integrable_mul (hX.memLp_exp_mul t 2) (hY.memLp_exp_mul t 2)
norm_cast
infer_instance
mgf_le
t := by
calc
mgf (X + Y) μ t
_ = mgf X μ t * mgf Y μ t := (hindep.mgf_add (hX.integrable_exp_mul t).1 (hY.integrable_exp_mul t).1)
_ ≤ exp (cX * t ^ 2 / 2) * exp (cY * t ^ 2 / 2) := by
gcongr
· exact mgf_nonneg
· exact hX.mgf_le t
· exact hY.mgf_le t
_ = exp ((cX + cY) * t ^ 2 / 2) := by rw [← exp_add]; congr; ring
