condExpIndL1_of_measurableSet_of_measure_ne_top

Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

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

← MathLib Explorer

English

If μ[s] = ∞, then condExpIndL1 hm μ s x equals 0.

Русский

Если μ[s] = ∞, condExpIndL1 hm μ s x = 0.

LaTeX

$$condExpIndL1_of_measure_eq_top hm μ s x = 0$$

Lean4

theorem condExpIndL1_of_measurableSet_of_measure_ne_top (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : G) :
    condExpIndL1 hm μ s x = condExpIndL1Fin hm hs hμs x := by
  simp only [condExpIndL1, And.intro hs hμs, dif_pos, Ne, not_false_iff, and_self_iff]

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

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

Разделы

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

Аффилиация

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