cgf_le — Mathlib

English

For almost every ω', cgf(X, κ ω') is bounded above by c t^2/2 for all t, i.e. an upper quadratic bound on the CGF.

Русский

Почти наверняка для ω' имеется верхняя квадратичная оценка cgf: cgf(X, κ ω')(t) ≤ c t^2/2 для всех t.

LaTeX

$$$\\forall^{\\!}\\omega'\\, (\\kappa(\\omega') \\text{-a.e.}) :\\forall t\\in\\mathbb{R},\\ cgf(X,\\kappa(\\omega'))(t) \\le c \\frac{t^2}{2}.$$$

Lean4

theorem cgf_le (h : HasSubgaussianMGF X c κ ν) : ∀ᵐ ω' ∂ν, ∀ t, cgf X (κ ω') t ≤ c * t ^ 2 / 2 :=
  by
  filter_upwards [h.mgf_le, h.ae_forall_integrable_exp_mul] with ω' h h_int t
  calc
    cgf X (κ ω') t
    _ = log (mgf X (κ ω') t) := rfl
    _ ≤ log (exp (c * t ^ 2 / 2)) := by
      by_cases h0 : κ ω' = 0
      · simpa [h0] using by positivity
      gcongr
      · exact mgf_pos' h0 (h_int t)
      · exact h t
    _ ≤ c * t ^ 2 / 2 := by rw [log_exp]

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