English
The complex moment-generating function of a Gaussian-distributed variable X with mean μ and variance v is exp(z μ + v z^2 / 2).
Русский
Комплексная моментогенерирующая функция гауссовой величины X имеет вид exp(z μ + v z^2 / 2).
LaTeX
$$$\text{complexMGF}_X(p, z) = \exp\left(z \mu + v z^2 / 2\right)$$$
Lean4
/-- The complex moment-generating function of a Gaussian distribution with mean `μ` and variance `v`
is given by `z ↦ exp (z * μ + v * z ^ 2 / 2)`. -/
theorem complexMGF_id_gaussianReal (z : ℂ) : complexMGF id (gaussianReal μ v) z = cexp (z * μ + v * z ^ 2 / 2) :=
by
by_cases hv : v = 0
· simp [complexMGF, hv]
calc
∫ x, cexp (z * x) ∂gaussianReal μ v
_ = ∫ x, gaussianPDFReal μ v x * cexp (z * x) ∂ℙ := by
simp_rw [integral_gaussianReal_eq_integral_smul hv, Complex.real_smul]
_ = (√(2 * π * v))⁻¹ * ∫ x : ℝ, cexp (-(2 * v)⁻¹ * x ^ 2 + (z + μ / v) * x + -μ ^ 2 / (2 * v)) ∂ℙ :=
by
unfold gaussianPDFReal
push_cast
simp_rw [mul_assoc, integral_const_mul, ← Complex.exp_add]
congr with x
congr 1
ring
_ =
(√(2 * π * v))⁻¹ * (π / - -(2 * v)⁻¹) ^ (1 / 2 : ℂ) *
cexp (-μ ^ 2 / (2 * v) - (z + μ / v) ^ 2 / (4 * -(2 * v)⁻¹)) :=
by rw [integral_cexp_quadratic (by simpa using pos_iff_ne_zero.mpr hv), ← mul_assoc]
_ = 1 * cexp (-μ ^ 2 / (2 * v) - (z + μ / v) ^ 2 / (4 * -(2 * v)⁻¹)) :=
by
congr 1
simp only [field, sqrt_eq_rpow, one_div, ofReal_inv, NNReal.coe_inv, NNReal.coe_mul, NNReal.coe_ofNat, ofReal_mul,
ofReal_ofNat, neg_neg, div_inv_eq_mul, ne_eq, ofReal_eq_zero, rpow_eq_zero, not_false_eq_true]
rw [Complex.ofReal_cpow (by positivity)]
push_cast
ring_nf
_ = cexp (z * μ + v * z ^ 2 / 2) := by
rw [one_mul]
congr 1
have : (v : ℂ) ≠ 0 := by simpa
simp [field]
ring
