fun_zero — Mathlib

English

If X has HasSubgaussianMGF with parameters X, c, κ, ν, then -X has HasSubgaussianMGF with the same c, κ, ν.

Русский

Если X имеет субгауссов MGФ, то и −X имеет субгауссов MGФ с теми же параметрами.

LaTeX

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

Lean4

@[simp]
theorem fun_zero [IsFiniteMeasure ν] [IsZeroOrMarkovKernel κ] : HasSubgaussianMGF (fun _ ↦ 0) 0 κ ν
    where
  integrable_exp_mul := by simp
  mgf_le := by simpa using ae_of_all _ fun _ ↦ measureReal_le_one

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