integrable_condExpL1

Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

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

English

If f and g are equal almost everywhere (μ-a.e.), then condExpL1 hm μ f = condExpL1 hm μ g.

Русский

Если f и g равны μ-почти везде, то condExpL1 hm μ f = condExpL1 hm μ g.

LaTeX

$$$f =_{a.e.\ μ} g \Rightarrow condExpL1 hm μ f = condExpL1 hm μ g$$$

Lean4

theorem integrable_condExpL1 (f : α → F') : Integrable (condExpL1 hm μ f) μ :=
  L1.integrable_coeFn _

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

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

Разделы

Аффилиация

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