mgf_const'

Mathlib.Probability.Moments.Basic

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

English

For a constant c, mgf of the constant process equals μ(Ω) times e^{t c}.

Русский

Для константы c mgf константного процесса равен μ(Ω) × e^{t c}.

LaTeX

$$mgf(\lambda _ , c) = μ(Ω) \cdot e^{t c}$$

Lean4

@[simp]
theorem mgf_const' (c : ℝ) : mgf (fun _ => c) μ t = μ.real Set.univ * exp (t * c) := by
  simp only [mgf, integral_const, smul_eq_mul]

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

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

Разделы

Аффилиация

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