complexMGF_id_map — Mathlib

English

Let X be a real-valued random variable on a measure space (Ω, m) with measure μ. Then the complex moment-generating function of X with respect to μ equals the complex moment-generating function of the identity function with respect to the pushforward measure μ.map X.

Русский

Пусть X — вещественная случайная величина на мере Ω с мерой μ. Тогда комплексная моментогенерационная функция X относительно μ равна комплексной MGF для тождественной функции относительно образа меры μ.map X.

LaTeX

$$$complexMGF\ id\ (\mu.map X) = complexMGF X\ \mu$$$

Lean4

theorem complexMGF_id_map (hX : AEMeasurable X μ) : complexMGF id (μ.map X) = complexMGF X μ :=
  by
  ext t
  rw [complexMGF, integral_map hX]
  · rfl
  · fun_prop

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