English
If hm ≤ m0 and μtrim hm is sigma-finite, then μ[f|m] is expressed as a piecewise object: it equals f when f is integrable and strongly measurable; otherwise it is represented by a measurable modification involving condExpL1.
Русский
При hm ≤ m0 и сигма-конечной мере μtrim hm, условное ожидание μ[f|m] равно f, если f интегрируемо и сильно измеримо; иначе — модификация через condExpL1.
LaTeX
$$$$\\mu[f|m] = \\begin{cases} f, & \\text{if } \\operatorname{Integrable}(f,\\mu) \\ \\text{and} \\ \\operatorname{StronglyMeasurable}(f)\\_m, \\\\[2pt] \\text{AEStronglyMeasurable}(.\\text{condExpL1}) , & \\text{otherwise}. \\end{cases}$$$$
Lean4
theorem condExp_of_sigmaFinite (hm : m ≤ m₀) [hμm : SigmaFinite (μ.trim hm)] :
μ[f|m] =
if Integrable f μ then if StronglyMeasurable[m] f then f else aestronglyMeasurable_condExpL1.mk (condExpL1 hm μ f)
else 0 :=
by
rw [condExp, dif_pos hm]
grind
