Commit 2024-08-29 16:54 92f9ab8b

View on Github →

feat (MeasureTheory.Integral): Generalize lemmas to setIntegral and setLIntegral (#15551) Add versions of existing lemmas for integrals restricted to a set, in particular:

  • setIntegral_rnDeriv_smul.
  • setIntegral_zero_measure.
  • setLIntegral_eq_zero_iff' and setLIntegral_eq_zero_iff.

Estimated changes