condExpL1_undef — Mathlib

English

If f is not integrable with respect to μ, then the L1 conditional expectation condExpL1 hm μ f equals 0.

Русский

Если f не интегрируема по μ, то условное ожидание в L1: condExpL1 hm μ f равно 0.

LaTeX

$$$\text{condExpL1}(hm, μ, f) = 0 \quad\text{if } \neg \mathrm{Integrable}(f, μ)$$$

Lean4

theorem condExpL1_undef (hf : ¬Integrable f μ) : condExpL1 hm μ f = 0 :=
  setToFun_undef (dominatedFinMeasAdditive_condExpInd F' hm μ) hf

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