English
For Ω with a finite measure μ and X: Ω→ℝ, HasSubgaussianMGF X c μ holds if and only if Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac Unit).
Русский
Для пространства Ω с мерой μ свойство HasSubgaussianMGF X c μ эквивалентно Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac Unit).
LaTeX
$$$HasSubgaussianMGF\\; X\\; c\\; μ \\;\\iff\\; Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac Unit).$$$
Lean4
theorem HasSubgaussianMGF_iff_kernel :
HasSubgaussianMGF X c μ ↔ Kernel.HasSubgaussianMGF X c (Kernel.const Unit μ) (Measure.dirac ()) :=
⟨fun ⟨h1, h2⟩ ↦ ⟨by simpa, by simpa⟩, fun ⟨h1, h2⟩ ↦ ⟨by simpa using h1, by simpa using h2⟩⟩