Commit 2021-03-16 21:43 890066ac

feat(measure_theory/measure_space): define quasi_measure_preserving (#6699)

• add measurable.iterate
• move section about measure_space up to make volume_tac available much earlier;
• add map_of_not_measurable;
• drop assumption measurable f in map_mono;
• add tendsto_ae_map;
• more API about absolutely_continuous;
• define quasi_measure_preserving and prove some properties.