feat(measure_theory/measure/measure_space): add formula for `(map f μ…

…).to_outer_measure` (#8714)

src/measure_theory/measure/measure_space.lean

@@ -604,6 +604,14 @@ else 0
   map f μ s = μ (f ⁻¹' s) :=
 by simp [map, dif_pos hf, hs]
 
+lemma map_to_outer_measure {f : α → β} (hf : measurable f) :
+  (map f μ).to_outer_measure = (outer_measure.map f μ.to_outer_measure).trim :=
+begin
+  rw [← trimmed, outer_measure.trim_eq_trim_iff],
+  intros s hs,
+  rw [coe_to_outer_measure, map_apply hf hs, outer_measure.map_apply, coe_to_outer_measure]
+end
+
 theorem map_of_not_measurable {f : α → β} (hf : ¬measurable f) :
   map f μ = 0 :=
 by rw [map, dif_neg hf, linear_map.zero_apply]

src/measure_theory/measure/outer_measure.lean

@@ -1215,6 +1215,14 @@ theorem le_trim_iff {m₁ m₂ : outer_measure α} :
   m₁ ≤ m₂.trim ↔ ∀ s, measurable_set s → m₁ s ≤ m₂ s :=
 le_of_function.trans $ forall_congr $ λ s, le_infi_iff
 
+theorem trim_le_trim_iff {m₁ m₂ : outer_measure α} :
+  m₁.trim ≤ m₂.trim ↔ ∀ s, measurable_set s → m₁ s ≤ m₂ s :=
+le_trim_iff.trans $ forall_congr $ λ s, forall_congr $ λ hs, by rw [trim_eq _ hs]
+
+theorem trim_eq_trim_iff {m₁ m₂ : outer_measure α} :
+  m₁.trim = m₂.trim ↔ ∀ s, measurable_set s → m₁ s = m₂ s :=
+by simp only [le_antisymm_iff, trim_le_trim_iff, forall_and_distrib]
+
 theorem trim_eq_infi (s : set α) : m.trim s = ⨅ t (st : s ⊆ t) (ht : measurable_set t), m t :=
 by { simp only [infi_comm] {single_pass := tt}, exact induced_outer_measure_eq_infi
     measurable_set.Union (λ f _, m.Union_nat f) (λ _ _ _ _ h, m.mono h) s }
@@ -1223,7 +1231,7 @@ theorem trim_eq_infi' (s : set α) : m.trim s = ⨅ t : {t // s ⊆ t ∧ measur
 by simp [infi_subtype, infi_and, trim_eq_infi]
 
 theorem trim_trim (m : outer_measure α) : m.trim.trim = m.trim :=
-le_antisymm (le_trim_iff.2 $ λ s hs, by simp [trim_eq _ hs, le_refl]) (le_trim _)
+trim_eq_trim_iff.2 $ λ s, m.trim_eq
 
 @[simp] theorem trim_zero : (0 : outer_measure α).trim = 0 :=
 ext $ λ s, le_antisymm