fun_zero — Mathlib

English

Let μ be a measure on Ω that is either zero or a probability measure. The constant zero random variable X(ω) ≡ 0 has a sub-Gaussian moment-generating function with parameter 0, i.e. HasSubgaussianMGF( X ≡ 0, c = 0, μ ).

Русский

Пусть μ — это либо нулевая, либо вероятностная мера, на множестве Ω. Постоянная нулевая случайная величина X(ω) ≡ 0 имеет субгауссову МGF с параметром 0: HasSubgaussianMGF(X ≡ 0, c = 0, μ).

LaTeX

$$$\mathrm{HasSubgaussianMGF}(X, c, \mu)$ with $X(\omega) \equiv 0$ and $c = 0$; i.e. $\mathrm{HasSubgaussianMGF}(0,0,\mu)$.$$

Lean4

@[simp]
theorem fun_zero [IsZeroOrProbabilityMeasure μ] : HasSubgaussianMGF (fun _ ↦ 0) 0 μ := by
  simp [HasSubgaussianMGF_iff_kernel]

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