English
If X has a sub-Gaussian MGF and Y has a sub-Gaussian MGF with respect to a kernel η, then the composed kernel κ ∘ Prod with prodMkLeft preserves the sub-Gaussian MGFs under the product measure.
Русский
Если X и Y имеют подгауссов MGФ относительно соответствующих ядер, композиция ядра сохраняет это свойство.
LaTeX
$$HasSubgaussianMGF X cX κ ν → HasSubgaussianMGF Y cY η (κ ∘ₘ ν) → HasSubgaussianMGF (X+Y) (c) (κ ∘ Prod) ν$$
Lean4
/-- For `ν : Measure Ω'`, `κ : Kernel Ω' Ω` and `η : (Ω' × Ω) Ω''`, if a random variable `X : Ω → ℝ`
has a sub-Gaussian mgf with respect to `κ` and `ν` and another random variable `Y : Ω'' → ℝ` has
a sub-Gaussian mgf with respect to `η` and `ν ⊗ₘ κ : Measure (Ω' × Ω)`, then `X + Y` (random
variable on the measurable space `Ω × Ω''`) has a sub-Gaussian mgf with respect to
`κ ⊗ₖ η : Kernel Ω' (Ω × Ω'')` and `ν`. -/
theorem add_compProd {η : Kernel (Ω' × Ω) Ω''} [IsZeroOrMarkovKernel η] (hX : HasSubgaussianMGF X c κ ν)
(hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)) : HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ η) ν :=
by
by_cases hκ : IsSFiniteKernel κ
swap; · simp [hκ]
refine .of_rat (integrable_exp_add_compProd hX hY) fun q ↦ ?_
filter_upwards [hX.mgf_le, hX.ae_integrable_exp_mul q, Measure.ae_ae_of_ae_compProd hY.mgf_le,
Measure.ae_integrable_of_integrable_comp <| integrable_exp_add_compProd hX hY q] with ω' hX_mgf hX_int hY_mgf
h_int_mul
calc
mgf (fun p ↦ X p.1 + Y p.2) ((κ ⊗ₖ η) ω') q
_ = ∫ x, exp (q * X x) * ∫ y, exp (q * Y y) ∂(η (ω', x)) ∂(κ ω') :=
by
simp_rw [mgf, mul_add, exp_add] at h_int_mul ⊢
simp_rw [integral_compProd h_int_mul, integral_const_mul]
_ ≤ ∫ x, exp (q * X x) * exp (cY * q ^ 2 / 2) ∂(κ ω') :=
by
refine integral_mono_of_nonneg ?_ (hX_int.mul_const _) ?_
· exact ae_of_all _ fun ω ↦ mul_nonneg (by positivity) (integral_nonneg (fun _ ↦ by positivity))
· filter_upwards [all_ae_of hY_mgf q] with ω hY_mgf
gcongr
exact hY_mgf
_ ≤ exp (↑(c + cY) * q ^ 2 / 2) :=
by
rw [integral_mul_const, NNReal.coe_add, add_mul, add_div, exp_add]
gcongr
exact hX_mgf q
