zero_measure

Mathlib.Probability.Moments.SubGaussian

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.Kernel.HasSubgaussianMGF.zero_measure

English

The HasSubgaussianMGF property holds for the trivial kernel when the target measure is zero.

Русский

Свойство HasSubgaussianMGF сохраняется для тривиального ядра, когда мера нулевая.

LaTeX

$$$\\text{HasSubgaussianMGF}(X,c,\\kappa,0).$$$

Lean4

@[simp]
theorem zero_measure : HasSubgaussianMGF X c κ (0 : Measure Ω') :=
  ⟨by simp, by simp⟩

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

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

Разделы

Аффилиация

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