English
The operator condExpL1 is defined by taking a function f and mapping it to setToFun μ (condExpInd F' hm μ) (dominatedFinMeasAdditive_condExpInd F' hm μ) f; this is the L1 conditional expectation operator.
Русский
Оператор condExpL1 определяется как применение setToFun к f с использованием condExpInd и domination, задавая оператор условного ожидания в L1.
LaTeX
$$$\text{condExpL1}(hm, μ) f = \text{setToFun } \big( μ \big)\big( \text{condExpInd } F' hm μ \big)\big( \text{dominatedFinMeasAdditive_condExpInd } F' hm μ \big) f$$$
Lean4
/-- Conditional expectation of a function, in L1. Its value is 0 if the function is not
integrable. The function-valued `condExp` should be used instead in most cases. -/
def condExpL1 (hm : m ≤ m0) (μ : Measure α) [SigmaFinite (μ.trim hm)] (f : α → F') : α →₁[μ] F' :=
setToFun μ (condExpInd F' hm μ) (dominatedFinMeasAdditive_condExpInd F' hm μ) f
