conditional_expectation): conditional expectation w.r.t. the restriction of a measure to a set (#14751)

Commit

3 years ago

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]`.

Author

RemyDegenne

Parents

ac2e9dbf

mathlib3 6cefaf4b - feat(measure_theory/function/conditional_expectation): conditional expectation w.r.t. the restriction of a measure to a set (#14751)

mathlib3
6cefaf4b - feat(measure_theory/function/conditional_expectation): conditional expectation w.r.t. the restriction of a measure to a set (#14751)