integrable_condVar

Mathlib.Probability.CondVar

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

English

The conditional variance is integrable with respect to μ: Var[X; μ | m] is μ-integrable.

Русский

Условная дисперсия интегрируема по μ: Var[X; μ | m] интегрируема по μ.

LaTeX

$$$ Integrable( Var[X; μ | m] )\, μ $$$

Lean4

theorem integrable_condVar : Integrable Var[X; μ | m] μ :=
  integrable_condExp

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

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

Разделы

Аффилиация

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