mgf_const_add

Mathlib.Probability.Moments.Basic

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.mgf_const_add

← MathLib Explorer

English

MGF of X plus a constant α satisfies M_{X+α}(t) = e^{t α} M_X(t).

Русский

MGF X+α удовлетворяет M_{X+α}(t) = e^{t α} M_X(t).

LaTeX

$$$\mathrm{mgf}(X + α; μ; t) = e^{t α} \mathrm{mgf}(X; μ; t)$$$

Lean4

theorem mgf_const_add (α : ℝ) : mgf (fun ω => α + X ω) μ t = exp (t * α) * mgf X μ t :=
  by
  rw [mgf, mgf, ← integral_const_mul]
  congr with x
  dsimp
  rw [mul_add, exp_add]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru