condExpL1_eq

Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

URI: https://scilib.ai/kg/mathlib#MeasureTheory.condExpL1_eq

← MathLib Explorer

English

The conditional expectation of the zero function is zero: condExpL1 hm μ (0) = 0.

Русский

Условное ожидание нулевой функции равно нулю: condExpL1 hm μ (0) = 0.

LaTeX

$$$condExpL1 hm μ (0) = 0$$$

Lean4

theorem condExpL1_eq (hf : Integrable f μ) : condExpL1 hm μ f = condExpL1CLM F' hm μ (hf.toL1 f) :=
  setToFun_eq (dominatedFinMeasAdditive_condExpInd F' hm μ) hf

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

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

Разделы

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

Аффилиация

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