English
If X has a sub-Gaussian MGF with κ and ν, and Y with η and κ ∘ₘ ν, then the product kernel κ ⊗ₖ prodMkLeft Ω' η preserves the sub-Gaussian MGF for the sum X p.1 + Y p.2.
Русский
Если X имеет MGФ относительно κ и ν, а Y — η и κ ∘ₘ ν, то произведение ядра сохраняет подгауссов MGФ для суммы X и Y.
LaTeX
$$HasSubgaussianMGF X c κ ν → HasSubgaussianMGF Y cY η (κ ∘ₘ ν) → HasSubgaussianMGF (fun p => X p.1 + Y p.2) (c + cY) (κ ⊗ₖ prodMkLeft Ω' η) ν$$
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
`κ ⊗ₖ prodMkLeft Ω' η : Kernel Ω' (Ω × Ω'')` and `ν`. -/
theorem add_comp {η : Kernel Ω Ω''} [IsZeroOrMarkovKernel η] (hX : HasSubgaussianMGF X c κ ν)
(hY : HasSubgaussianMGF Y cY η (κ ∘ₘ ν)) :
HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ prodMkLeft Ω' η) ν :=
hX.add_compProd hY.prodMkLeft_compProd
