Commits on Feb 19, 2024

1. refactor(MeasureTheory): redefine ≤ on measures …

   Redefine `≤` on `MeasureTheory.Measure`
   so that `μ ≤ ν ↔ ∀ s, μ s ≤ ν s` by definition
   instead of `∀ s, MeasurableSet s → μ s ≤ ν s`.
   
   The reasons are:
   
   - this way it is defeq to `≤` on outer measures;
   - if we decide to introduce an order on all `DFunLike` types
     **and** migrate measures to `FunLike`, then this is unavoidable;
   - the reasoning for the old definition was
     "it's slightly easier to prove `μ ≤ ν` this way";
     the counter-argument is
     "it's slightly harder to apply `μ ≤ ν` this way".
   
   Other changes
   
   - golf some proofs broken by this change;
   - add `@[gcongr]` tags to some `ENNReal` lemmas;
   - fix the name
     `ENNReal.coe_lt_coe_of_le` -> `ENNReal.ENNReal.coe_lt_coe_of_lt`;
   - drop an unneeded `MeasurableSet` assumption
     in `set_lintegral_pdf_le_map`

   

   urkud committed Feb 19, 2024
   Configuration menu

   • View commit details
   • Copy full SHA for f72bd11
   • Browse repository at this point

   Copy the full SHA

   f72bd11 View commit details

   Browse the repository at this point in the history