mgf_le — Mathlib

English

For HasCondSubgaussianMGF h, for each t the inequality comparing conditional exponential moment holds almost everywhere with respect to μ.trim hm.

Русский

Для HasCondSubgaussianMGF h для каждого t выполняется неравенство условного экспоненциального момента почти в большинстве μ.trim hm.

LaTeX

$$ae (μ.trim hm) (fun ω' => cgf X (condExpKernel μ m) ω' t <= exp(c t^2/2))$$

Lean4

theorem mgf_le (h : HasCondSubgaussianMGF m hm X c μ) :
    ∀ᵐ ω' ∂(μ.trim hm), ∀ t, mgf X (condExpKernel μ m ω') t ≤ exp (c * t ^ 2 / 2) :=
  Kernel.HasSubgaussianMGF.mgf_le h

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