Commit 2023-06-14 01:13 3534d848

View on Github →

feat: port MeasureTheory.Function.ConditionalExpectation.Unique (#5008)

Estimated changes

Modified Mathlib.lean

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

added theorem MeasureTheory.Lp.ae_eq_of_forall_set_integral_eq'

added theorem MeasureTheory.Lp.ae_eq_zero_of_forall_set_integral_eq_zero'

added theorem MeasureTheory.ae_eq_of_forall_set_integral_eq_of_sigmaFinite'

added theorem MeasureTheory.integral_norm_le_of_forall_fin_meas_integral_eq

added theorem MeasureTheory.lintegral_nnnorm_le_of_forall_fin_meas_integral_eq

added theorem MeasureTheory.lpMeas.ae_eq_zero_of_forall_set_integral_eq_zero