variance_continuousLinearMap_gaussianReal

Mathlib.Probability.Distributions.Gaussian.Real

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.variance_continuousLinearMap_gaussianReal

← MathLib Explorer

English

For GaussianReal μ v, Var[X] = v.

Русский

Для GaussianReal μ v верна D[X] = v.

LaTeX

$$$\operatorname{Var}(X) = v$, where $X \sim \mathcal{N}(\mu,v)$.$$

Lean4

@[simp]
theorem variance_continuousLinearMap_gaussianReal (L : ℝ →L[ℝ] ℝ) : Var[L; gaussianReal μ v] = (L 1 ^ 2).toNNReal * v :=
  variance_linearMap_gaussianReal L

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru