feat(measure_theory): preliminaries for Haar measure (#3195)

Move properties about lattice operations on encodable types to a new file. These are generalized from lemmas in the measure theory folder, for lattice operations and not just for `ennreal`. Also move them to the `encodable` namespace.
Rename `outer_measure.Union_aux` to `encodable.Union_decode2`.
Generalize some properties for outer measures to arbitrary complete lattices. This is useful for operations that behave like outer measures on a subset of `set \a`.

src/data/equiv/denumerable.lean

@@ -7,7 +7,7 @@ Denumerable (countably infinite) types, as a typeclass extending
 encodable. This is used to provide explicit encode/decode functions
 from nat, where the functions are known inverses of each other.
 -/
-import data.equiv.encodable
+import data.equiv.encodable.basic
 import data.sigma
 import data.fintype.basic
 import data.list.min_max

src/data/equiv/encodable/lattice.lean

@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2020 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Floris van Doorn
+-/
+import data.equiv.encodable.basic
+import data.finset
+import data.set.disjointed
+/-!
+# Lattice operations on encodable types
+
+Lemmas about lattice and set operations on encodable types
+
+## Implementation Notes
+
+This is a separate file, to avoid unnecessary imports in basic files.
+
+Previously some of these results were in the `measure_theory` folder.
+-/
+
+open set
+
+namespace encodable
+
+variables {α : Type*} {β : Type*} [encodable β]
+
+lemma supr_decode2 [complete_lattice α] (f : β → α) :
+  (⨆ (i : ℕ) (b ∈ decode2 β i), f b) = (⨆ b, f b) :=
+by { rw [supr_comm], simp [mem_decode2] }
+
+lemma Union_decode2 (f : β → set α) : (⋃ (i : ℕ) (b ∈ decode2 β i), f b) = (⋃ b, f b) :=
+supr_decode2 f
+
+@[elab_as_eliminator] lemma Union_decode2_cases
+  {f : β → set α} {C : set α → Prop}
+  (H0 : C ∅) (H1 : ∀ b, C (f b)) {n} :
+  C (⋃ b ∈ decode2 β n, f b) :=
+match decode2 β n with
+| none := by { simp, apply H0 }
+| (some b) := by { convert H1 b, simp [ext_iff] }
+end
+
+theorem Union_decode2_disjoint_on {f : β → set α} (hd : pairwise (disjoint on f)) :
+  pairwise (disjoint on λ i, ⋃ b ∈ decode2 β i, f b) :=
+begin
+  rintro i j ij x ⟨h₁, h₂⟩,
+  revert h₁ h₂,
+  simp, intros b₁ e₁ h₁ b₂ e₂ h₂,
+  refine hd _ _ _ ⟨h₁, h₂⟩,
+  cases encodable.mem_decode2.1 e₁,
+  cases encodable.mem_decode2.1 e₂,
+  exact mt (congr_arg _) ij
+end
+
+end encodable
+
+namespace finset
+
+lemma nonempty_encodable {α} (t : finset α) : nonempty $ encodable {i // i ∈ t} :=
+begin
+  classical, induction t using finset.induction with x t hx ih,
+  { refine ⟨⟨λ _, 0, λ _, none, λ ⟨x,y⟩, y.rec _⟩⟩ },
+  { cases ih with ih, exactI ⟨encodable.of_equiv _ (finset.subtype_insert_equiv_option hx)⟩ }
+end
+
+end finset

src/data/rat/basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
 import data.int.sqrt
-import data.equiv.encodable
+import data.equiv.encodable.basic
 import algebra.group
 import algebra.euclidean_domain
 import algebra.ordered_field

src/measure_theory/borel_space.lean

@@ -198,6 +198,9 @@ lemma is_measurable_interior : is_measurable (interior s) := is_open_interior.is
 lemma is_closed.is_measurable (h : is_closed s) : is_measurable s :=
 is_measurable.compl_iff.1 $ h.is_measurable
 
+lemma compact.is_measurable [t2_space α] (h : compact s) : is_measurable s :=
+h.is_closed.is_measurable
+
 lemma is_measurable_singleton [t1_space α] {x : α} : is_measurable ({x} : set α) :=
 is_closed_singleton.is_measurable
 

src/measure_theory/measurable_space.lean

@@ -7,6 +7,7 @@ Measurable spaces -- σ-algberas
 -/
 import data.set.disjointed
 import data.set.countable
+import data.equiv.encodable.lattice
 
 /-!
 # Measurable spaces and measurable functions
@@ -102,25 +103,12 @@ lemma is_measurable.congr {s t : set α} (hs : is_measurable s) (h : s = t) :
   is_measurable t :=
 by rwa ← h
 
-lemma encodable.Union_decode2 {α} [encodable β] (f : β → set α) :
-  (⋃ b, f b) = ⋃ (i : ℕ) (b ∈ decode2 β i), f b :=
-ext $ by simp [mem_decode2, exists_swap]
-
-@[elab_as_eliminator] lemma encodable.Union_decode2_cases
-  {α} [encodable β] {f : β → set α} {C : set α → Prop}
-  (H0 : C ∅) (H1 : ∀ b, C (f b)) {n} :
-  C (⋃ b ∈ decode2 β n, f b) :=
-match decode2 β n with
-| none := by simp; apply H0
-| (some b) := by convert H1 b; simp [ext_iff]
-end
-
 lemma is_measurable.Union [encodable β] {f : β → set α} (h : ∀b, is_measurable (f b)) :
   is_measurable (⋃b, f b) :=
-by rw encodable.Union_decode2; exact
+by { rw ← encodable.Union_decode2, exact
 ‹measurable_space α›.is_measurable_Union
   (λ n, ⋃ b ∈ decode2 β n, f b)
-  (λ n, encodable.Union_decode2_cases is_measurable.empty h)
+  (λ n, encodable.Union_decode2_cases is_measurable.empty h) }
 
 lemma is_measurable.bUnion {f : β → set α} {s : set β} (hs : countable s)
   (h : ∀b∈s, is_measurable (f b)) : is_measurable (⋃b∈s, f b) :=
@@ -882,19 +870,6 @@ structure dynkin_system (α : Type*) :=
 (has_compl : ∀{a}, has a → has aᶜ)
 (has_Union_nat : ∀{f:ℕ → set α}, pairwise (disjoint on f) → (∀i, has (f i)) → has (⋃i, f i))
 
-theorem Union_decode2_disjoint_on
-  {β} [encodable β] {f : β → set α} (hd : pairwise (disjoint on f)) :
-  pairwise (disjoint on λ i, ⋃ b ∈ decode2 β i, f b) :=
-begin
-  rintro i j ij x ⟨h₁, h₂⟩,
-  revert h₁ h₂,
-  simp, intros b₁ e₁ h₁ b₂ e₂ h₂,
-  refine hd _ _ _ ⟨h₁, h₂⟩,
-  cases encodable.mem_decode2.1 e₁,
-  cases encodable.mem_decode2.1 e₂,
-  exact mt (congr_arg _) ij
-end
-
 namespace dynkin_system
 
 @[ext] lemma ext :
@@ -913,9 +888,9 @@ 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
+by { rw ← encodable.Union_decode2, exact
 d.has_Union_nat (Union_decode2_disjoint_on hd)
-  (λ n, encodable.Union_decode2_cases d.has_empty h)
+  (λ 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₂) :=

src/measure_theory/measure_space.lean

@@ -25,7 +25,7 @@ extension of the restricted measure.
 In the first part of the file we define operations on arbitrary functions defined on measurable
 sets.
 
-Measures on `α` form a complete lattice.
+Measures on `α` form a complete lattice, and are closed under scalar multiplication with `ennreal`.
 
 Given a measure, the null sets are the sets where `μ s = 0`, where `μ` denotes the corresponding
 outer measure (so `s` might not be measurable). We can then define the completion of `μ` as the
@@ -129,10 +129,10 @@ lemma measure'_Union
   (hd : pairwise (disjoint on f)) (hm : ∀i, is_measurable (f i)) :
   measure' (⋃i, f i) = (∑'i, measure' (f i)) :=
 begin
-  rw [encodable.Union_decode2, outer_measure.Union_aux],
+  rw [← encodable.Union_decode2, ← tsum_Union_decode2],
   { exact measure'_Union_nat _ _
       (λ n, encodable.Union_decode2_cases is_measurable.empty hm)
-      (mU _ (measurable_space.Union_decode2_disjoint_on hd)) },
+      (mU _ (encodable.Union_decode2_disjoint_on hd)) },
   { apply measure'_empty },
 end
 
@@ -229,7 +229,7 @@ by simp [infi_subtype, infi_and, trim_eq_infi]
 theorem trim_trim (m : outer_measure α) : m.trim.trim = m.trim :=
 le_antisymm (le_trim_iff.2 $ λ s hs, by simp [trim_eq _ hs, le_refl]) (trim_ge _)
 
-theorem trim_zero : (0 : outer_measure α).trim = 0 :=
+@[simp] theorem trim_zero : (0 : outer_measure α).trim = 0 :=
 ext $ λ s, le_antisymm
   (le_trans ((trim 0).mono (subset_univ s)) $
     le_of_eq $ trim_eq _ is_measurable.univ)
@@ -251,6 +251,53 @@ theorem trim_sum_ge {ι} (m : ι → outer_measure α) : sum (λ i, (m i).trim)
 λ t st ht, ennreal.tsum_le_tsum (λ i,
   infi_le_of_le t $ infi_le_of_le st $ infi_le _ ht)
 
+lemma exists_is_measurable_superset_of_trim_eq_zero
+  {m : outer_measure α} {s : set α} (h : m.trim s = 0) :
+  ∃t, s ⊆ t ∧ is_measurable t ∧ m t = 0 :=
+begin
+  rw [trim_eq_infi] at h,
+  have h := (infi_eq_bot _).1 h,
+  choose t ht using show ∀n:ℕ, ∃t, s ⊆ t ∧ is_measurable t ∧ m t < n⁻¹,
+  { assume n,
+    have : (0 : ennreal) < n⁻¹ :=
+      (zero_lt_iff_ne_zero.2 $ ennreal.inv_ne_zero.2 $ ennreal.nat_ne_top _),
+    rcases h _ this with ⟨t, ht⟩,
+    use [t],
+    simpa [(>), infi_lt_iff, -add_comm] using ht },
+  refine ⟨⋂n, t n, subset_Inter (λn, (ht n).1), is_measurable.Inter (λn, (ht n).2.1), _⟩,
+  refine eq_of_le_of_forall_le_of_dense bot_le (assume r hr, _),
+  rcases ennreal.exists_inv_nat_lt (ne_of_gt hr) with ⟨n, hn⟩,
+  calc m (⋂n, t n) ≤ m (t n) : m.mono' (Inter_subset _ _)
+    ... ≤ n⁻¹ : le_of_lt (ht n).2.2
+    ... ≤ r : le_of_lt hn
+end
+
+/- Can this proof be simplified? Currently it's pretty ugly. -/
+lemma trim_smul (m : outer_measure α) (x : ennreal) : (x • m).trim = x • m.trim :=
+begin
+  ext1 s,
+  haveI : nonempty {t : set α // s ⊆ t ∧ is_measurable t} :=
+  ⟨⟨set.univ, subset_univ s, is_measurable.univ⟩⟩,
+  by_cases h : x = 0,
+  { simp only [h, zero_smul, zero_apply, trim_zero] },
+  simp only [smul_apply],
+  by_cases h2 : m.trim s = 0,
+  { rcases exists_is_measurable_superset_of_trim_eq_zero h2 with ⟨t, h1t, h2t, h3t⟩,
+    simp only [h2, mul_zero, ←le_zero_iff_eq],
+    refine le_trans (outer_measure.mono _ h1t) _,
+    simp only [trim_eq _ h2t, smul_apply, le_zero_iff_eq, measure_of_eq_coe, h3t, mul_zero] },
+  by_cases h3 : x = ⊤,
+  { simp only [h3, h2, with_top.top_mul, ne.def, not_false_iff],
+    simp only [trim_eq_infi, true_and, infi_eq_top, smul_apply, with_top.mul_eq_top_iff,
+      eq_self_iff_true, not_false_iff, ennreal.top_ne_zero, ← zero_lt_iff_ne_zero, true_and,
+      with_top.zero_lt_top],
+    intros t ht h2t, right, refine lt_of_lt_of_le (zero_lt_iff_ne_zero.mpr h2) _,
+    rw [← trim_eq m h2t], exact m.trim.mono ht },
+  simp only [trim_eq_infi, infi_and'],
+  simp only [infi_subtype'],
+  rw [ennreal.mul_infi], refl, exact h3
+end
+
 end outer_measure
 
 /-- A measure is defined to be an outer measure that is countably additive on
@@ -346,23 +393,7 @@ by rw [← le_zero_iff_eq, ← h₂]; exact measure_mono h
 
 lemma exists_is_measurable_superset_of_measure_eq_zero {s : set α} (h : μ s = 0) :
   ∃t, s ⊆ t ∧ is_measurable t ∧ μ t = 0 :=
-begin
-  rw [measure_eq_infi] at h,
-  have h := (infi_eq_bot _).1 h,
-  choose t ht using show ∀n:ℕ, ∃t, s ⊆ t ∧ is_measurable t ∧ μ t < n⁻¹,
-  { assume n,
-    have : (0 : ennreal) < n⁻¹ :=
-      (zero_lt_iff_ne_zero.2 $ ennreal.inv_ne_zero.2 $ ennreal.nat_ne_top _),
-    rcases h _ this with ⟨t, ht⟩,
-    use [t],
-    simpa [(>), infi_lt_iff, -add_comm] using ht },
-  refine ⟨⋂n, t n, subset_Inter (λn, (ht n).1), is_measurable.Inter (λn, (ht n).2.1), _⟩,
-  refine eq_of_le_of_forall_le_of_dense bot_le (assume r hr, _),
-  rcases ennreal.exists_inv_nat_lt (ne_of_gt hr) with ⟨n, hn⟩,
-  calc μ (⋂n, t n) ≤ μ (t n) : measure_mono (Inter_subset _ _)
-    ... ≤ n⁻¹ : le_of_lt (ht n).2.2
-    ... ≤ r : le_of_lt hn
-end
+outer_measure.exists_is_measurable_superset_of_trim_eq_zero (by rw [← measure_eq_trim, h])
 
 theorem measure_Union_le {β} [encodable β] (s : β → set α) : μ (⋃i, s i) ≤ (∑'i, μ (s i)) :=
 μ.to_outer_measure.Union _
@@ -658,6 +689,27 @@ instance : complete_lattice (measure α) :=
 -/
   .. complete_lattice_of_Inf (measure α) (λ ms, ⟨λ _, Inf_le, λ _, le_Inf⟩) }
 
+open outer_measure
+
+instance : has_scalar ennreal (measure α) :=
+⟨λ x m, {
+  m_Union := λ s hs h2s, by { simp only [measure_of_eq_coe, to_outer_measure_apply, smul_apply,
+    ennreal.tsum_mul_left, measure_Union h2s hs] },
+  trimmed := by { convert m.to_outer_measure.trim_smul x, ext1 s,
+    simp only [m.trimmed, smul_apply, measure_of_eq_coe] },
+  ..x • m.to_outer_measure }⟩
+
+@[simp] theorem smul_apply (a : ennreal) (m : measure α) (s : set α) : (a • m) s = a * m s := rfl
+
+instance : semimodule ennreal (measure α) :=
+{ smul_add := λ a m₁ m₂, ext $ λ s hs, mul_add _ _ _,
+  add_smul := λ a b m, ext $ λ s hs, add_mul _ _ _,
+  mul_smul := λ a b m, ext $ λ s hs, mul_assoc _ _ _,
+  one_smul := λ m, ext $ λ s hs, one_mul _,
+  zero_smul := λ m, ext $ λ s hs, zero_mul _,
+  smul_zero := λ a, ext $ λ s hs, mul_zero _,
+  ..measure.has_scalar }
+
 end
 
 /-- The pushforward of a measure. It is defined to be `0` if `f` is not a measurable function. -/

src/measure_theory/outer_measure.lean

@@ -61,55 +61,39 @@ structure outer_measure (α : Type*) :=
 
 namespace outer_measure
 
-instance {α} : has_coe_to_fun (outer_measure α) := ⟨_, λ m, m.measure_of⟩
-
 section basic
-variables {α : Type*} {ms : set (outer_measure α)} {m : outer_measure α}
+
+variables {α : Type*} {β : Type*} {ms : set (outer_measure α)} {m : outer_measure α}
+
+instance : has_coe_to_fun (outer_measure α) := ⟨_, λ m, m.measure_of⟩
+
+@[simp] lemma measure_of_eq_coe {m : outer_measure α} {s : set α} : m.measure_of s = m s := rfl
 
 @[simp] theorem empty' (m : outer_measure α) : m ∅ = 0 := m.empty
 
 theorem mono' (m : outer_measure α) {s₁ s₂}
   (h : s₁ ⊆ s₂) : m s₁ ≤ m s₂ := m.mono h
 
-theorem Union_aux (m : set α → ennreal) (m0 : m ∅ = 0)
-  {β} [encodable β] (s : β → set α) :
-  (∑' b, m (s b)) = ∑' i, m (⋃ b ∈ decode2 β i, s b) :=
-begin
-  have H : ∀ n, m (⋃ b ∈ decode2 β n, s b) ≠ 0 → (decode2 β n).is_some,
-  { intros n h,
-    cases decode2 β n with b,
-    { exact (h (by simp [m0])).elim },
-    { exact rfl } },
-  refine tsum_eq_tsum_of_ne_zero_bij (λ n h, option.get (H n h)) _ _ _,
-  { intros m n hm hn e,
-    have := mem_decode2.1 (option.get_mem (H n hn)),
-    rwa [← e, mem_decode2.1 (option.get_mem (H m hm))] at this },
-  { intros b h,
-    refine ⟨encode b, _, _⟩,
-    { convert h, simp [set.ext_iff, encodek2] },
-    { exact option.get_of_mem _ (encodek2 _) } },
-  { intros n h,
-    transitivity, swap,
-    rw [show decode2 β n = _, from option.get_mem (H n h)],
-    congr, simp [set.ext_iff, -option.some_get] }
-end
-
 protected theorem Union (m : outer_measure α)
   {β} [encodable β] (s : β → set α) :
   m (⋃i, s i) ≤ (∑'i, m (s i)) :=
-by rw [Union_decode2, Union_aux _ m.empty' s]; exact m.Union_nat _
+rel_supr_tsum m m.empty (≤) m.Union_nat s
 
 lemma Union_null (m : outer_measure α)
   {β} [encodable β] {s : β → set α} (h : ∀ i, m (s i) = 0) : m (⋃i, s i) = 0 :=
 by simpa [h] using m.Union s
 
+protected lemma Union_finset (m : outer_measure α) (s : β → set α) (t : finset β) :
+  m (⋃i ∈ t, s i) ≤ ∑ i in t, m (s i) :=
+rel_supr_sum m m.empty (≤) m.Union_nat s t
+
 protected lemma union (m : outer_measure α) (s₁ s₂ : set α) :
   m (s₁ ∪ s₂) ≤ m s₁ + m s₂ :=
-begin
-  convert m.Union (λ b, cond b s₁ s₂),
-  { simp [union_eq_Union] },
-  { rw tsum_fintype, change _ = _ + _, simp }
-end
+rel_sup_add m m.empty (≤) m.Union_nat s₁ s₂
+
+lemma le_inter_add_diff {m : outer_measure α} {t : set α} (s : set α) :
+  m t ≤ m (t ∩ s) + m (t \ s) :=
+by { convert m.union _ _, rw inter_union_diff t s }
 
 lemma union_null (m : outer_measure α) {s₁ s₂ : set α}
   (h₁ : m s₁ = 0) (h₂ : m s₂ = 0) : m (s₁ ∪ s₂) = 0 :=
@@ -339,8 +323,7 @@ variables {s s₁ s₂ : set α}
 private def C (s : set α) : Prop := ∀t, m t = m (t ∩ s) + m (t \ s)
 
 private lemma C_iff_le {s : set α} : C s ↔ ∀t, m (t ∩ s) + m (t \ s) ≤ m t :=
-forall_congr $ λ t, le_antisymm_iff.trans $ and_iff_right $
-by convert m.union _ _; rw inter_union_diff t s
+forall_congr $ λ t, le_antisymm_iff.trans $ and_iff_right $ le_inter_add_diff _
 
 @[simp] private lemma C_empty : C ∅ := by simp [C, m.empty, diff_empty]
 

src/order/ideal.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Wärn
 -/
 import order.basic
-import data.equiv.encodable
+import data.equiv.encodable.basic
 
 /-!
 # Order ideals, cofinal sets, and the Rasiowa–Sikorski lemma