complexMGF_mul_I — Mathlib

English

If X is an a.e. measurable function, then complexMGF X μ (t i) equals the characteristic function of the pushforward measure μ.map X evaluated at t.

Русский

Если X измерима почти всюду, тогда complexMGF X μ (t i) равно характеристической функции образа меры μ по X в t.

LaTeX

$$$ complexMGF X μ (t i) = charFun (μ.map X) t $$$

Lean4

theorem complexMGF_mul_I (hX : AEMeasurable X μ) (t : ℝ) : complexMGF X μ (t * I) = charFun (μ.map X) t := by
  rw [← complexMGF_id_map hX, complexMGF_id_mul_I]

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