English
Under independence and measurability conditions, mgf of X+Y equals mgf X times mgf Y, without additional integrability assumptions beyond measurability of X and Y themselves.
Русский
При независимости и условий измеримости, mgf(X+Y) = mgf(X) mgf(Y) без дополнительных предположений об интегрируемости, кроме измеримости X и Y сами по себе.
LaTeX
$$$\mathrm{mgf}(X+Y, \mu, t) = \mathrm{mgf}(X, \mu, t) \cdot \mathrm{mgf}(Y, \mu, t).$$$
Lean4
theorem mgf_add' {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) (hX : AEStronglyMeasurable X μ)
(hY : AEStronglyMeasurable Y μ) : mgf (X + Y) μ t = mgf X μ t * mgf Y μ t :=
by
have A : Continuous fun x : ℝ => exp (t * x) := by fun_prop
have h'X : AEStronglyMeasurable (fun ω => exp (t * X ω)) μ := A.aestronglyMeasurable.comp_aemeasurable hX.aemeasurable
have h'Y : AEStronglyMeasurable (fun ω => exp (t * Y ω)) μ := A.aestronglyMeasurable.comp_aemeasurable hY.aemeasurable
exact h_indep.mgf_add h'X h'Y
