ae_eq_zero_of_hasSubgaussianMGF_zero

English

If X has sub-Gaussian MGF with parameter 0, then X is almost everywhere equal to zero with respect to μ.

Русский

Если X имеет субгауссову MGФ с параметром 0, то X равно нулю μ‑почти везде.

LaTeX

$$$\mathrm{HasSubgaussianMGF}(X,0,\mu) \Rightarrow X =^{\mu}_{ae} 0$$$

Lean4

theorem ae_eq_zero_of_hasSubgaussianMGF_zero (h : HasSubgaussianMGF X 0 μ) : X =ᵐ[μ] 0 := by
  simpa using (HasSubgaussianMGF_iff_kernel.1 h).ae_eq_zero_of_hasSubgaussianMGF_zero

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