mgf_sum_measure

Mathlib.Probability.Moments.Basic

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

← MathLib Explorer

English

For c in ℝ≥0∞, mgf X (c • μ) t = c.toReal · mgf X μ t.

Русский

Для c≥0∞, mgf X (c • μ) t = c.toReal · mgf X μ t.

LaTeX

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

Lean4

theorem mgf_sum_measure {ι : Type*} {μ : ι → Measure Ω} (hμ : Integrable (fun ω ↦ exp (t * X ω)) (Measure.sum μ)) :
    mgf X (Measure.sum μ) t = ∑' i, mgf X (μ i) t := by simp_rw [mgf, integral_sum_measure hμ]

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

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

Разделы

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

Аффилиация

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