ae_trim_condExp_le — Mathlib

English

For HasCondSubgaussianMGF h, the almost-everywhere bound on the mgf under condExpKernel holds with respect to μ.

Русский

Для HasCondSubgaussianMGF h почти повсюду выполняется неравенство mgf под condExpKernel относительно μ.

LaTeX

$$ae (HasCondSubgaussianMGF.mgf_le h) (condExpKernel μ m)$$

Lean4

theorem ae_trim_condExp_le (h : HasCondSubgaussianMGF m hm X c μ) (t : ℝ) :
    ∀ᵐ ω' ∂(μ.trim hm), (μ[fun ω ↦ exp (t * X ω)|m]) ω' ≤ exp (c * t ^ 2 / 2) :=
  by
  have h_eq := condExp_ae_eq_trim_integral_condExpKernel hm (h.integrable_exp_mul t)
  simp_rw [condExpKernel_comp_trim] at h_eq
  filter_upwards [h.mgf_le, h_eq] with ω' h_mgf h_eq
  rw [h_eq]
  exact h_mgf t

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