English
Let X be a real-valued random variable with Gaussian distribution of mean μ and variance v. Then its cumulant generating function is κ_X(t) = μ t + (v t^2)/2 for all t ∈ ℝ.
Русский
Пусть X — действительная случайная величина, имеющая гауссовское распределение с математическим ожиданием μ и дисперсией v. Тогда кумулянтная функция X равна κ_X(t) = μ t + (v t^2)/2 для всех t ∈ ℝ.
LaTeX
$$$\text{If } X \text{ has Gaussian distribution } \mathcal{N}(\mu, v) \text{, then } \kappa_X(t) = \mu t + \frac{v t^{2}}{2} \quad (t \in \mathbb{R}).$$$
Lean4
/-- The cumulant-generating function of a random variable with Gaussian distribution
with mean `μ` and variance `v` is given by `t ↦ μ * t + v * t ^ 2 / 2`. -/
theorem cgf_gaussianReal (hX : p.map X = gaussianReal μ v) (t : ℝ) : cgf X p t = μ * t + v * t ^ 2 / 2 := by
rw [cgf, mgf_gaussianReal hX t, Real.log_exp]
