complexMGF_gaussianReal — Mathlib

English

The complex MGF of the Gaussian distribution with mean μ and variance v equals exp(z μ + v z^2 / 2) (identity form).

Русский

Комплексная MGF гауссова распределения имеет вид exp(z μ + v z^2 / 2) (тождество).

LaTeX

$$$\text{complexMGF}_\text{id} (\mathrm{gaussianReal}(\mu, v), z) = \exp\left(z \mu + v z^2 / 2\right)$$$

Lean4

/-- The complex moment-generating function of a random variable with Gaussian distribution
with mean `μ` and variance `v` is given by `z ↦ exp (z * μ + v * z ^ 2 / 2)`. -/
theorem complexMGF_gaussianReal (hX : p.map X = gaussianReal μ v) (z : ℂ) :
    complexMGF X p z = cexp (z * μ + v * z ^ 2 / 2) :=
  by
  have hX_meas : AEMeasurable X p := aemeasurable_of_map_neZero (by rw [hX]; infer_instance)
  rw [← complexMGF_id_map hX_meas, hX, complexMGF_id_gaussianReal]

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