Commit 2024-02-21 16:46 f17e2324

refactor(MeasureTheory): redefine ≤ on measures (#10714) Redefine ≤ on MeasureTheory.Measure so that μ ≤ ν ↔ ∀ s, μ s ≤ ν s by definition instead of ∀ s, MeasurableSet s → μ s ≤ ν s.

Reasons

• 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