condExpL1_neg

Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1

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

English

If f and g are integrable, then condExpL1 hm μ (f−g) = condExpL1 hm μ f − condExpL1 hm μ g.

Русский

Если f и g интегрируемы, то condExpL1 hm μ (f−g) = condExpL1 hm μ f − condExpL1 hm μ g.

LaTeX

$$$condExpL1 hm μ (f-g) = condExpL1 hm μ f - condExpL1 hm μ g$$$

Lean4

theorem condExpL1_neg (f : α → F') : condExpL1 hm μ (-f) = -condExpL1 hm μ f :=
  setToFun_neg _ f

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

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

Разделы

Аффилиация

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