feat(measure_theory/measure): add lemmas, drop measurable_set assum…

…ptions (#11499)

* `restrict_eq_self` no longer requires measurability of either set;
* `restrict_apply_self` no longer requires measurability of the set;
* add `restrict_apply_superset` and `restrict_restrict_of_subset` ;
* add `restrict_restrict'` that assumes measurability of the other
  set, drop one `measurable_set` assumption in `restrict_comm`;
* drop measurability assumptions in `restrict_congr_mono`.

src/measure_theory/integral/lebesgue.lean

@@ -2106,7 +2106,7 @@ lemma with_density_indicator {s : set α} (hs : measurable_set s) (f : α → 
 begin
   ext1 t ht,
   rw [with_density_apply _ ht, lintegral_indicator _ hs,
-      restrict_comm hs ht, ← with_density_apply _ ht]
+      restrict_comm hs, ← with_density_apply _ ht]
 end
 
 lemma with_density_of_real_mutually_singular {f : α → ℝ} (hf : measurable f) :

src/measure_theory/measure/lebesgue.lean

@@ -491,10 +491,9 @@ begin
       ← volume_region_between_eq_lintegral' hf.measurable_mk hg.measurable_mk hs],
   convert h₂ using 1,
   { rw measure.restrict_prod_eq_prod_univ,
-    exact (measure.restrict_eq_self' (hs.prod measurable_set.univ)
-      (region_between_subset f g s)).symm, },
+    exact (measure.restrict_eq_self _ (region_between_subset f g s)).symm, },
   { rw measure.restrict_prod_eq_prod_univ,
-    exact (measure.restrict_eq_self' (hs.prod measurable_set.univ)
+    exact (measure.restrict_eq_self _
       (region_between_subset (ae_measurable.mk f hf) (ae_measurable.mk g hg) s)).symm },
 end
 

src/measure_theory/measure/measure_space.lean

@@ -869,22 +869,37 @@ the measure to `s` equals the outer measure of `t ∩ s`. This is an alternate v
 by rw [← coe_to_outer_measure, measure.restrict_to_outer_measure_eq_to_outer_measure_restrict hs,
       outer_measure.restrict_apply s t _, coe_to_outer_measure]
 
-lemma restrict_eq_self' (hs : measurable_set s) (t_subset : t ⊆ s) :
-  μ.restrict s t = μ t :=
-by rw [restrict_apply' hs, set.inter_eq_self_of_subset_left t_subset]
+lemma restrict_le_self : μ.restrict s ≤ μ :=
+assume t ht,
+calc μ.restrict s t = μ (t ∩ s) : restrict_apply ht
+... ≤ μ t : measure_mono $ inter_subset_left t s
+
+variable (μ)
+
+lemma restrict_eq_self (h : s ⊆ t) : μ.restrict t s = μ s :=
+(le_iff'.1 restrict_le_self s).antisymm $
+calc μ s ≤ μ (to_measurable (μ.restrict t) s ∩ t) :
+  measure_mono (subset_inter (subset_to_measurable _ _) h)
+... =  μ.restrict t s :
+  by rw [← restrict_apply (measurable_set_to_measurable _ _), measure_to_measurable]
 
-lemma restrict_eq_self (h_meas_t : measurable_set t) (h : t ⊆ s) : μ.restrict s t = μ t :=
-by rw [restrict_apply h_meas_t, inter_eq_left_iff_subset.mpr h]
+@[simp] lemma restrict_apply_self (s : set α):
+  (μ.restrict s) s = μ s :=
+restrict_eq_self μ subset.rfl
 
-lemma restrict_apply_self {m0 : measurable_space α} (μ : measure α) (h_meas_s : measurable_set s) :
-  (μ.restrict s) s = μ s := (restrict_eq_self h_meas_s (set.subset.refl _))
+variable {μ}
 
 lemma restrict_apply_univ (s : set α) : μ.restrict s univ = μ s :=
 by rw [restrict_apply measurable_set.univ, set.univ_inter]
 
 lemma le_restrict_apply (s t : set α) :
   μ (t ∩ s) ≤ μ.restrict s t :=
-by { rw [restrict, restrictₗ], convert le_lift_linear_apply _ t, simp }
+calc μ (t ∩ s) = μ.restrict s (t ∩ s) : (restrict_eq_self μ (inter_subset_right _ _)).symm
+... ≤ μ.restrict s t : measure_mono (inter_subset_left _ _)
+
+lemma restrict_apply_superset (h : s ⊆ t) : μ.restrict s t = μ s :=
+((measure_mono (subset_univ _)).trans_eq $ restrict_apply_univ _).antisymm
+  ((restrict_apply_self μ s).symm.trans_le $ measure_mono h)
 
 @[simp] lemma restrict_add {m0 : measurable_space α} (μ ν : measure α) (s : set α) :
   (μ + ν).restrict s = μ.restrict s + ν.restrict s :=
@@ -902,9 +917,21 @@ by { rw [restrict, restrictₗ], convert le_lift_linear_apply _ t, simp }
   (μ.restrict t).restrict s = μ.restrict (s ∩ t) :=
 ext $ λ u hu, by simp [*, set.inter_assoc]
 
-lemma restrict_comm (hs : measurable_set s) (ht : measurable_set t) :
+lemma restrict_restrict_of_subset (h : s ⊆ t) :
+  (μ.restrict t).restrict s = μ.restrict s :=
+begin
+  ext1 u hu,
+  rw [restrict_apply hu, restrict_apply hu, restrict_eq_self],
+  exact (inter_subset_right _ _).trans h
+end
+
+lemma restrict_restrict' (ht : measurable_set t) :
+  (μ.restrict t).restrict s = μ.restrict (s ∩ t) :=
+ext $ λ u hu, by simp [*, set.inter_assoc]
+
+lemma restrict_comm (hs : measurable_set s) :
   (μ.restrict t).restrict s = (μ.restrict s).restrict t :=
-by rw [restrict_restrict hs, restrict_restrict ht, inter_comm]
+by rw [restrict_restrict hs, restrict_restrict' hs, inter_comm]
 
 lemma restrict_apply_eq_zero (ht : measurable_set t) : μ.restrict s t = 0 ↔ μ (t ∩ s) = 0 :=
 by rw [restrict_apply ht]
@@ -920,7 +947,7 @@ by rw [← measure_univ_eq_zero, restrict_apply_univ]
 
 lemma restrict_zero_set {s : set α} (h : μ s = 0) :
   μ.restrict s = 0 :=
-by simp only [measure.restrict_eq_zero, h]
+by rw [measure.restrict_eq_zero, h]
 
 @[simp] lemma restrict_empty : μ.restrict ∅ = 0 := restrict_zero_set measure_empty
 
@@ -1008,11 +1035,6 @@ calc μ.restrict s t = μ (t ∩ s) : restrict_apply ht
   μ.restrict s ≤ ν.restrict s' :=
 restrict_mono' (ae_of_all _ hs) hμν
 
-lemma restrict_le_self : μ.restrict s ≤ μ :=
-assume t ht,
-calc μ.restrict s t = μ (t ∩ s) : restrict_apply ht
-... ≤ μ t : measure_mono $ inter_subset_left t s
-
 lemma restrict_mono_ae (h : s ≤ᵐ[μ] t) : μ.restrict s ≤ μ.restrict t :=
 restrict_mono' h (le_refl μ)
 
@@ -1032,18 +1054,18 @@ lemma restrict_congr_meas (hs : measurable_set s) :
  λ H, ext $ λ t ht,
    by rw [restrict_apply ht, restrict_apply ht, H _ (inter_subset_right _ _) (ht.inter hs)]⟩
 
-lemma restrict_congr_mono (hs : s ⊆ t) (hm : measurable_set s) (h : μ.restrict t = ν.restrict t) :
+lemma restrict_congr_mono (hs : s ⊆ t) (h : μ.restrict t = ν.restrict t) :
   μ.restrict s = ν.restrict s :=
-by rw [← inter_eq_self_of_subset_left hs, ← restrict_restrict hm, h, restrict_restrict hm]
+by rw [← restrict_restrict_of_subset hs, h, restrict_restrict_of_subset hs]
 
 /-- If two measures agree on all measurable subsets of `s` and `t`, then they agree on all
 measurable subsets of `s ∪ t`. -/
 lemma restrict_union_congr (hsm : measurable_set s) (htm : measurable_set t) :
   μ.restrict (s ∪ t) = ν.restrict (s ∪ t) ↔
     μ.restrict s = ν.restrict s ∧ μ.restrict t = ν.restrict t :=
 begin
-  refine ⟨λ h, ⟨restrict_congr_mono (subset_union_left _ _) hsm h,
-    restrict_congr_mono (subset_union_right _ _) htm h⟩, _⟩,
+  refine ⟨λ h, ⟨restrict_congr_mono (subset_union_left _ _) h,
+    restrict_congr_mono (subset_union_right _ _) h⟩, _⟩,
   simp only [restrict_congr_meas, hsm, htm, hsm.union htm],
   rintros ⟨hs, ht⟩ u hu hum,
   rw [← measure_inter_add_diff u hsm, ← measure_inter_add_diff u hsm,
@@ -1067,7 +1089,7 @@ lemma restrict_Union_congr [encodable ι] {s : ι → set α} (hm : ∀ i, measu
   μ.restrict (⋃ i, s i) = ν.restrict (⋃ i, s i) ↔
     ∀ i, μ.restrict (s i) = ν.restrict (s i) :=
 begin
-  refine ⟨λ h i, restrict_congr_mono (subset_Union _ _) (hm i) h, λ h, _⟩,
+  refine ⟨λ h i, restrict_congr_mono (subset_Union _ _) h, λ h, _⟩,
   ext1 t ht,
   have M : ∀ t : finset ι, measurable_set (⋃ i ∈ t, s i) :=
     λ t, t.measurable_set_bUnion (λ i _, hm i),
@@ -2532,8 +2554,8 @@ begin
         { rw add_apply,
           apply le_add_right _,
           rw add_apply,
-          rw ← @restrict_eq_self _ _ μ s _ h_meas_t_inter_s (set.inter_subset_right _ _),
-          rw ← @restrict_eq_self _ _ ν s _ h_meas_t_inter_s (set.inter_subset_right _ _),
+          rw [← restrict_eq_self μ (set.inter_subset_right _ _),
+            ← restrict_eq_self ν (set.inter_subset_right _ _)],
           apply h_ν'_in _ h_meas_t_inter_s },
         { rw add_apply,
           have h_meas_inter_compl :=
@@ -2560,11 +2582,7 @@ end
 lemma sub_apply_eq_zero_of_restrict_le_restrict
   (h_le : μ.restrict s ≤ ν.restrict s) (h_meas_s : measurable_set s) :
   (μ - ν) s = 0 :=
-begin
-  rw [← restrict_apply_self _ h_meas_s, restrict_sub_eq_restrict_sub_restrict,
-      sub_eq_zero_of_le],
-  repeat {simp [*]},
-end
+by rw [← restrict_apply_self, restrict_sub_eq_restrict_sub_restrict, sub_eq_zero_of_le]; simp *
 
 instance is_finite_measure_sub [is_finite_measure μ] : is_finite_measure (μ - ν) :=
 { measure_univ_lt_top := lt_of_le_of_lt