refactor(measure_theory/measure): redefine `measure_theory.sigma_fini…

…te` (#9207)

* don't require in the definition that covering sets are measurable;
* use `to_measurable` in `sigma_finite.out` to get measurable sets.

src/measure_theory/constructions/pi.lean

@@ -328,7 +328,7 @@ def finite_spanning_sets_in.pi {C : Π i, set (set (α i))}
   (hμ : ∀ i, (μ i).finite_spanning_sets_in (C i)) (hC : ∀ i (s ∈ C i), measurable_set s) :
   (measure.pi μ).finite_spanning_sets_in (pi univ '' pi univ C) :=
 begin
-  haveI := λ i, (hμ i).sigma_finite (hC i),
+  haveI := λ i, (hμ i).sigma_finite,
   haveI := fintype.encodable ι,
   let e : ℕ → (ι → ℕ) := λ n, (decode (ι → ℕ) n).iget,
   refine ⟨λ n, pi univ (λ i, (hμ i).set (e n i)), λ n, _, λ n, _, _⟩,
@@ -356,7 +356,7 @@ begin
     (is_pi_system.pi h2C) _,
   rintro _ ⟨s, hs, rfl⟩,
   rw [mem_univ_pi] at hs,
-  haveI := λ i, (h3C i).sigma_finite (h4C i),
+  haveI := λ i, (h3C i).sigma_finite,
   simp_rw [h₁ s hs, pi_pi μ s (λ i, h4C i _ (hs i))]
 end
 
@@ -374,8 +374,7 @@ pi_eq_generate_from (λ i, generate_from_measurable_set)
 variable (μ)
 
 instance pi.sigma_finite : sigma_finite (measure.pi μ) :=
-⟨⟨(finite_spanning_sets_in.pi (λ i, (μ i).to_finite_spanning_sets_in) (λ _ _, id)).mono $
-  by { rintro _ ⟨s, hs, rfl⟩, exact measurable_set.pi_fintype hs }⟩⟩
+(finite_spanning_sets_in.pi (λ i, (μ i).to_finite_spanning_sets_in) (λ _ _, id)).sigma_finite
 
 lemma pi_eval_preimage_null {i : ι} {s : set (α i)} (hs : μ i s = 0) :
   measure.pi μ (eval i ⁻¹' s) = 0 :=

src/measure_theory/constructions/prod.lean

@@ -406,7 +406,7 @@ def finite_spanning_sets_in.prod {ν : measure β} {C : set (set α)} {D : set (
   (hC : ∀ s ∈ C, measurable_set s) (hD : ∀ t ∈ D, measurable_set t) :
   (μ.prod ν).finite_spanning_sets_in (image2 set.prod C D) :=
 begin
-  haveI := hν.sigma_finite hD,
+  haveI := hν.sigma_finite,
   refine ⟨λ n, (hμ.set n.unpair.1).prod (hν.set n.unpair.2),
     λ n, mem_image2_of_mem (hμ.set_mem _) (hν.set_mem _), λ n, _, _⟩,
   { simp_rw [prod_prod (hC _ (hμ.set_mem _)) (hD _ (hν.set_mem _))],
@@ -431,8 +431,7 @@ end
 variables [sigma_finite μ]
 
 instance prod.sigma_finite : sigma_finite (μ.prod ν) :=
-⟨⟨(μ.to_finite_spanning_sets_in.prod ν.to_finite_spanning_sets_in (λ _, id) (λ _, id)).mono $
- by { rintro _ ⟨s, t, hs, ht, rfl⟩, exact hs.prod ht }⟩⟩
+(μ.to_finite_spanning_sets_in.prod ν.to_finite_spanning_sets_in (λ _, id) (λ _, id)).sigma_finite
 
 /-- A measure on a product space equals the product measure if they are equal on rectangles
   with as sides sets that generate the corresponding σ-algebras. -/
@@ -450,7 +449,7 @@ begin
   refine (h3C.prod h3D h4C h4D).ext
     (generate_from_eq_prod hC hD h3C.is_countably_spanning h3D.is_countably_spanning).symm
     (h2C.prod h2D) _,
-  { rintro _ ⟨s, t, hs, ht, rfl⟩, haveI := h3D.sigma_finite h4D,
+  { rintro _ ⟨s, t, hs, ht, rfl⟩, haveI := h3D.sigma_finite,
     simp_rw [h₁ s hs t ht, prod_prod (h4C s hs) (h4D t ht)] }
 end
 

src/measure_theory/function/strongly_measurable.lean

@@ -258,19 +258,12 @@ begin
     refine λ x hxt, tendsto_nhds_unique (h_approx x) _,
     rw funext (λ n, h_fs_zero n x hxt),
     exact tendsto_const_nhds, },
-  { refine measure.finite_spanning_sets_in.sigma_finite _ _,
-    { exact set.range (λ n, tᶜ ∪ T n), },
-    { refine ⟨λ n, tᶜ ∪ T n, λ n, set.mem_range_self _, λ n, _, _⟩,
-      { rw [measure.restrict_apply' (measurable_set.Union hT_meas), set.union_inter_distrib_right,
-          set.compl_inter_self t, set.empty_union],
-        exact (measure_mono (set.inter_subset_left _ _)).trans_lt (hT_lt_top n), },
-      rw ← set.union_Union tᶜ T,
-      exact set.compl_union_self _, },
-    { intros s hs,
-      rw set.mem_range at hs,
-      cases hs with n hsn,
-      rw ← hsn,
-      exact (measurable_set.compl (measurable_set.Union hT_meas)).union (hT_meas n), }, },
+  { refine ⟨⟨⟨λ n, tᶜ ∪ T n, λ n, trivial, λ n, _, _⟩⟩⟩,
+    { rw [measure.restrict_apply' (measurable_set.Union hT_meas), set.union_inter_distrib_right,
+        set.compl_inter_self t, set.empty_union],
+      exact (measure_mono (set.inter_subset_left _ _)).trans_lt (hT_lt_top n), },
+    { rw ← set.union_Union tᶜ T,
+      exact set.compl_union_self _ } }
 end
 
 /-- A finitely strongly measurable function is measurable. -/

src/measure_theory/measure/measure_space.lean

@@ -33,7 +33,7 @@ We introduce the following typeclasses for measures:
 
 * `is_probability_measure μ`: `μ univ = 1`;
 * `is_finite_measure μ`: `μ univ < ∞`;
-* `sigma_finite μ`: there exists a countable collection of measurable sets that cover `univ`
+* `sigma_finite μ`: there exists a countable collection of sets that cover `univ`
   where `μ` is finite;
 * `is_locally_finite_measure μ` : `∀ x, ∃ s ∈ 𝓝 x, μ s < ∞`;
 * `has_no_atoms μ` : `∀ x, μ {x} = 0`; possibly should be redefined as
@@ -1781,23 +1781,27 @@ end measure
 open measure
 
 /-- 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`. -/
+ `{ A i | i ∈ ℕ }` such that `μ (A i) < ∞` and `⋃ i, A i = s`. -/
 class sigma_finite {m0 : measurable_space α} (μ : measure α) : Prop :=
-(out' : nonempty (μ.finite_spanning_sets_in {s | measurable_set s}))
+(out' : nonempty (μ.finite_spanning_sets_in univ))
 
 theorem sigma_finite_iff :
-  sigma_finite μ ↔ nonempty (μ.finite_spanning_sets_in {s | measurable_set s}) :=
+  sigma_finite μ ↔ nonempty (μ.finite_spanning_sets_in univ) :=
 ⟨λ h, h.1, λ h, ⟨h⟩⟩
 
 theorem sigma_finite.out (h : sigma_finite μ) :
-  nonempty (μ.finite_spanning_sets_in {s | measurable_set s}) := h.1
+  nonempty (μ.finite_spanning_sets_in univ) := h.1
 
 include m0
 
 /-- If `μ` is σ-finite it has finite spanning sets in the collection of all measurable sets. -/
 def measure.to_finite_spanning_sets_in (μ : measure α) [h : sigma_finite μ] :
   μ.finite_spanning_sets_in {s | measurable_set s} :=
-classical.choice h.out
+{ set := λ n, to_measurable μ (h.out.some.set n),
+  set_mem := λ n, measurable_set_to_measurable _ _,
+  finite := λ n, by { rw measure_to_measurable, exact h.out.some.finite n },
+  spanning := eq_univ_of_subset (Union_subset_Union $ λ n, subset_to_measurable _ _)
+    h.out.some.spanning }
 
 /-- 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
@@ -1872,9 +1876,9 @@ protected def mono (h : μ.finite_spanning_sets_in C) (hC : C ⊆ D) : μ.finite
 
 /-- If `μ` has finite spanning sets in the collection of measurable sets `C`, then `μ` is σ-finite.
 -/
-protected lemma sigma_finite (h : μ.finite_spanning_sets_in C) (hC : ∀ s ∈ C, measurable_set s) :
+protected lemma sigma_finite (h : μ.finite_spanning_sets_in C) :
   sigma_finite μ :=
-⟨⟨h.mono hC⟩⟩
+⟨⟨h.mono $ subset_univ C⟩⟩
 
 /-- An extensionality for measures. It is `ext_of_generate_from_of_Union` formulated in terms of
 `finite_spanning_sets_in`. -/
@@ -1893,8 +1897,7 @@ lemma sigma_finite_of_countable {S : set (set α)} (hc : countable S)
 begin
   obtain ⟨s, hμ, hs⟩ : ∃ s : ℕ → set α, (∀ n, μ (s n) < ∞) ∧ (⋃ n, s n) = univ,
     from (exists_seq_cover_iff_countable ⟨∅, by simp⟩).2 ⟨S, hc, hμ, hU⟩,
-  refine ⟨⟨⟨λ n, to_measurable μ (s n), λ n, measurable_set_to_measurable _ _, by simpa, _⟩⟩⟩,
-  exact eq_univ_of_subset (Union_subset_Union $ λ n, subset_to_measurable μ (s n)) hs
+  exact ⟨⟨⟨λ n, s n, λ n, trivial, hμ, hs⟩⟩⟩,
 end
 
 /-- Given measures `μ`, `ν` where `ν ≤ μ`, `finite_spanning_sets_in.of_le` provides the induced
@@ -1918,12 +1921,12 @@ include m0
 @[priority 100]
 instance is_finite_measure.to_sigma_finite (μ : measure α) [is_finite_measure μ] :
   sigma_finite μ :=
-⟨⟨⟨λ _, univ, λ _, measurable_set.univ, λ _, measure_lt_top μ _, Union_const _⟩⟩⟩
+⟨⟨⟨λ _, univ, λ _, trivial, λ _, measure_lt_top μ _, Union_const _⟩⟩⟩
 
 instance restrict.sigma_finite (μ : measure α) [sigma_finite μ] (s : set α) :
   sigma_finite (μ.restrict s) :=
 begin
-  refine ⟨⟨⟨spanning_sets μ, measurable_spanning_sets μ, λ i, _, Union_spanning_sets μ⟩⟩⟩,
+  refine ⟨⟨⟨spanning_sets μ, λ _, trivial, λ i, _, Union_spanning_sets μ⟩⟩⟩,
   rw [restrict_apply (measurable_spanning_sets μ i)],
   exact (measure_mono $ inter_subset_left _ _).trans_lt (measure_spanning_sets_lt_top μ i)
 end
@@ -1934,7 +1937,7 @@ begin
   haveI : encodable ι := fintype.encodable ι,
   have : ∀ n, measurable_set (⋂ (i : ι), spanning_sets (μ i) n) :=
     λ n, measurable_set.Inter (λ i, measurable_spanning_sets (μ i) n),
-  refine ⟨⟨⟨λ n, ⋂ i, spanning_sets (μ i) n, this, λ n, _, _⟩⟩⟩,
+  refine ⟨⟨⟨λ n, ⋂ i, spanning_sets (μ i) n, λ _, trivial, λ n, _, _⟩⟩⟩,
   { rw [sum_apply _ (this n), tsum_fintype, ennreal.sum_lt_top_iff],
     rintro i -,
     exact (measure_mono $ Inter_subset _ i).trans_lt (measure_spanning_sets_lt_top (μ i) n) },
@@ -1950,7 +1953,7 @@ lemma sigma_finite.of_map (μ : measure α) {f : α → β} (hf : measurable f)
   (h : sigma_finite (map f μ)) :
   sigma_finite μ :=
 ⟨⟨⟨λ n, f ⁻¹' (spanning_sets (map f μ) n),
-   λ n, hf $ measurable_spanning_sets _ _,
+   λ n, trivial,
    λ n, by simp only [← map_apply hf, measurable_spanning_sets, measure_spanning_sets_lt_top],
    by rw [← preimage_Union, Union_spanning_sets, preimage_univ]⟩⟩⟩
 

src/measure_theory/measure/regular.lean

@@ -221,10 +221,9 @@ end
 
 /-- A regular measure in a σ-compact space is σ-finite. -/
 @[priority 100] -- see Note [lower instance priority]
-instance sigma_finite [opens_measurable_space α] [t2_space α] [sigma_compact_space α]
-  [regular μ] : sigma_finite μ :=
+instance sigma_finite [sigma_compact_space α] [regular μ] : sigma_finite μ :=
 ⟨⟨{ set := compact_covering α,
-  set_mem := λ n, (is_compact_compact_covering α n).measurable_set,
+  set_mem := λ n, trivial,
   finite := λ n, regular.lt_top_of_is_compact $ is_compact_compact_covering α n,
   spanning := Union_compact_covering α }⟩⟩