English
If μ is finite and X is sub-Gaussian with μ.trim hm and Y is conditionally sub-Gaussian with respect to hm, then X+Y is sub-Gaussian with parameter cX+cY with respect to μ.
Русский
Если μ конечна и X субгауссово относительно μ с усечением hm, а Y условно субгауссово относительно hm, тогда X+Y субгауссов с параметром cX+cY.
LaTeX
$$$[IsFiniteMeasure μ] \Rightarrow (\mathrm{HasSubgaussianMGF}(X,cX,μ) \land \mathrm{HasCondSubgaussianMGF}(m,hm,Y,cY,μ)) \Rightarrow \mathrm{HasSubgaussianMGF}(X+Y,cX+cY,μ)$$$
Lean4
/-- If `X` is sub-Gaussian with parameter `cX` with respect to the restriction of `μ` to
a sub-sigma-algebra `m` and `Y` is conditionally sub-Gaussian with parameter `cY` with respect to
`m` and `μ` then `X + Y` is sub-Gaussian with parameter `cX + cY` with respect to `μ`.
`HasSubgaussianMGF X cX (μ.trim hm)` can be obtained from `HasSubgaussianMGF X cX μ` if `X` is
`m`-measurable. See `HasSubgaussianMGF.trim`. -/
theorem HasSubgaussianMGF_add_of_HasCondSubgaussianMGF [IsFiniteMeasure μ] {Y : Ω → ℝ} {cX cY : ℝ≥0} (hm : m ≤ mΩ)
(hX : HasSubgaussianMGF X cX (μ.trim hm)) (hY : HasCondSubgaussianMGF m hm Y cY μ) :
HasSubgaussianMGF (X + Y) (cX + cY) μ :=
by
suffices
HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (cX + cY) (@Measure.map Ω (Ω × Ω) mΩ (m.prod mΩ) (fun ω ↦ (id ω, id ω)) μ)
by
have h_eq : X + Y = (fun p ↦ X p.1 + Y p.2) ∘ (fun ω ↦ (id ω, id ω)) := rfl
rw [h_eq]
refine HasSubgaussianMGF.of_map ?_ this
exact @Measurable.aemeasurable _ _ _ (m.prod mΩ) _ _ ((measurable_id'' hm).prodMk measurable_id)
rw [HasSubgaussianMGF_iff_kernel] at hX ⊢
have hY' : Kernel.HasSubgaussianMGF Y cY (condExpKernel μ m) (Kernel.const Unit (μ.trim hm) ∘ₘ Measure.dirac ()) := by
simpa
convert hX.add_comp hY'
ext
rw [Kernel.const_apply, ← Measure.compProd, compProd_trim_condExpKernel]
