measure_ge_le — Mathlib

English

If X and Y are sub-Gaussian with parameters cX and cY under μ, then X + Y is sub-Gaussian with parameter (√cX + √cY)^2 under μ.

Русский

Если X и Y субгауссовы с параметрами cX и cY относительно μ, то сумма X + Y субгауссова с параметром (√cX + √cY)^2.

LaTeX

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

Lean4

/-- Chernoff bound on the right tail of a sub-Gaussian random variable. -/
theorem measure_ge_le (h : HasSubgaussianMGF X c μ) {ε : ℝ} (hε : 0 ≤ ε) :
    μ.real {ω | ε ≤ X ω} ≤ exp (-ε ^ 2 / (2 * c)) :=
  by
  rw [HasSubgaussianMGF_iff_kernel] at h
  simpa using h.measure_ge_le hε

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