exp_cgf

Mathlib.Probability.Moments.Basic

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

← MathLib Explorer

English

mgf id(μ.map X) t = mgf X μ t for ae-measurable X.

Русский

mgf(id)(μ.map X) t = mgf X μ t при ae-измеримости X.

LaTeX

$$$\mathrm{mgf}\; id\; (\mu\!\mapsto\! X)\; t = \mathrm{mgf}\; X\; \mu\; t$$$

Lean4

theorem exp_cgf [hμ : NeZero μ] (hX : Integrable (fun ω ↦ exp (t * X ω)) μ) : exp (cgf X μ t) = mgf X μ t := by
  rw [cgf, exp_log (mgf_pos' hμ.out hX)]

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

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

Разделы

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

Аффилиация

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