English
If X and Y are independent with finite mgf, then cgf(X+Y) = cgf(X) + cgf(Y).
Русский
Если X и Y независимы и mgf конечен, то cgf(X+Y) = cgf(X) + cgf(Y).
LaTeX
$$$\mathrm{cgf}(X+Y, \mu, t) = \mathrm{cgf}(X, \mu, t) + \mathrm{cgf}(Y, \mu, t).$$$
Lean4
theorem mgf_sum {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) (h_meas : ∀ i, Measurable (X i)) (s : Finset ι) :
mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t :=
by
have : IsProbabilityMeasure μ := h_indep.isProbabilityMeasure
classical
induction s using Finset.induction_on with
| empty => simp
| insert i s hi_notin_s
h_rec =>
have h_int' : ∀ i : ι, AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i =>
((h_meas i).const_mul t).exp.aestronglyMeasurable
rw [sum_insert hi_notin_s,
IndepFun.mgf_add (h_indep.indepFun_finset_sum_of_notMem h_meas hi_notin_s).symm (h_int' i)
(aestronglyMeasurable_exp_mul_sum fun i _ => h_int' i),
h_rec, prod_insert hi_notin_s]
