complexMGF_id_mul_I — Mathlib

English

For real t, complexMGF X μ at t times i equals the characteristic function of μ map X at t.

Русский

Для вещественного t, complexMGF X μ при t·i равно характеристической функции μ по X в t.

LaTeX

$$$ complexMGF X μ (t \cdot i) = charFun μ t $$$

Lean4

theorem complexMGF_id_mul_I {μ : Measure ℝ} (t : ℝ) : complexMGF id μ (t * I) = charFun μ t :=
  by
  simp only [complexMGF, id_eq, charFun, RCLike.inner_apply, conj_trivial, ofReal_mul]
  congr with x
  ring_nf

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