Commit 2023-06-17 13:45 9191c4ae

View on Github →

feat: port MeasureTheory.Function.ConditionalExpectation.Indicator (#5188)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/ConditionalExpectation/Indicator.lean

added theorem MeasureTheory.condexp_ae_eq_restrict_of_measurableSpace_eq_on

added theorem MeasureTheory.condexp_ae_eq_restrict_zero

added theorem MeasureTheory.condexp_indicator

added theorem MeasureTheory.condexp_indicator_aux

added theorem MeasureTheory.condexp_restrict_ae_eq_restrict