mgf_add_const — Mathlib

English

If μ and ν are integrable with respect to exp(t X), then mgf X (μ + ν) t = mgf X μ t + mgf X ν t.

Русский

Если μ и ν интегрируемы по exp(t X), то mgf(X; μ+ν; t) = mgf(X; μ; t) + mgf(X; ν; t).

LaTeX

$$$\mathrm{mgf}(X; μ + ν; t) = \mathrm{mgf}(X; μ; t) + \mathrm{mgf}(X; ν; t)$$$

Lean4

theorem mgf_add_const (α : ℝ) : mgf (fun ω => X ω + α) μ t = mgf X μ t * exp (t * α) := by
  simp only [add_comm, mgf_const_add, mul_comm]

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