English
The moment-generating function of a Gaussian distribution is after all equal to mgf_id_gaussianReal: mgf id (gaussianReal μ v) = t ↦ rexp(μ t + v t^2 / 2).
Русский
Моментогенерирующая функция гауссовского распределения равна mgf_id_gaussianReal: mgf id (gaussianReal μ v) = t ↦ exp(μ t + v t^2 / 2).
LaTeX
$$$\text{mgf}_{\mathrm{id}}(\mathrm{gaussianReal}(\mu, v))(t) = \exp\left(\mu t + v t^2 / 2\right)$$$
Lean4
/-- The moment-generating function of a random variable with Gaussian distribution
with mean `μ` and variance `v` is given by `t ↦ exp (μ * t + v * t ^ 2 / 2)`. -/
theorem mgf_gaussianReal (hX : p.map X = gaussianReal μ v) (t : ℝ) : mgf X p t = rexp (μ * t + v * t ^ 2 / 2) :=
by
suffices (mgf X p t : ℂ) = rexp (μ * t + ↑v * t ^ 2 / 2) from mod_cast this
have hX_meas : AEMeasurable X p := aemeasurable_of_map_neZero (by rw [hX]; infer_instance)
rw [← mgf_id_map hX_meas, ← complexMGF_ofReal, hX, complexMGF_id_gaussianReal, mul_comm μ]
norm_cast
