re_complexMGF_ofReal'

Mathlib.Probability.Moments.ComplexMGF

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.re_complexMGF_ofReal'

English

The real part of the complex moment generating function equals the real mgf.

Русский

Действительная часть комплексной mgf равна действительной mgf.

LaTeX

$$$\operatorname{re}(\text{complexMGF}(X, μ; x)) = \mathrm{mgf}(X, μ; x)$$$$

Lean4

theorem re_complexMGF_ofReal' : (fun x : ℝ ↦ (complexMGF X μ x).re) = mgf X μ :=
  by
  ext x
  exact re_complexMGF_ofReal x

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

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

Разделы

Аффилиация

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