doc(measure_theory): document basic measure theory files (#3057)

src/measure_theory/measurable_space.lean

@@ -19,12 +19,12 @@ subsets closed under complementation and countable union. A function
 between measurable spaces is measurable if the preimage of each
 measurable subset is measurable.
 
-σ-algebras on a fixed set α form a complete lattice. Here we order
-σ-algebras by writing m₁ ≤ m₂ if every set which is m₁-measurable is
-also m₂-measurable (that is, m₁ is a subset of m₂). In particular, any
-collection of subsets of α generates a smallest σ-algebra which
-contains all of them. A function f : α → β induces a Galois connection
-between the lattices of σ-algebras on α and β.
+σ-algebras on a fixed set `α` form a complete lattice. Here we order
+σ-algebras by writing `m₁ ≤ m₂` if every set which is `m₁`-measurable is
+also `m₂`-measurable (that is, `m₁` is a subset of `m₂`). In particular, any
+collection of subsets of `α` generates a smallest σ-algebra which
+contains all of them. A function `f : α → β` induces a Galois connection
+between the lattices of σ-algebras on `α` and `β`.
 
 A measurable equivalence between measurable spaces is an equivalence
 which respects the σ-algebras, that is, for which both directions of
@@ -33,17 +33,17 @@ the equivalence are measurable functions.
 ## Main statements
 
 The main theorem of this file is Dynkin's π-λ theorem, which appears
-here as an induction principle `induction_on_inter`. Suppose s is a
-collection of subsets of α such that the intersection of two members
-of s belongs to s whenever it is nonempty. Let m be the σ-algebra
-generated by s. In order to check that a predicate C holds on every
-member of m, it suffices to check that C holds on the members of s and
-that C is preserved by complementation and *disjoint* countable
+here as an induction principle `induction_on_inter`. Suppose `s` is a
+collection of subsets of `α` such that the intersection of two members
+of `s` belongs to `s` whenever it is nonempty. Let `m` be the σ-algebra
+generated by `s`. In order to check that a predicate `C` holds on every
+member of `m`, it suffices to check that `C` holds on the members of `s` and
+that `C` is preserved by complementation and *disjoint* countable
 unions.
 
 ## Implementation notes
 
-Measurability of a function f : α → β between measurable spaces is
+Measurability of a function `f : α → β` between measurable spaces is
 defined in terms of the Galois connection induced by f.
 
 ## References
@@ -65,6 +65,7 @@ universes u v w x
 variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} {ι : Sort x}
   {s t u : set α}
 
+/-- A measurable space is a space equipped with a σ-algebra. -/
 structure measurable_space (α : Type u) :=
 (is_measurable : set α → Prop)
 (is_measurable_empty : is_measurable ∅)
@@ -229,6 +230,8 @@ 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) :
   measurable_space α :=
 { is_measurable := λs, s ∈ g,
@@ -241,6 +244,8 @@ lemma mk_of_closure_sets {s : set (set α)}
   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
 
+/-- 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,
   le_l_u    := assume m s, is_measurable_generate_from,
@@ -648,10 +653,12 @@ instance (α β) [measurable_space α] [measurable_space β] : has_coe_to_fun (m
 lemma coe_eq {α β} [measurable_space α] [measurable_space β] (e : measurable_equiv α β) :
   (e : α → β) = e.to_equiv := rfl
 
+/-- Any measurable space is equivalent to itself. -/
 def refl (α : Type*) [measurable_space α] : measurable_equiv α α :=
 { to_equiv := equiv.refl α,
   measurable_to_fun := measurable_id, measurable_inv_fun := measurable_id }
 
+/-- The composition of equivalences between measurable spaces. -/
 def trans [measurable_space α] [measurable_space β] [measurable_space γ]
   (ab : measurable_equiv α β) (bc : measurable_equiv β γ) :
   measurable_equiv α γ :=
@@ -663,6 +670,7 @@ lemma trans_to_equiv {α β} [measurable_space α] [measurable_space β] [measur
   (e : measurable_equiv α β) (f : measurable_equiv β γ) :
   (e.trans f).to_equiv = e.to_equiv.trans f.to_equiv := rfl
 
+/-- The inverse of an equivalence between measurable spaces. -/
 def symm [measurable_space α] [measurable_space β] (ab : measurable_equiv α β) :
   measurable_equiv β α :=
 { to_equiv := ab.to_equiv.symm,
@@ -672,6 +680,7 @@ def symm [measurable_space α] [measurable_space β] (ab : measurable_equiv α 
 lemma symm_to_equiv {α β} [measurable_space α] [measurable_space β] (e : measurable_equiv α β) :
   e.symm.to_equiv = e.to_equiv.symm := rfl
 
+/-- Equal measurable spaces are equivalent. -/
 protected def cast {α β} [i₁ : measurable_space α] [i₂ : measurable_space β]
   (h : α = β) (hi : i₁ == i₂) : measurable_equiv α β :=
 { to_equiv := equiv.cast h,
@@ -690,6 +699,7 @@ iff.intro
     by rwa [trans_to_equiv, symm_to_equiv, equiv.symm_trans] at this)
   (λh, h.comp e.measurable)
 
+/-- Products of equivalent measurable spaces are equivalent. -/
 def prod_congr [measurable_space α] [measurable_space β] [measurable_space γ] [measurable_space δ]
   (ab : measurable_equiv α β) (cd : measurable_equiv γ δ) :
   measurable_equiv (α × γ) (β × δ) :=
@@ -701,11 +711,13 @@ def prod_congr [measurable_space α] [measurable_space β] [measurable_space γ]
     (ab.measurable_inv_fun.comp (measurable.fst measurable_id))
     (cd.measurable_inv_fun.comp (measurable.snd measurable_id)) }
 
+/-- Products of measurable spaces are symmetric. -/
 def prod_comm [measurable_space α] [measurable_space β] : measurable_equiv (α × β) (β × α) :=
 { to_equiv := equiv.prod_comm α β,
   measurable_to_fun  := measurable.prod_mk (measurable.snd measurable_id) (measurable.fst measurable_id),
   measurable_inv_fun := measurable.prod_mk (measurable.snd measurable_id) (measurable.fst measurable_id) }
 
+/-- Sums of measurable spaces are symmetric. -/
 def sum_congr [measurable_space α] [measurable_space β] [measurable_space γ] [measurable_space δ]
   (ab : measurable_equiv α β) (cd : measurable_equiv γ δ) :
   measurable_equiv (α ⊕ γ) (β ⊕ δ) :=
@@ -721,7 +733,7 @@ def sum_congr [measurable_space α] [measurable_space β] [measurable_space γ]
       refine measurable_sum (measurable_inl.comp abm) (measurable_inr.comp cdm)
     end }
 
-/-- `set.prod s t ≃ (s × t)` as a `measurable_equiv`. -/
+/-- `set.prod s t ≃ (s × t)` as measurable spaces. -/
 def set.prod [measurable_space α] [measurable_space β] (s : set α) (t : set β) :
   measurable_equiv (s.prod t) (s × t) :=
 { to_equiv := equiv.set.prod s t,
@@ -732,18 +744,20 @@ def set.prod [measurable_space α] [measurable_space β] (s : set α) (t : set 
     measurable_id.fst.subtype_coe
     measurable_id.snd.subtype_coe }
 
-/-- `univ α ≃ α` as a `measurable_equiv`. -/
+/-- `univ α ≃ α` as measurable spaces. -/
 def set.univ (α : Type*) [measurable_space α] : measurable_equiv (univ : set α) α :=
 { to_equiv := equiv.set.univ α,
   measurable_to_fun := measurable_id.subtype_coe,
   measurable_inv_fun := measurable_id.subtype_mk }
 
-/-- `{a} ≃ unit` as a `measurable_equiv`. -/
+/-- `{a} ≃ unit` as measurable spaces. -/
 def set.singleton [measurable_space α] (a:α) : measurable_equiv ({a} : set α) unit :=
 { to_equiv := equiv.set.singleton a,
   measurable_to_fun := measurable_const,
   measurable_inv_fun := measurable_const }
 
+/-- A set is equivalent to its image under a function `f` as measurable spaces,
+  if `f` is an injective measurable function that sends measurable sets to measurable sets. -/
 noncomputable def set.image [measurable_space α] [measurable_space β]
   (f : α → β) (s : set α)
   (hf : function.injective f)
@@ -763,6 +777,8 @@ noncomputable def set.image [measurable_space α] [measurable_space β]
       exact (measurable.subtype_coe measurable_id) (f '' u) (hfi u hu)
     end }
 
+/-- The domain of `f` is equivalent to its range as measurable spaces,
+  if `f` is an injective measurable function that sends measurable sets to measurable sets. -/
 noncomputable def set.range [measurable_space α] [measurable_space β]
   (f : α → β) (hf : function.injective f) (hfm : measurable f)
   (hfi : ∀s, is_measurable s → is_measurable (f '' s)) :
@@ -771,6 +787,7 @@ noncomputable def set.range [measurable_space α] [measurable_space β]
   (measurable_equiv.set.image f univ hf hfm hfi).trans $
   measurable_equiv.cast (by rw image_univ) (by rw image_univ)
 
+/-- `α` is equivalent to its image in `α ⊕ β` as measurable spaces. -/
 def set.range_inl [measurable_space α] [measurable_space β] :
   measurable_equiv (range sum.inl : set (α ⊕ β)) α :=
 { to_fun    := λab, match ab with
@@ -788,6 +805,7 @@ def set.range_inl [measurable_space α] [measurable_space β] :
     end,
   measurable_inv_fun := measurable.subtype_mk measurable_inl }
 
+/-- `β` is equivalent to its image in `α ⊕ β` as measurable spaces. -/
 def set.range_inr [measurable_space α] [measurable_space β] :
   measurable_equiv (range sum.inr : set (α ⊕ β)) β :=
 { to_fun    := λab, match ab with
@@ -805,6 +823,7 @@ def set.range_inr [measurable_space α] [measurable_space β] :
     end,
   measurable_inv_fun := measurable.subtype_mk measurable_inr }
 
+/-- Products distribute over sums (on the right) as measurable spaces. -/
 def sum_prod_distrib (α β γ) [measurable_space α] [measurable_space β] [measurable_space γ] :
   measurable_equiv ((α ⊕ β) × γ) ((α × γ) ⊕ (β × γ)) :=
 { to_equiv := equiv.sum_prod_distrib α β γ,
@@ -834,10 +853,12 @@ def sum_prod_distrib (α β γ) [measurable_space α] [measurable_space β] [mea
       ((measurable_inl.comp (measurable.fst measurable_id)).prod_mk (measurable.snd measurable_id))
       ((measurable_inr.comp (measurable.fst measurable_id)).prod_mk (measurable.snd measurable_id)) }
 
+/-- Products distribute over sums (on the left) as measurable spaces. -/
 def prod_sum_distrib (α β γ) [measurable_space α] [measurable_space β] [measurable_space γ] :
   measurable_equiv (α × (β ⊕ γ)) ((α × β) ⊕ (α × γ)) :=
 prod_comm.trans $ (sum_prod_distrib _ _ _).trans $ sum_congr prod_comm prod_comm
 
+/-- Products distribute over sums as measurable spaces. -/
 def sum_prod_sum (α β γ δ)
   [measurable_space α] [measurable_space β] [measurable_space γ] [measurable_space δ] :
   measurable_equiv ((α ⊕ β) × (γ ⊕ δ)) (((α × γ) ⊕ (α × δ)) ⊕ ((β × γ) ⊕ (β × δ))) :=
@@ -852,9 +873,12 @@ end measurable_equiv
 
 namespace measurable_space
 
-/-- Dynkin systems
-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 a collection of subsets of a type `α` that contains the empty set,
+  is closed under complementation and under countable union of pairwise disjoint sets.
+  The disjointness condition is the only difference with `σ`-algebras.
+
+  The main purpose of Dynkin systems is to provide a powerful induction rule for σ-algebras
+  generated by intersection stable set systems.
 -/
 structure dynkin_system (α : Type*) :=
 (has : set α → Prop)
@@ -915,6 +939,7 @@ instance : partial_order (dynkin_system α) :=
   le_trans    := assume a b c, le_trans,
   le_antisymm := assume a b h₁ h₂, ext $ assume s, ⟨h₁ s, h₂ s⟩ }
 
+/-- Every measurable space (σ-algebra) forms a Dynkin system -/
 def of_measurable_space (m : measurable_space α) : dynkin_system α :=
 { has       := m.is_measurable,
   has_empty := m.is_measurable_empty,
@@ -925,14 +950,16 @@ lemma of_measurable_space_le_of_measurable_space_iff {m₁ m₂ : measurable_spa
   of_measurable_space m₁ ≤ of_measurable_space m₂ ↔ m₁ ≤ m₂ :=
 iff.rfl
 
-/-- The least Dynkin system containing a collection of basic sets. -/
+/-- The least Dynkin system containing a collection of basic sets.
+  This inductive type gives the underlying collection of sets. -/
 inductive generate_has (s : set (set α)) : set α → Prop
 | basic : ∀t∈s, generate_has t
 | empty : generate_has ∅
 | compl : ∀{a}, generate_has a → generate_has (-a)
 | Union : ∀{f:ℕ → set α}, pairwise (disjoint on f) →
     (∀i, generate_has (f i)) → generate_has (⋃i, f i)
 
+/-- 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,
@@ -941,6 +968,7 @@ def generate (s : set (set α)) : dynkin_system α :=
 
 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,
@@ -958,6 +986,7 @@ lemma of_measurable_space_to_measurable_space
   of_measurable_space (d.to_measurable_space h_inter) = d :=
 ext $ assume s, iff.rfl
 
+/-- If `s` is in a Dynkin system `d`, we can form the new Dynkin system `{s ∩ t | t ∈ d}`. -/
 def restrict_on {s : set α} (h : d.has s) : dynkin_system α :=
 { has       := λt, d.has (t ∩ s),
   has_empty := by simp [d.has_empty],