variance_id_gaussianReal — Mathlib

English

The same variance result with the identity function: Var[X; GaussianReal(μ,v)] = v.

Русский

Та же дисперсия при тождественной функции: Var[X; GaussianReal(μ,v)] = v.

LaTeX

$$$\mathrm{Var}[\mathrm{Id}; GaussianReal(\mu,v)] = v.$$$

Lean4

/-- The variance of a real Gaussian distribution `gaussianReal μ v` is
its variance parameter `v`. -/
@[simp]
theorem variance_id_gaussianReal : Var[id; gaussianReal μ v] = v :=
  variance_fun_id_gaussianReal

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