Theorem MeasureTheory.integral_condexp

Modification history

2024-06-22 12:48
Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
feat(MeasureTheory/Function/ConditionalExpectation): relax `integral_condexp` assumption and add `integral_condexp_indicator` (#13932) …
Modified MeasureTheory.integral_condexpView on Github →
2023-06-17 12:30
Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean
feat: port MeasureTheory.Function.ConditionalExpectation.Basic (#4898)
Added MeasureTheory.integral_condexpView on Github →