mgf_neg

Mathlib.Probability.Moments.Basic

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

English

mgf(-X) μ t = mgf X μ (−t).

Русский

MGF от −X равен MGF(X) при −t.

LaTeX

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

Lean4

theorem mgf_neg : mgf (-X) μ t = mgf X μ (-t) := by simp_rw [mgf, Pi.neg_apply, mul_neg, neg_mul]

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

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

Разделы

Аффилиация

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