feat(measure_theory): ext lemmas for measures (#3895)

Add class `sigma_finite`.
Also some cleanup.
Rename `measurable_space.is_measurable` -> `measurable_space.is_measurable'`. This is to avoid name clash with `_root_.is_measurable`, which should almost always be used instead.
define `is_pi_system`.

Author: fpvandoorn

src/data/set/basic.lean

@@ -855,6 +855,9 @@ h.left
 theorem not_mem_of_mem_diff {s t : set α} {x : α} (h : x ∈ s \ t) : x ∉ t :=
 h.right
 
+theorem diff_eq_compl_inter {s t : set α} : s \ t = tᶜ ∩ s :=
+by rw [diff_eq, inter_comm]
+
 theorem nonempty_diff {s t : set α} : (s \ t).nonempty ↔ ¬ (s ⊆ t) :=
 ⟨λ ⟨x, xs, xt⟩, not_subset.2 ⟨x, xs, xt⟩,
   λ h, let ⟨x, xs, xt⟩ := not_subset.1 h in ⟨x, xs, xt⟩⟩
@@ -995,6 +998,12 @@ by rw [union_comm, union_diff_self, union_comm]
 theorem diff_inter_self {a b : set α} : (b \ a) ∩ a = ∅ :=
 by { ext, by simp [iff_def] {contextual:=tt} }
 
+theorem diff_inter_self_eq_diff {s t : set α} : s \ (t ∩ s) = s \ t :=
+by { ext, simp [iff_def] {contextual := tt} }
+
+theorem diff_self_inter {s t : set α} : s \ (s ∩ t) = s \ t :=
+by rw [inter_comm, diff_inter_self_eq_diff]
+
 theorem diff_eq_self {s t : set α} : s \ t = s ↔ t ∩ s ⊆ ∅ :=
 by finish [ext_iff, iff_def, subset_def]
 

src/logic/basic.lean

@@ -168,6 +168,8 @@ into an automated theorem prover for first order logic. -/
 @[class]
 def fact (p : Prop) := p
 
+lemma fact.elim {p : Prop} (h : fact p) : p := h
+
 end miscellany
 
 /-!

src/measure_theory/borel_space.lean

@@ -91,12 +91,12 @@ lemma borel_eq_generate_Iio (α)
 begin
   refine le_antisymm _ (generate_from_le _),
   { rw borel_eq_generate_from_of_subbasis (@order_topology.topology_eq_generate_intervals α _ _ _),
-    have H : ∀ a:α, is_measurable (measurable_space.generate_from (range Iio)) (Iio a) :=
-      λ a, generate_measurable.basic _ ⟨_, rfl⟩,
+    letI : measurable_space α := measurable_space.generate_from (range Iio),
+    have H : ∀ a:α, is_measurable (Iio a) := λ a, generate_measurable.basic _ ⟨_, rfl⟩,
     refine generate_from_le _, rintro _ ⟨a, rfl | rfl⟩; [skip, apply H],
     by_cases h : ∃ a', ∀ b, a < b ↔ a' ≤ b,
     { rcases h with ⟨a', ha'⟩,
-      rw (_ : Ioi a = (Iio a')ᶜ), {exact (H _).compl _},
+      rw (_ : Ioi a = (Iio a')ᶜ), { exact (H _).compl },
       simp [set.ext_iff, ha'] },
     { rcases is_open_Union_countable
         (λ a' : {a' : α // a < a'}, {b | a'.1 < b})
@@ -112,7 +112,7 @@ begin
           lt_of_lt_of_le ax⟩⟩ },
       rw this, resetI,
       apply is_measurable.Union,
-      exact λ _, (H _).compl _ } },
+      exact λ _, (H _).compl } },
   { rw forall_range_iff,
     intro a,
     exact generate_measurable.basic _ is_open_Iio }
@@ -564,8 +564,8 @@ lemma measure_ext_Ioo_rat {μ ν : measure ℝ} [locally_finite_measure μ]
 begin
   refine measure.ext_of_generate_from_of_cover_subset borel_eq_generate_from_Ioo_rat _
     (subset.refl _) _ _ _ _,
-  { simp only [mem_Union, mem_singleton_iff],
-    rintros _ ⟨a₁, b₁, h₁, rfl⟩ _ ⟨a₂, b₂, h₂, rfl⟩ ne,
+  { simp only [is_pi_system, mem_Union, mem_singleton_iff],
+    rintros _ _ ⟨a₁, b₁, h₁, rfl⟩ ⟨a₂, b₂, h₂, rfl⟩ ne,
     simp only [Ioo_inter_Ioo, sup_eq_max, inf_eq_min, ← rat.cast_max, ← rat.cast_min, nonempty_Ioo] at ne ⊢,
     refine ⟨_, _, _, rfl⟩,
     assumption_mod_cast },
@@ -591,8 +591,8 @@ begin
     simp only [mem_Union], rintro ⟨a, b, h, H⟩,
     rw [mem_singleton_iff.1 H],
     rw (set.ext (λ x, _) : Ioo (a:ℝ) b = (⋃c>a, (Iio c)ᶜ) ∩ Iio b),
-    { have hg : ∀q:ℚ, g.is_measurable (Iio q) :=
-        λ q, generate_measurable.basic _ (by simp; exact ⟨_, rfl⟩),
+    { have hg : ∀ q : ℚ, g.is_measurable' (Iio q) :=
+        λ q, generate_measurable.basic (Iio q) (by { simp, exact ⟨_, rfl⟩ }),
       refine @is_measurable.inter _ g _ _ _ (hg _),
       refine @is_measurable.bUnion _ _ g _ _ (countable_encodable _) (λ c h, _),
       exact @is_measurable.compl _ _ g (hg _) },
@@ -602,8 +602,7 @@ begin
         let ⟨c, ac, cx⟩ := exists_rat_btwn h in
         ⟨c, rat.cast_lt.1 ac, le_of_lt cx⟩,
        λ ⟨c, ac, cx⟩, lt_of_lt_of_le (rat.cast_lt.2 ac) cx⟩ } },
-  { simp, rintro r rfl,
-    exact is_open_Iio.is_measurable }
+  { simp, rintro r rfl, exact is_open_Iio.is_measurable }
 end
 
 end real
@@ -695,15 +694,9 @@ begin
       measurable_const }
 end
 
-lemma measurable.ennreal_add {α : Type*} [measurable_space α] {f g : α → ennreal} :
-  measurable f → measurable g → measurable (λa, f a + g a) :=
-begin
-  refine ennreal.measurable_of_measurable_nnreal_nnreal (+) _ _ _,
-  { simp only [ennreal.coe_add.symm],
-    exact ennreal.measurable_coe.comp measurable_add },
-  { simp [measurable_const] },
-  { simp [measurable_const] }
-end
+lemma measurable.ennreal_add {α : Type*} [measurable_space α] {f g : α → ennreal}
+  (hf : measurable f) (hg : measurable g) : measurable (λa, f a + g a) :=
+hf.add hg
 
 lemma measurable.ennreal_sub {α : Type*} [measurable_space α] {f g : α → ennreal} :
   measurable f → measurable g → measurable (λa, f a - g a) :=

src/measure_theory/content.lean

@@ -228,7 +228,7 @@ lemma is_left_invariant_of_content [group G] [topological_group G]
 by convert of_content_preimage h2 (homeomorph.mul_left g) (λ K, h g) A
 
 lemma of_content_caratheodory (A : set G) :
-  (of_content μ h1).caratheodory.is_measurable A ↔ ∀ (U : opens G),
+  (of_content μ h1).caratheodory.is_measurable' A ↔ ∀ (U : opens G),
   of_content μ h1 (U ∩ A) + of_content μ h1 (U \ A) ≤ of_content μ h1 U :=
 begin
   dsimp [opens], rw subtype.forall,

src/measure_theory/haar_measure.lean

@@ -465,7 +465,7 @@ lemma haar_outer_measure_exists_compact {K₀ : positive_compacts G} {U : opens
 outer_measure.of_content_exists_compact echaar_sup_le hU hε
 
 lemma haar_outer_measure_caratheodory {K₀ : positive_compacts G} (A : set G) :
-  (haar_outer_measure K₀).caratheodory.is_measurable A ↔ ∀ (U : opens G),
+  (haar_outer_measure K₀).caratheodory.is_measurable' A ↔ ∀ (U : opens G),
   haar_outer_measure K₀ (U ∩ A) + haar_outer_measure K₀ (U \ A) ≤ haar_outer_measure K₀ U :=
 outer_measure.of_content_caratheodory echaar_sup_le A
 

src/measure_theory/lebesgue_measure.lean

@@ -168,7 +168,7 @@ by rw [← Ico_diff_left, lebesgue_outer.diff_null _ (lebesgue_outer_singleton _
 by rw [← Icc_diff_left, lebesgue_outer.diff_null _ (lebesgue_outer_singleton _), lebesgue_outer_Icc]
 
 lemma is_lebesgue_measurable_Iio {c : ℝ} :
-  lebesgue_outer.caratheodory.is_measurable (Iio c) :=
+  lebesgue_outer.caratheodory.is_measurable' (Iio c) :=
 outer_measure.of_function_caratheodory $ λ t,
 le_infi $ λ a, le_infi $ λ b, le_infi $ λ h, begin
   refine le_trans (add_le_add