condExpIndL1_of_measure_eq_top

Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

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

← MathLib Explorer

English

If s is not measurable, condExpIndL1 hm μ s x equals 0.

Русский

Если s не измеримо, condExpIndL1 hm μ s x равно 0.

LaTeX

$$condExpIndL1_of_not_measurableSet hm μ s x = 0$$

Lean4

theorem condExpIndL1_of_measure_eq_top (hμs : μ s = ∞) (x : G) : condExpIndL1 hm μ s x = 0 := by
  simp only [condExpIndL1, hμs, not_true, Ne, dif_neg, not_false_iff, and_false]

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

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

Разделы

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

Аффилиация

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