English
If each X_i is measurable and X_i identically distributed with a fixed X_j on a finite set s, then mgf of the sum equals mgf(X_j) raised to the power card(s).
Русский
Если все X_i измеримы и X_i имеют одну и ту же распределение с X_j на конечном наборе s, то mgf суммы равен mgf(X_j)^{|s|}.
LaTeX
$$$\mathrm{mgf}\Big(\sum_{i\in s} X_i, \mu, t\Big) = \mathrm{mgf}(X_j, \mu, t)^{|s|}.$$$
Lean4
theorem mgf_sum_of_identDistrib {X : ι → Ω → ℝ} {s : Finset ι} {j : ι} (h_meas : ∀ i, Measurable (X i))
(h_indep : iIndepFun X μ) (hident : ∀ i ∈ s, ∀ j ∈ s, IdentDistrib (X i) (X j) μ μ) (hj : j ∈ s) (t : ℝ) :
mgf (∑ i ∈ s, X i) μ t = mgf (X j) μ t ^ #s :=
by
rw [h_indep.mgf_sum h_meas]
exact Finset.prod_eq_pow_card fun i hi => mgf_congr_of_identDistrib (X i) (X j) (hident i hi j hj) t
