cgf_le — Mathlib

English

If h : HasSubgaussianMGF X c μ, then for all t ∈ ℝ, cgf X μ t ≤ c t^2 / 2.

Русский

Если h: HasSubgaussianMGF X c μ, то для всех t ∈ ℝ выполняется неравенство cgf X μ t ≤ c t^2 / 2.

LaTeX

$$$\\text{cgf}(X,\\mu,t) \\le \\dfrac{c t^2}{2}$$$

Lean4

theorem cgf_le (h : HasSubgaussianMGF X c μ) (t : ℝ) : cgf X μ t ≤ c * t ^ 2 / 2 :=
  by
  rw [HasSubgaussianMGF_iff_kernel] at h
  simpa using (all_ae_of h.cgf_le t)

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