Commit 2024-06-22 12:48 e19c07e6
View on Github →feat(MeasureTheory/Function/ConditionalExpectation): relax integral_condexp assumption and add integral_condexp_indicator (#13932)
Remove the Integrable assumption of integral_condexp and add the total probability law using condexp as conditional probability.