From 36a061b6e1eb1b1d898628fa0a5e4512e01ab1d5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Johannes=20H=C3=B6lzl?= Date: Mon, 12 Mar 2018 17:09:31 +0100 Subject: [PATCH] feat(analysis/measure_theory): outer_measures form a complete lattice --- analysis/measure_theory/measure_space.lean | 20 +++- analysis/measure_theory/outer_measure.lean | 125 ++++++++++++++++++--- 2 files changed, 129 insertions(+), 16 deletions(-) diff --git a/analysis/measure_theory/measure_space.lean b/analysis/measure_theory/measure_space.lean index d60116e0d333b..1691430205111 100644 --- a/analysis/measure_theory/measure_space.lean +++ b/analysis/measure_theory/measure_space.lean @@ -183,7 +183,7 @@ measure_space_eq_of $ assume s hs, lemma measure_mono (h : s₁ ⊆ s₂) : μ.measure s₁ ≤ μ.measure s₂ := μ.to_outer_measure.mono h lemma measure_Union_le_tsum_nat {s : ℕ → set α} : μ.measure (⋃i, s i) ≤ (∑i, μ.measure (s i)) := -@outer_measure.Union_nat α μ.to_outer_measure s +μ.to_outer_measure.Union_nat s lemma measure_union (hd : disjoint s₁ s₂) (h₁ : is_measurable s₁) (h₂ : is_measurable s₂) : μ.measure (s₁ ∪ s₂) = μ.measure s₁ + μ.measure s₂ := @@ -381,6 +381,24 @@ def count : measure_space α := instance : has_zero (measure_space α) := ⟨{ measure_of := λs hs, 0, measure_of_empty := rfl, measure_of_Union := by simp }⟩ +instance measure_space.inhabited : inhabited (measure_space α) := ⟨0⟩ + +instance : has_add (measure_space α) := +⟨λμ₁ μ₂, { measure_space . + measure_of := λs hs, μ₁.measure_of s hs + μ₂.measure_of s hs, + measure_of_empty := by simp [measure_space.measure_of_empty], + measure_of_Union := assume f hf hd, + by simp [measure_space.measure_of_Union, hf, hd, tsum_add] {contextual := tt} }⟩ + +instance : add_comm_monoid (measure_space α) := +{ add_comm_monoid . + zero := 0, + add := (+), + add_assoc := assume a b c, measure_space_eq_of $ assume s hs, add_assoc _ _ _, + add_comm := assume a b, measure_space_eq_of $ assume s hs, add_comm _ _, + zero_add := assume a, measure_space_eq_of $ assume s hs, zero_add _, + add_zero := assume a, measure_space_eq_of $ assume s hs, add_zero _ } + instance : partial_order (measure_space α) := { partial_order . le := λm₁ m₂, ∀s (hs : is_measurable s), m₁.measure_of s hs ≤ m₂.measure_of s hs, diff --git a/analysis/measure_theory/outer_measure.lean b/analysis/measure_theory/outer_measure.lean index d58f50be1e09b..bf8b8e3989a9f 100644 --- a/analysis/measure_theory/outer_measure.lean +++ b/analysis/measure_theory/outer_measure.lean @@ -24,32 +24,127 @@ structure outer_measure (α : Type*) := (measure_of : set α → ennreal) (empty : measure_of ∅ = 0) (mono : ∀{s₁ s₂}, s₁ ⊆ s₂ → measure_of s₁ ≤ measure_of s₂) -(Union_nat : ∀{s:ℕ → set α}, measure_of (⋃i, s i) ≤ (∑i, measure_of (s i))) +(Union_nat : ∀(s:ℕ → set α), measure_of (⋃i, s i) ≤ (∑i, measure_of (s i))) namespace outer_measure -section -parameters {α : Type*} (m : outer_measure α) -include m - -variables {s s₁ s₂ : set α} -local notation `μ` := m.measure_of +section basic +variables {α : Type*} {ms : set (outer_measure α)} {m : outer_measure α} -lemma subadditive : μ (s₁ ∪ s₂) ≤ μ s₁ + μ s₂ := +lemma subadditive (m : outer_measure α) {s₁ s₂ : set α} : + m.measure_of (s₁ ∪ s₂) ≤ m.measure_of s₁ + m.measure_of s₂ := let s := λi, ([s₁, s₂].nth i).get_or_else ∅ in -calc μ (s₁ ∪ s₂) ≤ μ (⋃i, s i) : +calc m.measure_of (s₁ ∪ s₂) ≤ m.measure_of (⋃i, s i) : m.mono $ union_subset (subset_Union s 0) (subset_Union s 1) - ... ≤ (∑i, μ (s i)) : @outer_measure.Union_nat α m s - ... = (insert 0 {1} : finset ℕ).sum (μ ∘ s) : tsum_eq_sum $ assume n h, + ... ≤ (∑i, m.measure_of (s i)) : m.Union_nat s + ... = (insert 0 {1} : finset ℕ).sum (m.measure_of ∘ s) : tsum_eq_sum $ assume n h, match n, h with | 0, h := by simp at h; contradiction | 1, h := by simp at h; contradiction | nat.succ (nat.succ n), h := m.empty end - ... = μ s₁ + μ s₂ : by simp [-add_comm]; refl - + ... = m.measure_of s₁ + m.measure_of s₂ : by simp [-add_comm]; refl + +lemma outer_measure_eq : ∀{μ₁ μ₂ : outer_measure α}, + (∀s, μ₁.measure_of s = μ₂.measure_of s) → μ₁ = μ₂ +| ⟨m₁, e₁, _, u₁⟩ ⟨m₂, e₂, _, u₂⟩ h := + have m₁ = m₂, from funext $ assume s, h s, + by simp [this] + +instance : has_zero (outer_measure α) := +⟨{ measure_of := λ_, 0, + empty := rfl, + mono := assume _ _ _, le_refl 0, + Union_nat := assume s, ennreal.zero_le }⟩ + +instance : inhabited (outer_measure α) := ⟨0⟩ + +instance : has_add (outer_measure α) := +⟨λm₁ m₂, + { measure_of := λs, m₁.measure_of s + m₂.measure_of s, + empty := show m₁.measure_of ∅ + m₂.measure_of ∅ = 0, by simp [outer_measure.empty], + mono := assume s₁ s₂ h, add_le_add' (m₁.mono h) (m₂.mono h), + Union_nat := assume s, + calc m₁.measure_of (⋃i, s i) + m₂.measure_of (⋃i, s i) ≤ + (∑i, m₁.measure_of (s i)) + (∑i, m₂.measure_of (s i)) : + add_le_add' (m₁.Union_nat s) (m₂.Union_nat s) + ... = _ : (tsum_add ennreal.has_sum ennreal.has_sum).symm}⟩ + +instance : add_comm_monoid (outer_measure α) := +{ zero := 0, + add := (+), + add_comm := assume a b, outer_measure_eq $ assume s, add_comm _ _, + add_assoc := assume a b c, outer_measure_eq $ assume s, add_assoc _ _ _, + add_zero := assume a, outer_measure_eq $ assume s, add_zero _, + zero_add := assume a, outer_measure_eq $ assume s, zero_add _ } + +instance : has_bot (outer_measure α) := ⟨0⟩ + +instance outer_measure.order_bot : order_bot (outer_measure α) := +{ le := λm₁ m₂, ∀s, m₁.measure_of s ≤ m₂.measure_of s, + bot := 0, + le_refl := assume a s, le_refl _, + le_trans := assume a b c hab hbc s, le_trans (hab s) (hbc s), + le_antisymm := assume a b hab hba, outer_measure_eq $ assume s, le_antisymm (hab s) (hba s), + bot_le := assume a s, ennreal.zero_le } + +section supremum + +private def sup (ms : set (outer_measure α)) (h : ms ≠ ∅) := +{ outer_measure . + measure_of := λs, ⨆m:ms, m.val.measure_of s, + empty := + let ⟨m, hm⟩ := set.exists_mem_of_ne_empty h in + have ms := ⟨m, hm⟩, + by simp [outer_measure.empty]; exact @supr_const _ _ _ _ ⟨this⟩, + mono := assume s₁ s₂ hs, supr_le_supr $ assume ⟨m, hm⟩, m.mono hs, + Union_nat := assume f, supr_le $ assume m, + calc m.val.measure_of (⋃i, f i) ≤ (∑ (i : ℕ), m.val.measure_of (f i)) : m.val.Union_nat _ + ... ≤ (∑i, ⨆m:ms, m.val.measure_of (f i)) : + ennreal.tsum_le_tsum $ assume i, le_supr (λm:ms, m.val.measure_of (f i)) m } + +instance : has_Sup (outer_measure α) := ⟨λs, if h : s = ∅ then ⊥ else sup s h⟩ + +private lemma le_Sup (hm : m ∈ ms) : m ≤ Sup ms := +show m ≤ (if h : ms = ∅ then ⊥ else sup ms h), + by rw [dif_neg (set.ne_empty_of_mem hm)]; + exact assume s, le_supr (λm:ms, m.val.measure_of s) ⟨m, hm⟩ + +private lemma Sup_le (hm : ∀m' ∈ ms, m' ≤ m) : Sup ms ≤ m := +show (if h : ms = ∅ then ⊥ else sup ms h) ≤ m, +begin + by_cases ms = ∅, + { rw [dif_pos h], exact bot_le }, + { rw [dif_neg h], exact assume s, (supr_le $ assume ⟨m', h'⟩, (hm m' h') s) } end +instance : has_Inf (outer_measure α) := ⟨λs, Sup {m | ∀m'∈s, m ≤ m'}⟩ +private lemma Inf_le (hm : m ∈ ms) : Inf ms ≤ m := Sup_le $ assume m' h', h' _ hm +private lemma le_Inf (hm : ∀m' ∈ ms, m ≤ m') : m ≤ Inf ms := le_Sup hm + +instance : complete_lattice (outer_measure α) := +{ top := Sup univ, + le_top := assume a, le_Sup (mem_univ a), + Sup := Sup, + Sup_le := assume s m, Sup_le, + le_Sup := assume s m, le_Sup, + Inf := Inf, + Inf_le := assume s m, Inf_le, + le_Inf := assume s m, le_Inf, + sup := λa b, Sup {a, b}, + le_sup_left := assume a b, le_Sup $ by simp, + le_sup_right := assume a b, le_Sup $ by simp, + sup_le := assume a b c ha hb, Sup_le $ by simp [or_imp_distrib, ha, hb] {contextual:=tt}, + inf := λa b, Inf {a, b}, + inf_le_left := assume a b, Inf_le $ by simp, + inf_le_right := assume a b, Inf_le $ by simp, + le_inf := assume a b c ha hb, le_Inf $ by simp [or_imp_distrib, ha, hb] {contextual:=tt}, + .. outer_measure.order_bot } + +end supremum + +end basic + section of_function set_option eqn_compiler.zeta true @@ -212,7 +307,7 @@ suffices μ t ≥ μ (t ∩ (⋃i, s i)) + μ (t \ (⋃i, s i)), this, have hp : μ (t ∩ ⋃i, s i) ≤ (⨆n, μ (t ∩ ⋃i