English
The of_rat construction preserves HasSubgaussianMGF when the accompanying conditions on integrability and mgf bounds hold for rational approximations.
Русский
Конструкция of_rat сохраняет HasSubgaussianMGF при соблюдении условий интегрируемости и ограничений MGФ для рациональных приближений.
LaTeX
$$$\\text{of\\_rat}(\\,h\\,)$ preserves subgaussian MGFs under rational approximations, i.e. the property is closed under taking limits of MGFs on rationals.$$
Lean4
theorem of_map {Ω'' : Type*} {mΩ'' : MeasurableSpace Ω''} {κ : Kernel Ω' Ω''} {Y : Ω'' → Ω} {X : Ω → ℝ}
(hY : Measurable Y) (h : HasSubgaussianMGF X c (κ.map Y) ν) : HasSubgaussianMGF (X ∘ Y) c κ ν
where
integrable_exp_mul
t := by
have h1 := h.integrable_exp_mul t
rwa [← Measure.map_comp _ _ hY, integrable_map_measure h1.aestronglyMeasurable (by fun_prop)] at h1
mgf_le := by
filter_upwards [h.ae_forall_integrable_exp_mul, h.mgf_le] with ω' h_int h_mgf t
convert h_mgf t
ext t
rw [map_apply _ hY, mgf_map hY.aemeasurable]
convert (h_int t).1
rw [map_apply _ hY]
