charFun_gaussianReal — Mathlib

English

For a Gaussian random variable X with mean μ and variance v, mgf X p t equals exp(μ t + v t^2 / 2).

Русский

Для гауссовой случайной величины X с параметрами μ и v, mgf равна exp(μ t + v t^2 / 2).

LaTeX

$$$\text{mgf } X p t = \exp\left(\mu t + v t^2 / 2\right)$$$

Lean4

/-- The characteristic function of a Gaussian distribution with mean `μ` and variance `v`
is given by `t ↦ exp (t * μ - v * t ^ 2 / 2)`. -/
theorem charFun_gaussianReal (t : ℝ) : charFun (gaussianReal μ v) t = cexp (t * μ * I - v * t ^ 2 / 2) :=
  by
  rw [← complexMGF_id_mul_I, complexMGF_id_gaussianReal]
  congr
  simp only [mul_pow, I_sq, mul_neg, mul_one, sub_eq_add_neg]
  ring_nf

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