English
If X and Y have sub-Gaussian MGFs with respect to κ and η respectively, then the sum X+Y has a sub-Gaussian MGF with respect to the combined kernel κ ⊗ η and a bound with (cX.sqrt + cY.sqrt)^2.
Русский
Если X и Y имеют подгауссов MGФ относительно κ и η, то сумма X+Y имеет MGФ относительно объединенного ядра κ ⊗ η и ограничение (cX.sqrt + cY.sqrt)^2.
LaTeX
$$HasSubgaussianMGF X cX κ ν → HasSubgaussianMGF Y cY η (ν ⊗ₘ κ) → HasSubgaussianMGF (λ ω, X ω.1 + Y ω.2) ( (cX.sqrt + cY.sqrt)^2 ) (κ ⊗ η) ν$$
Lean4
theorem add {Y : Ω → ℝ} {cX cY : ℝ≥0} (hX : HasSubgaussianMGF X cX κ ν) (hY : HasSubgaussianMGF Y cY κ ν) :
HasSubgaussianMGF (fun ω ↦ X ω + Y ω) ((cX.sqrt + cY.sqrt) ^ 2) κ ν :=
by
by_cases hX0 : cX = 0
· simp only [hX0, NNReal.sqrt_zero, zero_add, NNReal.sq_sqrt] at hX ⊢
refine hY.congr ?_
filter_upwards [ae_eq_zero_of_hasSubgaussianMGF_zero' hX] with ω hX0 using by simp [hX0]
by_cases hY0 : cY = 0
· simp only [hY0, NNReal.sqrt_zero, add_zero, NNReal.sq_sqrt] at hY ⊢
refine hX.congr ?_
filter_upwards [ae_eq_zero_of_hasSubgaussianMGF_zero' hY] with ω hY0 using by simp [hY0]
exact
{ 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 := by
let p := (cX.sqrt + cY.sqrt) / cX.sqrt
let q := (cX.sqrt + cY.sqrt) / cY.sqrt
filter_upwards [hX.mgf_le, hY.mgf_le, hX.ae_forall_memLp_exp_mul p, hY.ae_forall_memLp_exp_mul q] with ω' hmX
hmY hlX hlY t
calc
(κ ω')[fun ω ↦ exp (t * (X ω + Y ω))]
_ ≤
(κ ω')[fun ω ↦ exp (t * X ω) ^ (p : ℝ)] ^ (1 / (p : ℝ)) *
(κ ω')[fun ω ↦ exp (t * Y ω) ^ (q : ℝ)] ^ (1 / (q : ℝ)) :=
by
simp_rw [mul_add, exp_add]
apply integral_mul_le_Lp_mul_Lq_of_nonneg
· exact ⟨by simp [field, p, q], by positivity, by positivity⟩
· exact ae_of_all _ fun _ ↦ exp_nonneg _
· exact ae_of_all _ fun _ ↦ exp_nonneg _
· simpa using (hlX t)
· simpa using (hlY t)
_ ≤ exp (cX * (t * p) ^ 2 / 2) ^ (1 / (p : ℝ)) * exp (cY * (t * q) ^ 2 / 2) ^ (1 / (q : ℝ)) :=
by
simp_rw [← exp_mul _ p, ← exp_mul _ q, mul_right_comm t _ p, mul_right_comm t _ q]
gcongr
· exact hmX (t * p)
· exact hmY (t * q)
_ = exp ((cX.sqrt + cY.sqrt) ^ 2 * t ^ 2 / 2) :=
by
simp_rw [← exp_mul, ← exp_add]
simp only [NNReal.coe_div, NNReal.coe_add, coe_sqrt, one_div, inv_div, exp_eq_exp, p, q]
field_simp
linear_combination t ^ 2 * (-√↑cY * Real.sq_sqrt cX.coe_nonneg - √↑cX * Real.sq_sqrt cY.coe_nonneg) }
