English
For X ∼ GaussianReal(μ,v), the variance of X is v. More generally, Var[x ↦ x; GaussianReal μ v] = v.
Русский
Дисперсия X при X ∼ GaussianReal(μ,v) равна v. В частности, Var[x; GaussianReal(μ,v)] = v.
LaTeX
$$$\mathrm{Var}[X; GaussianReal(\mu,v)] = v.$$$
Lean4
/-- The variance of a real Gaussian distribution `gaussianReal μ v` is
its variance parameter `v`. -/
@[simp]
theorem variance_fun_id_gaussianReal : Var[fun x ↦ x; gaussianReal μ v] = v :=
by
rw [variance_eq_integral measurable_id'.aemeasurable]
simp only [integral_id_gaussianReal]
calc
∫ ω, (ω - μ) ^ 2 ∂gaussianReal μ v
_ = ∫ ω, ω ^ 2 ∂(gaussianReal μ v).map (fun x ↦ x - μ) := by rw [integral_map (by fun_prop) (by fun_prop)]
_ = ∫ ω, ω ^ 2 ∂(gaussianReal 0 v) := by simp [gaussianReal_map_sub_const]
_ = iteratedDeriv 2 (mgf (fun x ↦ x) (gaussianReal 0 v)) 0 := by rw [iteratedDeriv_mgf_zero] <;> simp
_ = v := by
rw [mgf_fun_id_gaussianReal, iteratedDeriv_succ, iteratedDeriv_one]
simp only [zero_mul, zero_add]
have : deriv (fun t ↦ rexp (v * t ^ 2 / 2)) = fun t ↦ v * t * rexp (v * t ^ 2 / 2) :=
by
ext t
rw [_root_.deriv_exp (by fun_prop)]
simp only [deriv_div_const, differentiableAt_const, differentiableAt_fun_id, Nat.cast_ofNat,
DifferentiableAt.fun_pow, deriv_fun_mul, deriv_const', zero_mul, deriv_fun_pow, Nat.add_one_sub_one, pow_one,
deriv_id'', mul_one, zero_add]
ring
rw [this, deriv_fun_mul (by fun_prop) (by fun_prop), deriv_fun_mul (by fun_prop) (by fun_prop)]
simp
