ae_condExp_le

Mathlib.Probability.Moments.SubGaussian

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.HasCondSubgaussianMGF.ae_condExp_le

← MathLib Explorer

English

The HasCondSubgaussianMGF mgf_le bound holds almost everywhere with respect to μ.

Русский

Неравенство mgf_le выполняется почти всюду относительно μ.

LaTeX

$$cgf_le (h)$$

Lean4

theorem ae_condExp_le (h : HasCondSubgaussianMGF m hm X c μ) (t : ℝ) :
    ∀ᵐ ω' ∂μ, (μ[fun ω ↦ exp (t * X ω)|m]) ω' ≤ exp (c * t ^ 2 / 2) :=
  ae_of_ae_trim hm (h.ae_trim_condExp_le t)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru