HasSubgaussianMGF_iff_kernel — Mathlib

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⟩⟩

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