English
If Y is almost-everywhere measurable and X has a sub-Gaussian MGF with respect to the pushforward measure μ.map Y, then the composition X ∘ Y has the same sub-Gaussian MGФ with respect to μ.
Русский
Если Y почти surely измерима и X имеет субгауссов MGФ относительно меры μ.map Y, то композиция X ∘ Y имеет такую же субгауссовскую MGФ относительно μ.
LaTeX
$$$\forall Y,X,\; AEMeasurable(Y,\mu) \land HasSubgaussianMGF(X,c,(\mu.map Y)) \Rightarrow HasSubgaussianMGF(X\circ Y,c,\mu)$$$
Lean4
theorem of_map {Ω' : Type*} {mΩ' : MeasurableSpace Ω'} {μ : Measure Ω'} {Y : Ω' → Ω} {X : Ω → ℝ} (hY : AEMeasurable 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 [integrable_map_measure h1.aestronglyMeasurable (by fun_prop)] at h1
mgf_le
t := by
convert h.mgf_le t using 1
rw [mgf_map hY (h.integrable_exp_mul t).1]
