add — Mathlib

English

If X and Y are sub-Gaussian with parameters cX and cY and are independent, then X + Y is sub-Gaussian with parameter cX + cY.

Русский

Если X и Y субгауссовы с параметрами cX и cY и независимы, то X + Y субгауссов с параметром cX + cY.

LaTeX

$$$\mathrm{HasSubgaussianMGF}(X,cX,\mu) \land \mathrm{HasSubgaussianMGF}(Y,cY,\mu) \land \mathrm{IndepFun}(X,Y,\mu) \Rightarrow \mathrm{HasSubgaussianMGF}(X+Y,cX+cY,\mu)$$$

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
  have := (HasSubgaussianMGF_iff_kernel.1 hX).add (HasSubgaussianMGF_iff_kernel.1 hY)
  simpa [HasSubgaussianMGF_iff_kernel] using this

Похожие утверждения