zero — Mathlib

English

If μ is a zero-or-probability measure, the identically zero random variable X(ω) ≡ 0 is sub-Gaussian with parameter 0, i.e., HasSubgaussianMGF 0 0 μ.

Русский

Если μ — нулевая или вероятностная мера, тождественно нулевая случайная величина X(ω) ≡ 0 является субгауссовой со параметром 0, то есть HasSubgaussianMGF 0 0 μ.

LaTeX

$$$\mathrm{HasSubgaussianMGF}(0,0,\mu)$$$

Lean4

@[simp]
theorem zero [IsZeroOrProbabilityMeasure μ] : HasSubgaussianMGF 0 0 μ :=
  fun_zero

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