mathlib

745e23d5 - feat(measure_theory/function/conditional_expectation): conditional expectation with respect to the bot sigma algebra (#16342)

feat(measure_theory/function/conditional_expectation): conditional expectation with respect to the bot sigma algebra (#16342) Prove that for a probability measure, `μ[f|⊥] = λ _, ∫ x, f x ∂μ`. Co-authored-by: RemyDegenne <remydegenne@gmail.com>