Commit 2022-06-24 09:16 6cefaf4b
View on Github →feat(measure_theory/function/conditional_expectation): conditional expectation w.r.t. the restriction of a measure to a set (#14751)
We prove (μ.restrict s)[f | m] =ᵐ[μ.restrict s] μ[f | m].
feat(measure_theory/function/conditional_expectation): conditional expectation w.r.t. the restriction of a measure to a set (#14751)
We prove (μ.restrict s)[f | m] =ᵐ[μ.restrict s] μ[f | m].