feat(measure_theory): ext lemmas for measures

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 preferred.

src/data/set/basic.lean

@@ -852,6 +852,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⟩⟩
@@ -986,6 +989,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 } },
   { simp, rintro _ a rfl,
     exact generate_measurable.basic _ is_open_Iio }
 end
@@ -581,8 +581,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 _) },
@@ -592,8 +592,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

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

src/measure_theory/measurable_space.lean

@@ -71,18 +71,18 @@ variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} {ι : Sort x}
 
 /-- A measurable space is a space equipped with a σ-algebra. -/
 structure measurable_space (α : Type u) :=
-(is_measurable : set α → Prop)
-(is_measurable_empty : is_measurable ∅)
-(is_measurable_compl : ∀s, is_measurable s → is_measurable sᶜ)
-(is_measurable_Union : ∀f:ℕ → set α, (∀i, is_measurable (f i)) → is_measurable (⋃i, f i))
+(is_measurable' : set α → Prop)
+(is_measurable_empty : is_measurable' ∅)
+(is_measurable_compl : ∀s, is_measurable' s → is_measurable' sᶜ)
+(is_measurable_Union : ∀f:ℕ → set α, (∀i, is_measurable' (f i)) → is_measurable' (⋃i, f i))
 
 attribute [class] measurable_space
 
 section
 variable [measurable_space α]
 
 /-- `is_measurable s` means that `s` is measurable (in the ambient measure space on `α`) -/
-def is_measurable : set α → Prop := ‹measurable_space α›.is_measurable
+def is_measurable : set α → Prop := ‹measurable_space α›.is_measurable'
 
 @[simp] lemma is_measurable.empty : is_measurable (∅ : set α) :=
 ‹measurable_space α›.is_measurable_empty
@@ -173,11 +173,15 @@ by { by_cases p; simp [h, is_measurable.empty]; apply is_measurable.univ }
 end
 
 @[ext] lemma measurable_space.ext :
-  ∀{m₁ m₂ : measurable_space α}, (∀s:set α, m₁.is_measurable s ↔ m₂.is_measurable s) → m₁ = m₂
+  ∀{m₁ m₂ : measurable_space α}, (∀s:set α, m₁.is_measurable' s ↔ m₂.is_measurable' s) → m₁ = m₂
 | ⟨s₁, _, _, _⟩ ⟨s₂, _, _, _⟩ h :=
   have s₁ = s₂, from funext $ assume x, propext $ h x,
   by subst this
 
+@[ext] lemma measurable_space.ext_iff {m₁ m₂ : measurable_space α} :
+  m₁ = m₂ ↔ (∀s:set α, m₁.is_measurable' s ↔ m₂.is_measurable' s) :=
+⟨by { unfreezingI {rintro rfl}, intro s, refl }, measurable_space.ext⟩
+
 /-- A typeclass mixin for `measurable_space`s such that each singleton is measurable. -/
 class measurable_singleton_class (α : Type*) [measurable_space α] : Prop :=
 (is_measurable_singleton : ∀ x, is_measurable ({x} : set α))
@@ -216,7 +220,7 @@ namespace measurable_space
 section complete_lattice
 
 instance : partial_order (measurable_space α) :=
-{ le          := λm₁ m₂, m₁.is_measurable ≤ m₂.is_measurable,
+{ le          := λm₁ m₂, m₁.is_measurable' ≤ m₂.is_measurable',
   le_refl     := assume a b, le_refl _,
   le_trans    := assume a b c, le_trans,
   le_antisymm := assume a b h₁ h₂, measurable_space.ext $ assume s, ⟨h₁ s, h₂ s⟩ }
@@ -230,49 +234,49 @@ inductive generate_measurable (s : set (set α)) : set α → Prop
 
 /-- Construct the smallest measure space containing a collection of basic sets -/
 def generate_from (s : set (set α)) : measurable_space α :=
-{ is_measurable       := generate_measurable s,
+{ is_measurable'      := generate_measurable s,
   is_measurable_empty := generate_measurable.empty,
   is_measurable_compl := generate_measurable.compl,
   is_measurable_Union := generate_measurable.union }
 
 lemma is_measurable_generate_from {s : set (set α)} {t : set α} (ht : t ∈ s) :
-  (generate_from s).is_measurable t :=
+  (generate_from s).is_measurable' t :=
 generate_measurable.basic t ht
 
-lemma generate_from_le {s : set (set α)} {m : measurable_space α} (h : ∀t∈s, m.is_measurable t) :
+lemma generate_from_le {s : set (set α)} {m : measurable_space α} (h : ∀t∈s, m.is_measurable' t) :
   generate_from s ≤ m :=
 assume t (ht : generate_measurable s t), ht.rec_on h
   (is_measurable_empty m)
   (assume s _ hs, is_measurable_compl m s hs)
   (assume f _ hf, is_measurable_Union m f hf)
 
-lemma generate_from_le_iff {s : set (set α)} {m : measurable_space α} :
-  generate_from s ≤ m ↔ s ⊆ {t | m.is_measurable t} :=
+lemma generate_from_le_iff {s : set (set α)} (m : measurable_space α) :
+  generate_from s ≤ m ↔ s ⊆ {t | m.is_measurable' t} :=
 iff.intro
   (assume h u hu, h _ $ is_measurable_generate_from hu)
   (assume h, generate_from_le h)
 
 /-- If `g` is a collection of subsets of `α` such that the `σ`-algebra generated from `g` contains the
   same sets as `g`, then `g` was already a `σ`-algebra. -/
-protected def mk_of_closure (g : set (set α)) (hg : {t | (generate_from g).is_measurable t} = g) :
+protected def mk_of_closure (g : set (set α)) (hg : {t | (generate_from g).is_measurable' t} = g) :
   measurable_space α :=
-{ is_measurable := λs, s ∈ g,
+{ is_measurable'      := λs, s ∈ g,
   is_measurable_empty := hg ▸ is_measurable_empty _,
   is_measurable_compl := hg ▸ is_measurable_compl _,
   is_measurable_Union := hg ▸ is_measurable_Union _ }
 
 lemma mk_of_closure_sets {s : set (set α)}
-  {hs : {t | (generate_from s).is_measurable t} = s} :
+  {hs : {t | (generate_from s).is_measurable' t} = s} :
   measurable_space.mk_of_closure s hs = generate_from s :=
 measurable_space.ext $ assume t, show t ∈ s ↔ _, by { conv_lhs { rw [← hs] }, refl }
 
 /-- We get a Galois insertion between `σ`-algebras on `α` and `set (set α)` by using `generate_from`
   on one side and the collection of measurable sets on the other side. -/
 def gi_generate_from : galois_insertion (@generate_from α) (λm, {t | @is_measurable α m t}) :=
-{ gc        := assume s m, generate_from_le_iff,
+{ gc        := assume s, generate_from_le_iff,
   le_l_u    := assume m s, is_measurable_generate_from,
   choice    :=
-    λg hg, measurable_space.mk_of_closure g $ le_antisymm hg $ generate_from_le_iff.1 $ le_refl _,
+    λg hg, measurable_space.mk_of_closure g $ le_antisymm hg $ (generate_from_le_iff _).1 le_rfl,
   choice_eq := assume g hg, mk_of_closure_sets }
 
 instance : complete_lattice (measurable_space α) :=
@@ -282,7 +286,7 @@ instance : inhabited (measurable_space α) := ⟨⊤⟩
 
 lemma is_measurable_bot_iff {s : set α} : @is_measurable α ⊥ s ↔ (s = ∅ ∨ s = univ) :=
 let b : measurable_space α :=
-{ is_measurable       := λs, s = ∅ ∨ s = univ,
+{ is_measurable'      := λs, s = ∅ ∨ s = univ,
   is_measurable_empty := or.inl rfl,
   is_measurable_compl := by simp [or_imp_distrib] {contextual := tt},
   is_measurable_Union := assume f hf, classical.by_cases
@@ -312,22 +316,22 @@ show s ∈ (λm, {s | @is_measurable _ m s }) (infi m) ↔ _,
 by { rw (@gi_generate_from α).gc.u_infi, simp }
 
 theorem is_measurable_sup {m₁ m₂ : measurable_space α} {s : set α} :
-  @is_measurable _ (m₁ ⊔ m₂) s ↔ generate_measurable (m₁.is_measurable ∪ m₂.is_measurable) s :=
+  @is_measurable _ (m₁ ⊔ m₂) s ↔ generate_measurable (m₁.is_measurable' ∪ m₂.is_measurable') s :=
 iff.refl _
 
 theorem is_measurable_Sup {ms : set (measurable_space α)} {s : set α} :
-  @is_measurable _ (Sup ms) s ↔ generate_measurable (⋃₀ (measurable_space.is_measurable '' ms)) s :=
+  @is_measurable _ (Sup ms) s ↔ generate_measurable (⋃₀ (measurable_space.is_measurable' '' ms)) s :=
 begin
-  change @is_measurable _ (generate_from _) _ ↔ _,
+  change @is_measurable' _ (generate_from _) _ ↔ _,
   dsimp [generate_from],
-  rw (show (⨆ (b : measurable_space α) (H : b ∈ ms), set_of (is_measurable b)) = (⋃₀(is_measurable '' ms)),
+  rw (show (⨆ (b : measurable_space α) (H : b ∈ ms), set_of (@is_measurable _ b)) = (⋃₀ (is_measurable' '' ms)),
   { ext,
     simp only [exists_prop, mem_Union, sUnion_image, mem_set_of_eq],
     refl, })
 end
 
 theorem is_measurable_supr {ι} {m : ι → measurable_space α} {s : set α} :
-  @is_measurable _ (supr m) s ↔ generate_measurable (⋃i, (m i).is_measurable) s :=
+  @is_measurable _ (supr m) s ↔ generate_measurable (⋃i, (m i).is_measurable') s :=
 begin
   convert @is_measurable_Sup _ (range m) s,
   simp,
@@ -341,7 +345,7 @@ variables {m m₁ m₂ : measurable_space α} {m' : measurable_space β} {f : α
 /-- The forward image of a measure space under a function. `map f m` contains the sets `s : set β`
   whose preimage under `f` is measurable. -/
 protected def map (f : α → β) (m : measurable_space α) : measurable_space β :=
-{ is_measurable       := λs, m.is_measurable $ f ⁻¹' s,
+{ is_measurable'      := λs, m.is_measurable' $ f ⁻¹' s,
   is_measurable_empty := m.is_measurable_empty,
   is_measurable_compl := assume s hs, m.is_measurable_compl _ hs,
   is_measurable_Union := assume f hf, by { rw [preimage_Union], exact m.is_measurable_Union _ hf }}
@@ -355,7 +359,7 @@ measurable_space.ext $ assume s, iff.rfl
 /-- The reverse image of a measure space under a function. `comap f m` contains the sets `s : set α`
   such that `s` is the `f`-preimage of a measurable set in `β`. -/
 protected def comap (f : α → β) (m : measurable_space β) : measurable_space α :=
-{ is_measurable       := λs, ∃s', m.is_measurable s' ∧ f ⁻¹' s' = s,
+{ is_measurable'      := λs, ∃s', m.is_measurable' s' ∧ f ⁻¹' s' = s,
   is_measurable_empty := ⟨∅, m.is_measurable_empty, rfl⟩,
   is_measurable_compl := assume s ⟨s', h₁, h₂⟩, ⟨s'ᶜ, m.is_measurable_compl _ h₁, h₂ ▸ rfl⟩,
   is_measurable_Union := assume s hs,
@@ -932,6 +936,8 @@ namespace measurable_space
 
   The main purpose of Dynkin systems is to provide a powerful induction rule for σ-algebras
   generated by intersection stable set systems.
+
+  A Dynkin system is also known as a "λ-system" or a "d-system".
 -/
 structure dynkin_system (α : Type*) :=
 (has : set α → Prop)
@@ -978,7 +984,7 @@ instance : partial_order (dynkin_system α) :=
 
 /-- Every measurable space (σ-algebra) forms a Dynkin system -/
 def of_measurable_space (m : measurable_space α) : dynkin_system α :=
-{ has       := m.is_measurable,
+{ has       := m.is_measurable',
   has_empty := m.is_measurable_empty,
   has_compl := m.is_measurable_compl,
   has_Union_nat := assume f _ hf, m.is_measurable_Union f hf }
@@ -996,19 +1002,24 @@ inductive generate_has (s : set (set α)) : set α → Prop
 | Union : ∀{f:ℕ → set α}, pairwise (disjoint on f) →
     (∀i, generate_has (f i)) → generate_has (⋃i, f i)
 
+lemma generate_has_compl {C : set (set α)} {s : set α} : generate_has C sᶜ ↔ generate_has C s :=
+by { refine ⟨_, generate_has.compl⟩, intro h, convert generate_has.compl h, simp }
+
 /-- The least Dynkin system containing a collection of basic sets. -/
 def generate (s : set (set α)) : dynkin_system α :=
 { has := generate_has s,
   has_empty := generate_has.empty,
   has_compl := assume a, generate_has.compl,
   has_Union_nat := assume f, generate_has.Union }
 
+lemma generate_has_def {C : set (set α)} : (generate C).has = generate_has C := rfl
+
 instance : inhabited (dynkin_system α) := ⟨generate univ⟩
 
 /-- If a Dynkin system is closed under binary intersection, then it forms a `σ`-algebra. -/
 def to_measurable_space (h_inter : ∀s₁ s₂, d.has s₁ → d.has s₂ → d.has (s₁ ∩ s₂)) :=
 { measurable_space .
-  is_measurable := d.has,
+  is_measurable'      := d.has,
   is_measurable_empty := d.has_empty,
   is_measurable_compl := assume s h, d.has_compl h,
   is_measurable_Union := assume f hf,
@@ -1045,6 +1056,10 @@ lemma generate_le {s : set (set α)} (h : ∀t∈s, d.has t) : generate s ≤ d
   (assume a _ h, d.has_compl h)
   (assume f hd _ hf, d.has_Union hd hf)
 
+lemma generate_has_subset_generate_measurable {C : set (set α)} {s : set α}
+  (hs : (generate C).has s) : (generate_from C).is_measurable' s :=
+generate_le (of_measurable_space (generate_from C)) (λ t, is_measurable_generate_from) s hs
+
 lemma generate_inter {s : set (set α)}
   (hs : ∀ (t₁ ∈ s) (t₂ ∈ s), (t₁ ∩ t₂ : set α).nonempty → t₁ ∩ t₂ ∈ s) {t₁ t₂ : set α}
   (ht₁ : (generate s).has t₁) (ht₂ : (generate s).has t₂) : (generate s).has (t₁ ∩ t₂) :=
@@ -1061,9 +1076,15 @@ have generate s ≤ (generate s).restrict_on ht₂,
   show (generate s).has (s₁ ∩ t₂), by rwa [inter_comm],
 this _ ht₁
 
+/--
+  If we have a collection of sets closed under binary intersections, then the Dynkin system it
+  generates is equal to the σ-algebra it generates.
+  This result is known as the π-λ theorem.
+  A collection of sets closed under binary intersection is called a "π-system" if it is non-empty.
+-/
 lemma generate_from_eq {s : set (set α)}
   (hs : ∀ (t₁ ∈ s) (t₂ ∈ s), (t₁ ∩ t₂ : set α).nonempty → t₁ ∩ t₂ ∈ s) :
-generate_from s = (generate s).to_measurable_space (assume t₁ t₂, generate_inter hs) :=
+  generate_from s = (generate s).to_measurable_space (assume t₁ t₂, generate_inter hs) :=
 le_antisymm
   (generate_from_le $ assume t ht, generate_has.basic t ht)
   (of_measurable_space_le_of_measurable_space_iff.mp $
@@ -1072,13 +1093,13 @@ le_antisymm
 
 end dynkin_system
 
-lemma induction_on_inter {C : set α → Prop} {s : set (set α)} {m : measurable_space α}
+lemma induction_on_inter {C : set α → Prop} {s : set (set α)} [m : measurable_space α]
   (h_eq : m = generate_from s)
   (h_inter : ∀ (t₁ ∈ s) (t₂ ∈ s), (t₁ ∩ t₂ : set α).nonempty → t₁ ∩ t₂ ∈ s)
-  (h_empty : C ∅) (h_basic : ∀t∈s, C t) (h_compl : ∀t, m.is_measurable t → C t → C tᶜ)
-  (h_union : ∀f:ℕ → set α, (pairwise (disjoint on f)) →
-    (∀i, m.is_measurable (f i)) → (∀i, C (f i)) → C (⋃i, f i)) :
-  ∀{t}, m.is_measurable t → C t :=
+  (h_empty : C ∅) (h_basic : ∀t∈s, C t) (h_compl : ∀t, is_measurable t → C t → C tᶜ)
+  (h_union : ∀f:ℕ → set α, pairwise (disjoint on f) →
+    (∀i, is_measurable (f i)) → (∀i, C (f i)) → C (⋃i, f i)) :
+  ∀{t}, is_measurable t → C t :=
 have eq : m.is_measurable = dynkin_system.generate_has s,
   by { rw [h_eq, dynkin_system.generate_from_eq h_inter], refl },
 assume t ht,