mgf_add — Mathlib

English

If X and Y are independent and exp(tX), exp(tY) are integrable/strongly measurable, then mgf(X+Y) = mgf(X) · mgf(Y).

Русский

Если X и Y независимы и exp(tX), exp(tY) пригодны для интегрирования/сильно измеримы, то 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 mgf_add {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) (hX : AEStronglyMeasurable (fun ω => exp (t * X ω)) μ)
    (hY : AEStronglyMeasurable (fun ω => exp (t * Y ω)) μ) : mgf (X + Y) μ t = mgf X μ t * mgf Y μ t :=
  by
  simp_rw [mgf, Pi.add_apply, mul_add, exp_add]
  exact (h_indep.exp_mul t t).integral_mul_eq_mul_integral hX hY

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