neg — Mathlib

English

If X has sub-Gaussian MGF with parameter c, then the negation −X also has sub-Gaussian MGF with the same parameter c.

Русский

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

LaTeX

$$$\forall X,c,\mu\,\;\mathrm{HasSubgaussianMGF}(X,c,\mu) \Rightarrow \mathrm{HasSubgaussianMGF}(-X,c,\mu)$$$

Lean4

theorem neg {c : ℝ≥0} (h : HasSubgaussianMGF X c μ) : HasSubgaussianMGF (-X) c μ := by
  simpa [HasSubgaussianMGF_iff_kernel] using (HasSubgaussianMGF_iff_kernel.1 h).neg

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