Commit 2023-07-23 10:55 f8c1566c

refactor: use NeZero for measures (#6048) Assume NeZero μ instead of μ.ae.NeBot everywhere, and sometimes instead of μ ≠ 0.

API changes

• Convex.average_mem, Convex.set_average_mem, ConvexOn.average_mem_epigraph, ConcaveOn.average_mem_hypograph, ConvexOn.map_average_le, ConcaveOn.le_map_average: assume [NeZero μ] instead of μ ≠ 0;
• MeasureTheory.condexp_bot', essSup_const', essInf_const', MeasureTheory.laverage_const, MeasureTheory.laverage_one, MeasureTheory.average_const: assume [NeZero μ] instead of [μ.ae.NeBot]
• MeasureTheory.Measure.measure_ne_zero: replace with an instance;
• remove @[simp] from MeasureTheory.ae_restrict_neBot, use ≠ 0 in the RHS;
• turn MeasureTheory.IsProbabilityMeasure.ae_neBot into a theorem because inferInstance can find it now;
• add instances:
  • [NeZero μ] : NeZero (μ univ);
  • [NeZero (μ s)] : NeZero (μ.restrict s);
  • [NeZero μ] : μ.ae.NeBot;
  • [IsProbabilityMeasure μ] : NeZero μ;
  • [IsFiniteMeasure μ] [NeZero μ] : IsProbabilityMeasure ((μ univ)⁻¹ • μ) this was a theorem MeasureTheory.isProbabilityMeasureSmul assuming μ ≠ 0;