Commit 2023-06-17 18:41 d87b20b7

View on Github →

feat: port MeasureTheory.Function.ConditionalExpectation.Real (#5193)

Estimated changes

Modified Mathlib.lean

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

added theorem MeasureTheory.Integrable.uniformIntegrable_condexp

added theorem MeasureTheory.ae_bdd_condexp_of_ae_bdd

added theorem MeasureTheory.condexp_stronglyMeasurable_mul

added theorem MeasureTheory.condexp_stronglyMeasurable_mul_of_bound

added theorem MeasureTheory.condexp_stronglyMeasurable_mul_of_bound₀

added theorem MeasureTheory.condexp_stronglyMeasurable_mul₀

added theorem MeasureTheory.condexp_stronglyMeasurable_simpleFunc_mul

added theorem MeasureTheory.integral_abs_condexp_le

added theorem MeasureTheory.rnDeriv_ae_eq_condexp

added theorem MeasureTheory.set_integral_abs_condexp_le

added theorem MeasureTheory.snorm_one_condexp_le_snorm