[Merged by Bors] - feat(measure_theory/measure/measure_space): A measurable_equiv is quasi_measure_preserving

src/dynamics/ergodic/measure_preserving.lean

@@ -160,4 +160,11 @@ end
 
 end measure_preserving
 
+namespace measurable_equiv
+
+lemma measure_preserving_symm (μ : measure α) (e : α ≃ᵐ β) :
+  measure_preserving e.symm (map e μ) μ :=
+(e.measurable.measure_preserving μ).symm _
+
+end measurable_equiv
 end measure_theory

src/measure_theory/measure/measure_space.lean

@@ -3736,6 +3736,10 @@ e.measurable_embedding.restrict_map _ _
 lemma map_ae (f : α ≃ᵐ β) (μ : measure α) : filter.map f μ.ae = (map f μ).ae :=
 by { ext s, simp_rw [mem_map, mem_ae_iff, ← preimage_compl, f.map_apply] }
 
+lemma quasi_measure_preserving_symm (μ : measure α) (e : α ≃ᵐ β) :
+  quasi_measure_preserving e.symm (map e μ) μ :=
+⟨e.symm.measurable, by rw [measure.map_map, e.symm_comp_self, measure.map_id]; measurability⟩
+
 end measurable_equiv