complexMGF_ofReal — Mathlib

English

When the argument is real, the complex MGF agrees with the real MGF: complexMGF X μ x = mgf X μ x for all real x.

Русский

При действительном аргументе комплексная MGФ совпадает с действительной MGФ: complexMGF X μ x = mgf X μ x для всех действительных x.

LaTeX

$$$complexMGF X μ x = mgf X μ x \quad( x \in \mathbb{R})$$$

Lean4

theorem complexMGF_ofReal (x : ℝ) : complexMGF X μ x = mgf X μ x :=
  by
  rw [complexMGF, mgf, ← integral_complex_ofReal]
  norm_cast

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