English
If X and Y are independent and exp(tX), exp(tY) are integrable/strongly measurable, then mgf(X+Y) = mgf(X) · mgf(Y).
Русский
Если X и Y независимы и exp(tX), exp(tY) пригодны для интегрирования/сильно измеримы, то mgf(X+Y) = mgf(X) · mgf(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 (fun ω => exp (t * X ω)) μ)
(hY : AEStronglyMeasurable (fun ω => exp (t * Y ω)) μ) : mgf (X + Y) μ t = mgf X μ t * mgf Y μ t :=
by
simp_rw [mgf, Pi.add_apply, mul_add, exp_add]
exact (h_indep.exp_mul t t).integral_mul_eq_mul_integral hX hY