neg — Mathlib

English

If X is HasSubgaussianMGF with c, κ, ν, then −X is HasSubgaussianMGF with the same parameters; and if X and Y are ae-equal, the statement is preserved.

Русский

Если X имеет субгауссов MGФ с параметрами, то −X также имеет субгауссов MGФ с теми же параметрами; сохранится и при ae-эквивалентности.

LaTeX

$$$\\text{HasSubgaussianMGF}(-X,c,\\kappa,\\nu) \\quad\\text{и}\\quad \\text{congr}$$$

Lean4

theorem neg {c : ℝ≥0} (h : HasSubgaussianMGF X c κ ν) : HasSubgaussianMGF (-X) c κ ν
    where
  integrable_exp_mul t := by simpa using h.integrable_exp_mul (-t)
  mgf_le := by filter_upwards [h.mgf_le] with ω' hm t using by simpa [mgf] using hm (-t)

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