Commit 2024-07-18 07:43 098bb43a

View on Github →

feat(MeasureTheory): adding setLintegral_compl and setIntegral_compl theorems. (#14853) Adding setLintegral_compl and setIntegral_compl theorems for convenience. setIntegral_compl is used immediately to simplify a few lines in Martingale.Convergence.lean.

Estimated changes

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

added theorem MeasureTheory.setLintegral_compl

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

added theorem MeasureTheory.setIntegral_compl

Modified Mathlib/Probability/Martingale/Convergence.lean