complexMGF — Mathlib

English

Introduce a complex extension of the moment generating function: complexMGF(X, μ, z) = ∫ ce^{z X(ω)} dμ(ω).

Русский

Введём комплексное расширение функции момента: complexMGF(X, μ, z) = ∫ ce^{z X(ω)} dμ(ω).

LaTeX

$$$\mathrm{complexMGF}(X, \mu, z) = \int_{\Omega} \mathrm{cexp}(z \cdot X(\omega)) \, d\mu(\omega).$$$

Lean4

/-- Complex extension of the moment-generating function. -/
noncomputable def complexMGF (X : Ω → ℝ) (μ : Measure Ω) (z : ℂ) : ℂ :=
  μ[fun ω ↦ cexp (z * X ω)]

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