mgf_smul_measure

Mathlib.Probability.Moments.Basic

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

English

If c ∈ ℝ≥0∞, then mgf X (c • μ) t = c.toReal · mgf X μ t (in real scalar sense).

Русский

Если c ∈ ℝ≥0∞, mgf X (c • μ) t = c.toReal · mgf X μ t.

LaTeX

$$$\mathrm{mgf}(X; c \cdot μ; t) = c^{\text{toReal}} \cdot \mathrm{mgf}(X; μ; t)$$$

Lean4

theorem mgf_smul_measure (c : ℝ≥0∞) : mgf X (c • μ) t = c.toReal * mgf X μ t := by
  rw [mgf, integral_smul_measure, mgf, smul_eq_mul]

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

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

Разделы

Аффилиация

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