Commit 2021-01-14 19:06 0817e7fe

feat(measure_theory): absolute continuity of the integral (#5743)

API changes:

ennreals and nnreals:

• ennreal.mul_le_mul and ennreal.mul_lt_mul are now mono lemmas;
• rename ennreal.sub_lt_sub_self to ennreal.sub_lt_self: there is no - in the RHS;
• new lemmas enrneal.mul_div_le, nnreal.sub_add_eq_max, and nnreal.add_sub_eq_max;
• add new lemma ennreal.bsupr_add, use in in the proof of ennreal.Sup_add;

Complete lattice

• new lemma supr_lt_iff;

Simple functions

• new lemmas simple_func.exists_forall_le, simple_func.map_add, simple_func.sub_apply;
• weaker typeclass assumptions in simple_func.coe_sub;
• monotone_eapprox is now a mono lemma;

Integration

• new lemmas exists_simple_func_forall_lintegral_sub_lt_of_pos, exists_pos_set_lintegral_lt_of_measure_lt, tendsto_set_lintegral_zero, and has_finite_integral.tendsto_set_integral_nhds_zero.