English
For independent X and Y with appropriate measurability, mgf(X+Y) equals mgf(X) mgf(Y).
Русский
Для независимых X и Y при надлежащей измеримости 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 integrable_exp_mul_sum [IsFiniteMeasure μ] {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ)
(h_meas : ∀ i, Measurable (X i)) {s : Finset ι} (h_int : ∀ i ∈ s, Integrable (fun ω => exp (t * X i ω)) μ) :
Integrable (fun ω => exp (t * (∑ i ∈ s, X i) ω)) μ := by
classical
induction s using Finset.induction_on with
| empty =>
simp only [sum_apply, sum_empty, mul_zero, exp_zero]
exact integrable_const _
| insert i s hi_notin_s
h_rec =>
have : ∀ i : ι, i ∈ s → Integrable (fun ω : Ω => exp (t * X i ω)) μ := fun i hi => h_int i (mem_insert_of_mem hi)
specialize h_rec this
rw [sum_insert hi_notin_s]
refine IndepFun.integrable_exp_mul_add ?_ (h_int i (mem_insert_self _ _)) h_rec
exact (h_indep.indepFun_finset_sum_of_notMem h_meas hi_notin_s).symm
