English
If X and Y are independent and exp(tX), exp(tY) are integrable, then cgf(X+Y) = cgf(X) + cgf(Y).
Русский
Если X и Y независимы и exp(tX), exp(tY) интегрируемы, то 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 cgf_add {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) (h_int_X : Integrable (fun ω => exp (t * X ω)) μ)
(h_int_Y : Integrable (fun ω => exp (t * Y ω)) μ) : cgf (X + Y) μ t = cgf X μ t + cgf Y μ t :=
by
by_cases hμ : μ = 0
· simp [hμ]
simp only [cgf, h_indep.mgf_add h_int_X.aestronglyMeasurable h_int_Y.aestronglyMeasurable]
exact log_mul (mgf_pos' hμ h_int_X).ne' (mgf_pos' hμ h_int_Y).ne'