cgf_add — Mathlib

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'

Похожие утверждения