English
If X is measurable with respect to a sub-sigma-algebra m and HasSubgaussianMGF X c μ, then trimming μ to m preserves HasSubgaussianMGF with the same parameter c.
Русский
Если X измерима относительно под-алгебры m и имеет субгауссовскую MGФ с параметром c, то усечение меры по m сохраняет тот же параметр.
LaTeX
$$$\text{hm}: m \le m_\Omega, \; X \text{ meas } m, \; \mathrm{HasSubgaussianMGF}(X,c,\mu) \Rightarrow \mathrm{HasSubgaussianMGF}(X,c,\mu\;\text{trim}\;\text{hm})$$$
Lean4
theorem trim (hm : m ≤ mΩ) (hXm : Measurable[m] X) (hX : HasSubgaussianMGF X c μ) : HasSubgaussianMGF X c (μ.trim hm)
where
integrable_exp_mul
t := by
refine (hX.integrable_exp_mul t).trim hm ?_
exact Measurable.stronglyMeasurable <| by fun_prop
mgf_le
t := by
rw [mgf, ← integral_trim]
· exact hX.mgf_le t
· exact Measurable.stronglyMeasurable <| by fun_prop
