zero

Mathlib.Probability.Moments.SubGaussian

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.HasCondSubgaussianMGF.zero

English

If X ≡ 0, then HasCondSubgaussianMGF m hm 0 0 μ.

Русский

Если X ≡ 0, то HasCondSubgaussianMGF m hm 0 0 μ.

LaTeX

$$$HasCondSubgaussianMGF\\; m\\; hm\\; 0\\; 0\\; \\mu$$$

Lean4

@[simp]
theorem zero : HasCondSubgaussianMGF m hm 0 0 μ :=
  Kernel.HasSubgaussianMGF.zero

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru