variance_id_map

Mathlib.Probability.Moments.Variance

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

English

Let X: Ω → ℝ be a random variable and μ a measure. Then Var[id; μ.map X] = Var[X; μ].

Русский

Пусть X: Ω → ℝ — случайная величина, μ — мера. Тогда Var[id; μ.map X] = Var[X; μ].

LaTeX

$$$\operatorname{Var}[\mathrm{id};\, \mu.map X] = \operatorname{Var}[X;\, \mu]$$$

Lean4

theorem variance_id_map (hX : AEMeasurable X μ) : Var[id; μ.map X] = Var[X; μ] := by
  simp [variance_map measurable_id.aemeasurable hX]

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

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

Разделы

Аффилиация

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