variance_linearMap_gaussianReal — Mathlib

English

Var[L; GaussianReal(μ,v)] = (L 1^2).toNNReal · v.

Русский

Дисперсия после линейного отображения: Var[L X] = (L(1))^2 · v.

LaTeX

$$$\operatorname{Var}[L; GaussianReal(\mu,v)] = (L(1)^2).toNNReal \cdot v.$$$

Lean4

@[simp]
theorem variance_linearMap_gaussianReal (L : ℝ →ₗ[ℝ] ℝ) : Var[L; gaussianReal μ v] = (L 1 ^ 2).toNNReal * v :=
  by
  rw [← variance_id_map, gaussianReal_map_linearMap, variance_id_gaussianReal]
  · simp only [NNReal.coe_mul, Real.coe_toNNReal']
  · fun_prop

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