mgf_const

Mathlib.Probability.Moments.Basic

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

English

If μ is a probability measure, mgf of a constant c is exp(t c).

Русский

Если μ является вероятностной мерой, mgf константы c равно e^{t c}.

LaTeX

$$mgf (\text{const } c) μ t = e^{t c}$$

Lean4

theorem mgf_const (c : ℝ) [IsProbabilityMeasure μ] : mgf (fun _ => c) μ t = exp (t * c) := by simp

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

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

Разделы

Аффилиация

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