feat(measure_theory): cleanup and generalize measure' (#3648)

There were two functions `measure'` and `outer_measure'` with undescriptive names, and which were not very general

rename `measure'` -> `extend`
rename `outer_measure'` -> `induced_outer_measure`
generalize both `extend` and `induced_outer_measure` to an arbitrary subset of `set α` (instead of just the measurable sets). Most lemmas still hold in full generality, sometimes with a couple more assumptions. For the lemmas that need more assumptions, we have also kept the version that is just for `is_measurable`.
Move functions `extend`, `induced_outer_measure` and `trim` to `outer_measure.lean`.
rename `caratheodory_is_measurable` -> `of_function_caratheodory`
rename `trim_ge` -> `le_trim`
Make the section on caratheodory sets not private (and give a more descriptive name to lemmas).
Style in `measurable_space` and `outer_measure`

Author: fpvandoorn

src/data/equiv/basic.lean

@@ -17,6 +17,7 @@ universes u v w z
 variables {α : Sort u} {β : Sort v} {γ : Sort w}
 
 /-- `α ≃ β` is the type of functions from `α → β` with a two-sided inverse. -/
+@[nolint inhabited]
 structure equiv (α : Sort*) (β : Sort*) :=
 (to_fun    : α → β)
 (inv_fun   : β → α)
@@ -1198,6 +1199,14 @@ equiv.set.image_of_inj_on f s (λ x y hx hy hxy, H hxy)
 @[simp] theorem image_apply {α β} (f : α → β) (s : set α) (H : injective f) (a h) :
   set.image f s H ⟨a, h⟩ = ⟨f a, mem_image_of_mem _ h⟩ := rfl
 
+lemma image_symm_preimage {α β} {f : α → β} (hf : injective f) (u s : set α) :
+  (λ x, (set.image f s hf).symm x : f '' s → α) ⁻¹' u = coe ⁻¹' (f '' u) :=
+begin
+  ext ⟨b, a, has, rfl⟩,
+  have : ∀(h : ∃a', a' ∈ s ∧ a' = a), classical.some h = a := λ h, (classical.some_spec h).2,
+  simp [equiv.set.image, equiv.set.image_of_inj_on, hf, this],
+end
+
 /-- If `f : α → β` is an injective function, then `α` is equivalent to the range of `f`. -/
 protected noncomputable def range {α β} (f : α → β) (H : injective f) :
   α ≃ range f :=

src/measure_theory/lebesgue_measure.lean

@@ -90,7 +90,7 @@ def lebesgue_outer : outer_measure ℝ :=
 outer_measure.of_function lebesgue_length lebesgue_length_empty
 
 lemma lebesgue_outer_le_length (s : set ℝ) : lebesgue_outer s ≤ lebesgue_length s :=
-outer_measure.of_function_le _ _ _
+outer_measure.of_function_le _
 
 lemma lebesgue_length_subadditive {a b : ℝ} {c d : ℕ → ℝ}
   (ss : Icc a b ⊆ ⋃i, Ioo (c i) (d i)) :
@@ -176,7 +176,7 @@ end
 
 lemma is_lebesgue_measurable_Iio {c : ℝ} :
   lebesgue_outer.caratheodory.is_measurable (Iio c) :=
-outer_measure.caratheodory_is_measurable $ λ t,
+outer_measure.of_function_caratheodory $ λ t,
 le_infi $ λ a, le_infi $ λ b, le_infi $ λ h, begin
   refine le_trans (add_le_add
     (lebesgue_length_mono $ inter_subset_inter_left _ h)
@@ -193,7 +193,7 @@ end
 
 theorem lebesgue_outer_trim : lebesgue_outer.trim = lebesgue_outer :=
 begin
-  refine le_antisymm (λ s, _) (outer_measure.trim_ge _),
+  refine le_antisymm (λ s, _) (outer_measure.le_trim _),
   rw outer_measure.trim_eq_infi,
   refine le_infi (λ f, le_infi $ λ hf,
     ennreal.le_of_forall_epsilon_le $ λ ε ε0 h, _),

src/measure_theory/measurable_space.lean

@@ -106,7 +106,7 @@ lemma is_measurable.congr {s t : set α} (hs : is_measurable s) (h : s = t) :
   is_measurable t :=
 by rwa ← h
 
-lemma is_measurable.Union [encodable β] {f : β → set α} (h : ∀b, is_measurable (f b)) :
+lemma is_measurable.Union [encodable β] {{f : β → set α}} (h : ∀b, is_measurable (f b)) :
   is_measurable (⋃b, f b) :=
 by { rw ← encodable.Union_decode2, exact
 ‹measurable_space α›.is_measurable_Union
@@ -123,39 +123,37 @@ end
 
 lemma is_measurable.sUnion {s : set (set α)} (hs : countable s) (h : ∀t∈s, is_measurable t) :
   is_measurable (⋃₀ s) :=
-by rw sUnion_eq_bUnion; exact is_measurable.bUnion hs h
+by { rw sUnion_eq_bUnion, exact is_measurable.bUnion hs h }
 
 lemma is_measurable.Union_Prop {p : Prop} {f : p → set α} (hf : ∀b, is_measurable (f b)) :
   is_measurable (⋃b, f b) :=
-by by_cases p; simp [h, hf, is_measurable.empty]
+by { by_cases p; simp [h, hf, is_measurable.empty] }
 
 lemma is_measurable.Inter [encodable β] {f : β → set α} (h : ∀b, is_measurable (f b)) :
   is_measurable (⋂b, f b) :=
 is_measurable.compl_iff.1 $
-by rw compl_Inter; exact is_measurable.Union (λ b, (h b).compl)
+by { rw compl_Inter, exact is_measurable.Union (λ b, (h b).compl) }
 
 lemma is_measurable.bInter {f : β → set α} {s : set β} (hs : countable s)
   (h : ∀b∈s, is_measurable (f b)) : is_measurable (⋂b∈s, f b) :=
 is_measurable.compl_iff.1 $
-by rw compl_bInter; exact is_measurable.bUnion hs (λ b hb, (h b hb).compl)
+by { rw compl_bInter, exact is_measurable.bUnion hs (λ b hb, (h b hb).compl) }
 
 lemma is_measurable.sInter {s : set (set α)} (hs : countable s) (h : ∀t∈s, is_measurable t) :
   is_measurable (⋂₀ s) :=
-by rw sInter_eq_bInter; exact is_measurable.bInter hs h
+by { rw sInter_eq_bInter, exact is_measurable.bInter hs h }
 
 lemma is_measurable.Inter_Prop {p : Prop} {f : p → set α} (hf : ∀b, is_measurable (f b)) :
   is_measurable (⋂b, f b) :=
-by by_cases p; simp [h, hf, is_measurable.univ]
+by { by_cases p; simp [h, hf, is_measurable.univ] }
 
 lemma is_measurable.union {s₁ s₂ : set α}
   (h₁ : is_measurable s₁) (h₂ : is_measurable s₂) : is_measurable (s₁ ∪ s₂) :=
-by rw union_eq_Union; exact
-is_measurable.Union (bool.forall_bool.2 ⟨h₂, h₁⟩)
+by { rw union_eq_Union, exact is_measurable.Union (bool.forall_bool.2 ⟨h₂, h₁⟩) }
 
 lemma is_measurable.inter {s₁ s₂ : set α}
   (h₁ : is_measurable s₁) (h₂ : is_measurable s₂) : is_measurable (s₁ ∩ s₂) :=
-by rw inter_eq_compl_compl_union_compl; exact
-(h₁.compl.union h₂.compl).compl
+by { rw inter_eq_compl_compl_union_compl, exact (h₁.compl.union h₂.compl).compl }
 
 lemma is_measurable.diff {s₁ s₂ : set α}
   (h₁ : is_measurable s₁) (h₂ : is_measurable s₂) : is_measurable (s₁ \ s₂) :=
@@ -166,7 +164,7 @@ lemma is_measurable.disjointed {f : ℕ → set α} (h : ∀i, is_measurable (f
 disjointed_induct (h n) (assume t i ht, is_measurable.diff ht $ h _)
 
 lemma is_measurable.const (p : Prop) : is_measurable {a : α | p} :=
-by by_cases p; simp [h, is_measurable.empty]; apply is_measurable.univ
+by { by_cases p; simp [h, is_measurable.empty]; apply is_measurable.univ }
 
 end
 
@@ -262,7 +260,7 @@ protected def mk_of_closure (g : set (set α)) (hg : {t | (generate_from g).is_m
 lemma mk_of_closure_sets {s : set (set α)}
   {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 rw [← hs] {occs := occurrences.pos [1] }; refl
+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. -/
@@ -306,7 +304,8 @@ show s ∈ (⋂m∈ms, {t | @is_measurable _ m t }) ↔ _, by simp
 
 @[simp] theorem is_measurable_infi {ι} {m : ι → measurable_space α} {s : set α} :
   @is_measurable _ (infi m) s ↔ ∀ i, @is_measurable _ (m i) s :=
-show s ∈ (λm, {s | @is_measurable _ m s }) (infi m) ↔ _, by rw (@gi_generate_from α).gc.u_infi; simp; refl
+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 :=
@@ -341,7 +340,7 @@ protected def map (f : α → β) (m : measurable_space α) : measurable_space 
 { 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 }
+  is_measurable_Union := assume f hf, by { rw [preimage_Union], exact m.is_measurable_Union _ hf }}
 
 @[simp] lemma map_id : m.map id = m :=
 measurable_space.ext $ assume s, iff.rfl
@@ -415,7 +414,7 @@ open measurable_space
 
 /-- A function `f` between measurable spaces is measurable if the preimage of every
   measurable set is measurable. -/
-def measurable [measurable_space α] [ measurable_space β] (f : α → β) : Prop :=
+def measurable [measurable_space α] [measurable_space β] (f : α → β) : Prop :=
 ∀ ⦃t : set β⦄, is_measurable t → is_measurable (f ⁻¹' t)
 
 lemma measurable_iff_le_map {m₁ : measurable_space α} {m₂ : measurable_space β} {f : α → β} :
@@ -497,7 +496,7 @@ end
 
 lemma measurable_unit [measurable_space α] (f : unit → α) : measurable f :=
 have f = (λu, f ()) := funext $ assume ⟨⟩, rfl,
-by rw this; exact measurable_const
+by { rw this, exact measurable_const }
 
 section nat
 
@@ -601,8 +600,8 @@ lemma measurable.prod [measurable_space α] [measurable_space β] [measurable_sp
   {f : α → β × γ} (hf₁ : measurable (λa, (f a).1)) (hf₂ : measurable (λa, (f a).2)) :
   measurable f :=
 measurable.of_le_map $ sup_le
-  (by rw [measurable_space.comap_le_iff_le_map, measurable_space.map_comp]; exact hf₁)
-  (by rw [measurable_space.comap_le_iff_le_map, measurable_space.map_comp]; exact hf₂)
+  (by { rw [measurable_space.comap_le_iff_le_map, measurable_space.map_comp], exact hf₁ })
+  (by { rw [measurable_space.comap_le_iff_le_map, measurable_space.map_comp], exact hf₂ })
 
 lemma measurable.prod_mk [measurable_space α] [measurable_space β] [measurable_space γ]
   {f : α → β} {g : α → γ} (hf : measurable f) (hg : measurable g) : measurable (λa:α, (f a, g a)) :=
@@ -654,23 +653,23 @@ measurable_sum hf hg
 
 lemma is_measurable.inl_image {s : set α} (hs : is_measurable s) :
   is_measurable (sum.inl '' s : set (α ⊕ β)) :=
-⟨show is_measurable (sum.inl ⁻¹' _), by rwa [preimage_image_eq]; exact (assume a b, sum.inl.inj),
+⟨show is_measurable (sum.inl ⁻¹' _), by { rwa [preimage_image_eq], exact (λ a b, sum.inl.inj) },
   have sum.inr ⁻¹' (sum.inl '' s : set (α ⊕ β)) = ∅ :=
     eq_empty_of_subset_empty $ assume x ⟨y, hy, eq⟩, by contradiction,
-  show is_measurable (sum.inr ⁻¹' _), by rw [this]; exact is_measurable.empty⟩
+  show is_measurable (sum.inr ⁻¹' _), by { rw [this], exact is_measurable.empty }⟩
 
 lemma is_measurable_range_inl : is_measurable (range sum.inl : set (α ⊕ β)) :=
-by rw [← image_univ]; exact is_measurable.univ.inl_image
+by { rw [← image_univ], exact is_measurable.univ.inl_image }
 
 lemma is_measurable_inr_image {s : set β} (hs : is_measurable s) :
   is_measurable (sum.inr '' s : set (α ⊕ β)) :=
 ⟨ have sum.inl ⁻¹' (sum.inr '' s : set (α ⊕ β)) = ∅ :=
     eq_empty_of_subset_empty $ assume x ⟨y, hy, eq⟩, by contradiction,
-  show is_measurable (sum.inl ⁻¹' _), by rw [this]; exact is_measurable.empty,
-  show is_measurable (sum.inr ⁻¹' _), by rwa [preimage_image_eq]; exact (assume a b, sum.inr.inj)⟩
+  show is_measurable (sum.inl ⁻¹' _), by { rw [this], exact is_measurable.empty },
+  show is_measurable (sum.inr ⁻¹' _), by { rwa [preimage_image_eq], exact λ a b, sum.inr.inj }⟩
 
 lemma is_measurable_range_inr : is_measurable (range sum.inr : set (α ⊕ β)) :=
-by rw [← image_univ]; exact is_measurable_inr_image is_measurable.univ
+by { rw [← image_univ], exact is_measurable_inr_image is_measurable.univ }
 
 end sum
 
@@ -725,8 +724,8 @@ lemma symm_to_equiv {α β} [measurable_space α] [measurable_space β] (e : mea
 protected def cast {α β} [i₁ : measurable_space α] [i₂ : measurable_space β]
   (h : α = β) (hi : i₁ == i₂) : measurable_equiv α β :=
 { to_equiv := equiv.cast h,
-  measurable_to_fun  := by substI h; substI hi; exact measurable_id,
-  measurable_inv_fun := by substI h; substI hi; exact measurable_id }
+  measurable_to_fun  := by { substI h, substI hi, exact measurable_id },
+  measurable_inv_fun := by { substI h, substI hi, exact measurable_id }}
 
 protected lemma measurable {α β} [measurable_space α] [measurable_space β]
   (e : measurable_equiv α β) : measurable (e : α → β) :=
@@ -807,14 +806,8 @@ noncomputable def set.image [measurable_space α] [measurable_space β]
 { to_equiv := equiv.set.image f s hf,
   measurable_to_fun  := (hfm.comp measurable_id.subtype_coe).subtype_mk,
   measurable_inv_fun :=
-    assume t ⟨u, (hu : is_measurable u), eq⟩,
     begin
-      clear_, subst eq,
-      show is_measurable {x : f '' s | ((equiv.set.image f s hf).inv_fun x).val ∈ u},
-      have : ∀(a ∈ s) (h : ∃a', a' ∈ s ∧ a' = a), classical.some h = a :=
-        λa ha h, (classical.some_spec h).2,
-      rw show {x:f '' s | ((equiv.set.image f s hf).inv_fun x).val ∈ u} = subtype.val ⁻¹' (f '' u),
-        by ext ⟨b, a, hbs, rfl⟩; simp [equiv.set.image, equiv.set.image_of_inj_on, hf, this _ hbs],
+      rintro t ⟨u, hu, rfl⟩, simp [preimage_preimage, equiv.set.image_symm_preimage hf],
       exact measurable_subtype_coe (hfi u hu)
     end }
 
@@ -833,10 +826,10 @@ def set.range_inl [measurable_space α] [measurable_space β] :
   measurable_equiv (range sum.inl : set (α ⊕ β)) α :=
 { to_fun    := λab, match ab with
     | ⟨sum.inl a, _⟩ := a
-    | ⟨sum.inr b, p⟩ := have false, by cases p; contradiction, this.elim
+    | ⟨sum.inr b, p⟩ := have false, by { cases p, contradiction }, this.elim
     end,
   inv_fun   := λa, ⟨sum.inl a, a, rfl⟩,
-  left_inv  := assume ⟨ab, a, eq⟩, by subst eq; refl,
+  left_inv  := by { rintro ⟨ab, a, rfl⟩, refl },
   right_inv := assume a, rfl,
   measurable_to_fun  := assume s (hs : is_measurable s),
     begin
@@ -851,10 +844,10 @@ def set.range_inr [measurable_space α] [measurable_space β] :
   measurable_equiv (range sum.inr : set (α ⊕ β)) β :=
 { to_fun    := λab, match ab with
     | ⟨sum.inr b, _⟩ := b
-    | ⟨sum.inl a, p⟩ := have false, by cases p; contradiction, this.elim
+    | ⟨sum.inl a, p⟩ := have false, by { cases p, contradiction }, this.elim
     end,
   inv_fun   := λb, ⟨sum.inr b, b, rfl⟩,
-  left_inv  := assume ⟨ab, b, eq⟩, by subst eq; refl,
+  left_inv  := by { rintro ⟨ab, b, rfl⟩, refl },
   right_inv := assume b, rfl,
   measurable_to_fun  := assume s (hs : is_measurable s),
     begin
@@ -875,7 +868,7 @@ def sum_prod_distrib (α β γ) [measurable_space α] [measurable_space β] [mea
       ((range sum.inr).prod univ)
       (is_measurable_range_inl.prod is_measurable.univ)
       (is_measurable_range_inr.prod is_measurable.univ)
-      (assume ⟨ab, c⟩ s, by cases ab; simp [set.prod_eq])
+      (by { rintro ⟨a|b, c⟩; simp [set.prod_eq] })
       _
       _,
     { refine (set.prod (range sum.inl) univ).symm.measurable_coe_iff.1 _,
@@ -929,11 +922,8 @@ structure dynkin_system (α : Type*) :=
 
 namespace dynkin_system
 
-@[ext] lemma ext :
-  ∀{d₁ d₂ : dynkin_system α}, (∀s:set α, d₁.has s ↔ d₂.has s) → d₁ = d₂
-| ⟨s₁, _, _, _⟩ ⟨s₂, _, _, _⟩ h :=
-  have s₁ = s₂, from funext $ assume x, propext $ h x,
-  by subst this
+@[ext] lemma ext : ∀{d₁ d₂ : dynkin_system α}, (∀s:set α, d₁.has s ↔ d₂.has s) → d₁ = d₂
+| ⟨s₁, _, _, _⟩ ⟨s₂, _, _, _⟩ h := have s₁ = s₂, from funext $ assume x, propext $ h x, by subst this
 
 variable (d : dynkin_system α)
 
@@ -946,17 +936,17 @@ by simpa using d.has_compl d.has_empty
 theorem has_Union {β} [encodable β] {f : β → set α}
   (hd : pairwise (disjoint on f)) (h : ∀i, d.has (f i)) : d.has (⋃i, f i) :=
 by { rw ← encodable.Union_decode2, exact
-d.has_Union_nat (Union_decode2_disjoint_on hd)
-  (λ n, encodable.Union_decode2_cases d.has_empty h) }
+  d.has_Union_nat (Union_decode2_disjoint_on hd)
+    (λ n, encodable.Union_decode2_cases d.has_empty h) }
 
 theorem has_union {s₁ s₂ : set α}
   (h₁ : d.has s₁) (h₂ : d.has s₂) (h : s₁ ∩ s₂ ⊆ ∅) : d.has (s₁ ∪ s₂) :=
-by rw union_eq_Union; exact
-d.has_Union (pairwise_disjoint_on_bool.2 h)
-  (bool.forall_bool.2 ⟨h₂, h₁⟩)
+by { rw union_eq_Union, exact
+  d.has_Union (pairwise_disjoint_on_bool.2 h) (bool.forall_bool.2 ⟨h₂, h₁⟩) }
 
 lemma has_diff {s₁ s₂ : set α} (h₁ : d.has s₁) (h₂ : d.has s₂) (h : s₂ ⊆ s₁) : d.has (s₁ \ s₂) :=
-d.has_compl_iff.1 begin
+begin
+  apply d.has_compl_iff.1,
   simp [diff_eq, compl_inter],
   exact d.has_union (d.has_compl h₁) h₂ (λ x ⟨h₁, h₂⟩, h₁ (h h₂)),
 end
@@ -1020,9 +1010,9 @@ def restrict_on {s : set α} (h : d.has s) : dynkin_system α :=
   has_empty := by simp [d.has_empty],
   has_compl := assume t hts,
     have tᶜ ∩ s = ((t ∩ s)ᶜ) \ sᶜ,
-      from set.ext $ assume x, by by_cases x ∈ s; simp [h],
-    by rw [this]; from d.has_diff (d.has_compl hts) (d.has_compl h)
-      (compl_subset_compl.mpr $ inter_subset_right _ _),
+      from set.ext $ assume x, by { by_cases x ∈ s; simp [h] },
+    by { rw [this], exact d.has_diff (d.has_compl hts) (d.has_compl h)
+      (compl_subset_compl.mpr $ inter_subset_right _ _) },
   has_Union_nat := assume f hd hf,
     begin
       rw [inter_comm, inter_Union],
@@ -1058,8 +1048,8 @@ generate_from s = (generate s).to_measurable_space (assume t₁ t₂, generate_i
 le_antisymm
   (generate_from_le $ assume t ht, generate_has.basic t ht)
   (of_measurable_space_le_of_measurable_space_iff.mp $
-    by rw [of_measurable_space_to_measurable_space];
-    from (generate_le _ $ assume t ht, is_measurable_generate_from ht))
+    by { rw [of_measurable_space_to_measurable_space],
+    exact (generate_le _ $ assume t ht, is_measurable_generate_from ht) })
 
 end dynkin_system
 
@@ -1071,12 +1061,12 @@ lemma induction_on_inter {C : set α → Prop} {s : set (set α)} {m : measurabl
     (∀i, m.is_measurable (f i)) → (∀i, C (f i)) → C (⋃i, f i)) :
   ∀{t}, m.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,
+  by { rw [h_eq, dynkin_system.generate_from_eq h_inter], refl },
 assume t ht,
 have dynkin_system.generate_has s t, by rwa [eq] at ht,
 this.rec_on h_basic h_empty
-  (assume t ht, h_compl t $ by rw [eq]; exact ht)
-  (assume f hf ht, h_union f hf $ assume i, by rw [eq]; exact ht _)
+  (assume t ht, h_compl t $ by { rw [eq], exact ht })
+  (assume f hf ht, h_union f hf $ assume i, by { rw [eq], exact ht _ })
 
 end measurable_space