English
If X and Y are a.e.-measurable, then exp(t(X+Y)) is aestronglyMeasurable.
Русский
Если X и Y а.е.-измеримы, то exp(t(X+Y)) является aestronglyMeasurable.
LaTeX
$$$\mathrm{AEStronglyMeasurable}\big(\omega \mapsto e^{t(X(\omega)+Y(\omega))}\big)\mu$$
Lean4
theorem cgf_sum {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) (h_meas : ∀ i, Measurable (X i)) {s : Finset ι}
(h_int : ∀ i ∈ s, Integrable (fun ω => exp (t * X i ω)) μ) : cgf (∑ i ∈ s, X i) μ t = ∑ i ∈ s, cgf (X i) μ t :=
by
have : IsProbabilityMeasure μ := h_indep.isProbabilityMeasure
simp_rw [cgf]
rw [← log_prod _ _ fun j hj => ?_]
· rw [h_indep.mgf_sum h_meas]
· exact (mgf_pos (h_int j hj)).ne'