feat(measure_space): define sigma finite measures (#4265)

They are defined as a `Prop`. The noncomputable "eliminator" is called `spanning_sets`, and satisfies monotonicity, even though that is not required to give a `sigma_finite` instance.

I define a helper function `accumulate s := ⋃ y ≤ x, s y`. This is helpful, to separate out some monotonicity proofs. It is in its own file purely for import reasons (there is no good file to put it that imports both `set.lattice` and `finset.basic`, the latter is used in 1 lemma).

src/data/set/accumulate.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2020 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+-/
+import data.set.lattice
+/-!
+# Accumulate
+
+The function `accumulate` takes a set `s` and returns `⋃ y ≤ x, s y`.
+-/
+
+variables {α β γ : Type*} {s : α → set β} {t : α → set γ}
+
+namespace set
+
+/-- `accumulate s` is the union of `s y` for `y ≤ x`. -/
+def accumulate [has_le α] (s : α → set β) (x : α) : set β := ⋃ y ≤ x, s y
+
+variable {s}
+lemma accumulate_def [has_le α] {x : α} : accumulate s x = ⋃ y ≤ x, s y := rfl
+@[simp] lemma mem_accumulate [has_le α] {x : α} {z : β} : z ∈ accumulate s x ↔ ∃ y ≤ x, z ∈ s y :=
+mem_bUnion_iff
+
+lemma subset_accumulate [preorder α] {x : α} : s x ⊆ accumulate s x :=
+λ z, mem_bUnion le_rfl
+
+lemma monotone_accumulate [preorder α] : monotone (accumulate s) :=
+λ x y hxy, bUnion_subset_bUnion_left $ λ z hz, le_trans hz hxy
+
+lemma bUnion_accumulate [preorder α] (x : α) : (⋃ y ≤ x, accumulate s y) = ⋃ y ≤ x, s y :=
+begin
+  apply subset.antisymm,
+  { exact bUnion_subset (λ x hx, (monotone_accumulate hx : _)) },
+  { exact bUnion_subset_bUnion_right (λ x hx, subset_accumulate) }
+end
+
+lemma Union_accumulate [preorder α] : (⋃ x, accumulate s x) = ⋃ x, s x :=
+begin
+  apply subset.antisymm,
+  { simp only [subset_def, mem_Union, exists_imp_distrib, mem_accumulate],
+    intros z x x' hx'x hz, exact ⟨x', hz⟩ },
+  { exact Union_subset_Union (λ i, subset_accumulate),  }
+end
+
+end set

src/data/set/lattice.lean

@@ -899,6 +899,23 @@ by simp
 
 end preimage
 
+section prod
+
+theorem monotone_prod [preorder α] {f : α → set β} {g : α → set γ}
+  (hf : monotone f) (hg : monotone g) : monotone (λx, (f x).prod (g x)) :=
+assume a b h, prod_mono (hf h) (hg h)
+
+alias monotone_prod ← monotone.set_prod
+
+lemma Union_prod_of_monotone [semilattice_sup α] {s : α → set β} {t : α → set γ}
+  (hs : monotone s) (ht : monotone t) : (⋃ x, (s x).prod (t x)) = (⋃ x, (s x)).prod (⋃ x, (t x)) :=
+begin
+  ext ⟨z, w⟩, simp only [mem_prod, mem_Union, exists_imp_distrib, and_imp, iff_def], split,
+  { intros x hz hw, exact ⟨⟨x, hz⟩, ⟨x, hw⟩⟩ },
+  { intros x hz x' hw, exact ⟨x ⊔ x', hs le_sup_left hz, ht le_sup_right hw⟩ }
+end
+
+end prod
 
 section seq
 
@@ -955,11 +972,10 @@ lemma prod_image_seq_comm (s : set α) (t : set β) :
   (prod.mk '' s).seq t = seq ((λb a, (a, b)) '' t) s :=
 by rw [← prod_eq_seq, ← image_swap_prod, prod_eq_seq, image_seq, ← image_comp, prod.swap]
 
-end seq
+lemma image2_eq_seq (f : α → β → γ) (s : set α) (t : set β) : image2 f s t = seq (f '' s) t :=
+by { ext, simp }
 
-theorem monotone_prod [preorder α] {f : α → set β} {g : α → set γ}
-  (hf : monotone f) (hg : monotone g) : monotone (λx, (f x).prod (g x)) :=
-assume a b h, prod_mono (hf h) (hg h)
+end seq
 
 instance : monad set :=
 { pure       := λ(α : Type u) a, {a},

src/measure_theory/measure_space.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Mario Carneiro
 -/
 import measure_theory.outer_measure
 import order.filter.countable_Inter
+import data.set.accumulate
 
 /-!
 # Measure spaces
@@ -28,6 +29,8 @@ We introduce the following typeclasses for measures:
 
 * `probability_measure μ`: `μ univ = 1`;
 * `finite_measure μ`: `μ univ < ⊤`;
+* `sigma_finite μ`: there exists a countable collection of measurable sets that cover `univ`
+  where `μ` is finite;
 * `locally_finite_measure μ` : `∀ x, ∃ s ∈ 𝓝 x, μ s < ⊤`;
 * `has_no_atoms μ` : `∀ x, μ {x} = 0`; possibly should be redefined as
   `∀ s, 0 < μ s → ∃ t ⊆ s, 0 < μ t ∧ μ t < μ s`.
@@ -222,6 +225,14 @@ begin
   exact measure_bUnion_le s.countable_to_set f
 end
 
+lemma measure_bUnion_lt_top {s : set β} {f : β → set α} (hs : finite s)
+  (hfin : ∀ i ∈ s, μ (f i) < ⊤) : μ (⋃ i ∈ s, f i) < ⊤ :=
+begin
+  convert (measure_bUnion_finset_le hs.to_finset f).trans_lt _,
+  { ext, rw [finite.mem_to_finset] },
+  apply ennreal.sum_lt_top, simpa only [finite.mem_to_finset]
+end
+
 lemma measure_Union_null {β} [encodable β] {s : β → set α} :
   (∀ i, μ (s i) = 0) → μ (⋃i, s i) = 0 :=
 μ.to_outer_measure.Union_null
@@ -1333,6 +1344,10 @@ class probability_measure (μ : measure α) : Prop := (measure_univ : μ univ =
 /-- A measure `μ` is called finite if `μ univ < ⊤`. -/
 class finite_measure (μ : measure α) : Prop := (measure_univ_lt_top : μ univ < ⊤)
 
+instance restrict.finite_measure (μ : measure α) {s : set α} [hs : fact (μ s < ⊤)] :
+  finite_measure (μ.restrict s) :=
+⟨by simp [hs.elim]⟩
+
 /-- Measure `μ` *has no atoms* if the measure of each singleton is zero.
 
 NB: Wikipedia assumes that for any measurable set `s` with positive `μ`-measure,
@@ -1417,10 +1432,72 @@ lemma finite_at_filter_of_finite (μ : measure α) [finite_measure μ] (f : filt
 lemma measure.finite_at_bot (μ : measure α) : μ.finite_at_filter ⊥ :=
 ⟨∅, mem_bot_sets, by simp only [measure_empty, with_top.zero_lt_top]⟩
 
+/-- A measure `μ` is called σ-finite if there is a countable collection of sets
+  `{ A i | i ∈ ℕ }` such that `μ (A i) < ⊤` and `⋃ i, A i = s`. -/
+class sigma_finite (μ : measure α) : Prop :=
+(exists_finite_spanning_sets :
+  ∃ s : ℕ → set α,
+  (∀ i, is_measurable (s i)) ∧
+  (∀ i, μ (s i) < ⊤) ∧
+  (⋃ i, s i) = univ)
+
+lemma exists_finite_spanning_sets (μ : measure α) [sigma_finite μ] :
+  ∃ s : ℕ → set α,
+  (∀ i, is_measurable (s i)) ∧
+  (∀ i, μ (s i) < ⊤) ∧
+  (⋃ i, s i) = univ :=
+sigma_finite.exists_finite_spanning_sets
+
+/-- A noncomputable way to get a monotone collection of sets that span `univ` and have finite
+  measure using `classical.some`. This definition satisfies monotonicity in addition to all other
+  properties in `sigma_finite`. -/
+def spanning_sets (μ : measure α) [sigma_finite μ] (i : ℕ) : set α :=
+accumulate (classical.some $ exists_finite_spanning_sets μ) i
+
+lemma monotone_spanning_sets (μ : measure α) [sigma_finite μ] :
+  monotone (spanning_sets μ) :=
+monotone_accumulate
+
+lemma is_measurable_spanning_sets (μ : measure α) [sigma_finite μ] (i : ℕ) :
+  is_measurable (spanning_sets μ i) :=
+is_measurable.Union $ λ j, is_measurable.Union_Prop $
+  λ hij, (classical.some_spec $ exists_finite_spanning_sets μ).1 j
+
+lemma measure_spanning_sets_lt_top (μ : measure α) [sigma_finite μ] (i : ℕ) :
+  μ (spanning_sets μ i) < ⊤ :=
+measure_bUnion_lt_top (finite_le_nat i) $
+  λ j _, (classical.some_spec $ exists_finite_spanning_sets μ).2.1 j
+
+lemma Union_spanning_sets (μ : measure α) [sigma_finite μ] :
+  (⋃ i : ℕ, spanning_sets μ i) = univ :=
+by simp_rw [spanning_sets, Union_accumulate,
+  (classical.some_spec $ exists_finite_spanning_sets μ).2.2]
 
-instance restrict.finite_measure (μ : measure α) {s : set α} [hs : fact (μ s < ⊤)] :
-  finite_measure (μ.restrict s) :=
-⟨by simp [hs.elim]⟩
+namespace measure
+
+lemma supr_restrict_spanning_sets {μ : measure α} [sigma_finite μ] {s : set α}
+  (hs : is_measurable s) :
+  (⨆ i, μ.restrict (spanning_sets μ i) s) = μ s :=
+begin
+  convert (restrict_Union_apply_eq_supr (is_measurable_spanning_sets μ) _ hs).symm,
+  { simp [Union_spanning_sets] },
+  { exact directed_of_sup (monotone_spanning_sets μ) }
+end
+end measure
+open measure
+
+/-- Every finite measure is σ-finite. -/
+@[priority 100]
+instance finite_measure.to_sigma_finite (μ : measure α) [finite_measure μ] : sigma_finite μ :=
+⟨⟨λ _, univ, λ _, is_measurable.univ, λ _, measure_lt_top μ _, Union_const _⟩⟩
+
+instance restrict.sigma_finite (μ : measure α) [sigma_finite μ] (s : set α) :
+  sigma_finite (μ.restrict s) :=
+begin
+  refine ⟨⟨spanning_sets μ, is_measurable_spanning_sets μ, λ i, _, Union_spanning_sets μ⟩⟩,
+  rw [restrict_apply (is_measurable_spanning_sets μ i)],
+  exact (measure_mono $ inter_subset_left _ _).trans_lt (measure_spanning_sets_lt_top μ i)
+end
 
 /-- A measure is called locally finite if it is finite in some neighborhood of each point. -/
 class locally_finite_measure [topological_space α] (μ : measure α) : Prop :=