Commit 2022-09-12 09:20 745e23d5
View on Github →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 ∂μ.
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 ∂μ.