feat(outer_measure): define bounded_by (#5314)

`bounded_by` wrapper around `of_function` that drops the condition that `m ∅ = 0`. 
Refactor `Inf_gen` to use `bounded_by`.
I am also planning to use `bounded_by` for finitary products of measures.

Also add some complete lattice lemmas

src/measure_theory/measure_space.lean

@@ -618,15 +618,14 @@ variables {m : set (measure α)}
 lemma Inf_caratheodory (s : set α) (hs : is_measurable s) :
   (Inf (to_outer_measure '' m)).caratheodory.is_measurable' s :=
 begin
-  rw [outer_measure.Inf_eq_of_function_Inf_gen],
-  refine outer_measure.of_function_caratheodory (assume t, _),
-  cases t.eq_empty_or_nonempty with ht ht, by simp [ht],
-  simp only [outer_measure.Inf_gen_nonempty1 _ _ ht, le_infi_iff, ball_image_iff,
-    coe_to_outer_measure, measure_eq_infi t],
-  assume μ hμ u htu hu,
+  rw [outer_measure.Inf_eq_bounded_by_Inf_gen],
+  refine outer_measure.bounded_by_caratheodory (λ t, _),
+  simp only [outer_measure.Inf_gen, le_infi_iff, ball_image_iff, coe_to_outer_measure,
+    measure_eq_infi t],
+  intros μ hμ u htu hu,
   have hm : ∀{s t}, s ⊆ t → outer_measure.Inf_gen (to_outer_measure '' m) s ≤ μ t,
-  { assume s t hst,
-    rw [outer_measure.Inf_gen_nonempty2 _ ⟨_, mem_image_of_mem _ hμ⟩],
+  { intros s t hst,
+    rw [outer_measure.Inf_gen_def],
     refine infi_le_of_le (μ.to_outer_measure) (infi_le_of_le (mem_image_of_mem _ hμ) _),
     rw [to_outer_measure_apply],
     refine measure_mono hst },

src/measure_theory/outer_measure.lean

@@ -32,7 +32,9 @@ for all sets `t` we have `m t = m (t ∩ s) + m (t \ s)`. This forms a measurabl
 
 ## Main definitions and statements
 
-* `outer_measure.of_function` is the greatest outer measure that is at most the given function.
+* `outer_measure.bounded_by` is the greatest outer measure that is at most the given function.
+  If you know that the given functions sends `∅` to `0`, then `outer_measure.of_function` is a
+  special case.
 * `caratheodory` is the Carathéodory-measurable space of an outer measure.
 * `Inf_eq_of_function_Inf_gen` is a characterization of the infimum of outer measures.
 * `induced_outer_measure` is the measure induced by a function on a subset of `set α`
@@ -353,6 +355,47 @@ theorem le_of_function {μ : outer_measure α} :
 
 end of_function
 
+section bounded_by
+
+variables {α : Type*} (m : set α → ennreal)
+
+/-- Given any function `m` assigning measures to sets, there is a unique maximal outer measure `μ`
+  satisfying `μ s ≤ m s` for all `s : set α`. This is the same as `outer_measure.of_function`,
+  except that it doesn't require `m ∅ = 0`. -/
+def bounded_by : outer_measure α :=
+outer_measure.of_function (λ s, ⨆ (h : s.nonempty), m s) (by simp [empty_not_nonempty])
+
+variables {m}
+theorem bounded_by_le (s : set α) : bounded_by m s ≤ m s :=
+(of_function_le _).trans supr_const_le
+
+theorem bounded_by_eq_of_function (m_empty : m ∅ = 0) (s : set α) :
+  bounded_by m s = outer_measure.of_function m m_empty s :=
+begin
+  have : (λ s : set α, ⨆ (h : s.nonempty), m s) = m,
+  { ext1 t, cases t.eq_empty_or_nonempty with h h; simp [h, empty_not_nonempty, m_empty] },
+  simp [bounded_by, this]
+end
+theorem bounded_by_apply (s : set α) :
+  bounded_by m s = ⨅ (t : ℕ → set α) (h : s ⊆ Union t), ∑' n, ⨆ (h : (t n).nonempty), m (t n) :=
+by simp [bounded_by, of_function_apply]
+
+theorem bounded_by_eq (s : set α) (m_empty : m ∅ = 0) (m_mono : ∀ ⦃t : set α⦄, s ⊆ t → m s ≤ m t)
+  (m_subadd : ∀ (s : ℕ → set α), m (⋃i, s i) ≤ (∑'i, m (s i))) : bounded_by m s = m s :=
+by rw [bounded_by_eq_of_function m_empty, of_function_eq s m_mono m_subadd]
+
+theorem le_bounded_by {μ : outer_measure α} : μ ≤ bounded_by m ↔ ∀ s, μ s ≤ m s :=
+begin
+  rw [bounded_by, le_of_function, forall_congr], intro s,
+  cases s.eq_empty_or_nonempty with h h; simp [h, empty_not_nonempty]
+end
+
+theorem le_bounded_by' {μ : outer_measure α} :
+  μ ≤ bounded_by m ↔ ∀ s : set α, s.nonempty → μ s ≤ m s :=
+by { rw [le_bounded_by, forall_congr], intro s, cases s.eq_empty_or_nonempty with h h; simp [h] }
+
+end bounded_by
+
 section caratheodory_measurable
 universe u
 parameters {α : Type u} (m : outer_measure α)
@@ -484,6 +527,15 @@ begin
   { rw ← ennreal.tsum_add, exact ennreal.tsum_le_tsum (λ i, hs _) }
 end
 
+lemma bounded_by_caratheodory {m : set α → ennreal} {s : set α}
+  (hs : ∀t, m (t ∩ s) + m (t \ s) ≤ m t) : (bounded_by m).caratheodory.is_measurable' s :=
+begin
+  apply of_function_caratheodory, intro t,
+  cases t.eq_empty_or_nonempty with h h,
+  { simp [h, empty_not_nonempty] },
+  { convert le_trans _ (hs t), { simp [h] }, exact add_le_add supr_const_le supr_const_le }
+end
+
 @[simp] theorem zero_caratheodory : (0 : outer_measure α).caratheodory = ⊤ :=
 top_unique $ λ s _ t, (add_zero _).symm
 
@@ -518,35 +570,31 @@ section Inf_gen
   function is defined to be `0` on `∅`, even if the collection of outer measures is empty.
   The outer measure generated by this function is the infimum of the given outer measures. -/
 def Inf_gen (m : set (outer_measure α)) (s : set α) : ennreal :=
-⨆(h : s.nonempty), ⨅ (μ : outer_measure α) (h : μ ∈ m), μ s
-
-@[simp] lemma Inf_gen_empty (m : set (outer_measure α)) : Inf_gen m ∅ = 0 :=
-by simp [Inf_gen, empty_not_nonempty]
+⨅ (μ : outer_measure α) (h : μ ∈ m), μ s
 
-lemma Inf_gen_nonempty1 (m : set (outer_measure α)) (t : set α) (h : t.nonempty) :
+lemma Inf_gen_def (m : set (outer_measure α)) (t : set α) :
   Inf_gen m t = (⨅ (μ : outer_measure α) (h : μ ∈ m), μ t) :=
-by rw [Inf_gen, supr_pos h]
+rfl
 
-lemma Inf_gen_nonempty2 (m : set (outer_measure α)) (h : m.nonempty) (t : set α) :
-  Inf_gen m t = (⨅ (μ : outer_measure α) (h : μ ∈ m), μ t) :=
+lemma Inf_eq_bounded_by_Inf_gen (m : set (outer_measure α)) :
+  Inf m = outer_measure.bounded_by (Inf_gen m) :=
 begin
-  cases t.eq_empty_or_nonempty with ht ht,
-  { simp only [ht, empty', Inf_gen_empty],
-    rcases h with ⟨μ, h⟩,
-    refine (bot_unique $ infi_le_of_le μ $ _).symm,
-    refine infi_le_of_le h (le_refl ⊥) },
-  { exact Inf_gen_nonempty1 m t ht }
+  refine le_antisymm _ _,
+  { refine (le_bounded_by.2 $ λ s, _), refine le_binfi _,
+    intros μ hμ, refine (show Inf m ≤ μ, from Inf_le hμ) s },
+  { refine le_Inf _, intros μ hμ t, refine le_trans (bounded_by_le t) (binfi_le μ hμ) }
 end
 
-lemma Inf_eq_of_function_Inf_gen (m : set (outer_measure α)) :
-  Inf m = outer_measure.of_function (Inf_gen m) (Inf_gen_empty m) :=
+lemma supr_Inf_gen_nonempty {m : set (outer_measure α)} (h : m.nonempty) (t : set α) :
+   (⨆ (h : t.nonempty), Inf_gen m t) = (⨅ (μ : outer_measure α) (h : μ ∈ m), μ t) :=
 begin
-  refine le_antisymm
-    (assume t', le_of_function.2 (assume t, _) _)
-    (le_Inf $ assume μ hμ t, le_trans (outer_measure.of_function_le _) _);
-    cases t.eq_empty_or_nonempty with ht ht; simp [ht, Inf_gen_nonempty1],
-  { assume μ hμ, exact (show Inf m ≤ μ, from _root_.Inf_le hμ) t },
-  { exact infi_le_of_le μ (infi_le _ hμ) }
+  rcases t.eq_empty_or_nonempty with rfl|ht,
+  { rcases h with ⟨μ, hμ⟩,
+    rw [eq_false_intro empty_not_nonempty, supr_false, eq_comm],
+    simp_rw [empty'],
+    apply bot_unique,
+    refine infi_le_of_le μ (infi_le _ hμ) },
+  { simp [ht, Inf_gen_def] }
 end
 
 /-- The value of the Infimum of a nonempty set of outer measures on a set is not simply
@@ -555,7 +603,7 @@ sets that covers that set, where a different measure can be used for each set in
 lemma Inf_apply {m : set (outer_measure α)} {s : set α} (h : m.nonempty) :
   Inf m s = ⨅ (t : ℕ → set α) (h2 : s ⊆ Union t),
     ∑' n, ⨅ (μ : outer_measure α) (h3 : μ ∈ m), μ (t n) :=
-by simp_rw [Inf_eq_of_function_Inf_gen, of_function_apply, Inf_gen_nonempty2 _ h]
+by simp_rw [Inf_eq_bounded_by_Inf_gen, bounded_by_apply, supr_Inf_gen_nonempty h]
 
 /-- This proves that Inf and restrict commute for outer measures, so long as the set of
 outer measures is nonempty. -/

src/order/complete_lattice.lean

@@ -334,6 +334,10 @@ theorem le_bsupr {p : ι → Prop} {f : Π i (h : p i), α} (i : ι) (hi : p i)
   f i hi ≤ ⨆ i hi, f i hi :=
 le_supr_of_le i $ le_supr (f i) hi
 
+theorem le_bsupr_of_le {p : ι → Prop} {f : Π i (h : p i), α} (i : ι) (hi : p i) (h : a ≤ f i hi) :
+  a ≤ ⨆ i hi, f i hi :=
+le_trans h (le_bsupr i hi)
+
 theorem supr_le (h : ∀i, s i ≤ a) : supr s ≤ a :=
 Sup_le $ assume b ⟨i, eq⟩, eq ▸ h i
 
@@ -424,6 +428,10 @@ theorem binfi_le {p : ι → Prop} {f : Π i (hi : p i), α} (i : ι) (hi : p i)
   (⨅ i hi, f i hi) ≤ f i hi :=
 infi_le_of_le i $ infi_le (f i) hi
 
+theorem binfi_le_of_le {p : ι → Prop} {f : Π i (hi : p i), α} (i : ι) (hi : p i) (h : f i hi ≤ a) :
+  (⨅ i hi, f i hi) ≤ a :=
+le_trans (binfi_le i hi) h
+
 theorem le_infi (h : ∀i, a ≤ s i) : a ≤ infi s :=
 le_Inf $ assume b ⟨i, eq⟩, eq ▸ h i
 
@@ -488,6 +496,12 @@ lemma infi_congr {α : Type*} [has_Inf α] {f : ι → α} {g : ι₂ → α} (h
   (pq : p ↔ q) (f : ∀x, f₁ (pq.mpr x) = f₂ x) : infi f₁ = infi f₂ :=
 @supr_congr_Prop (order_dual α) _ p q f₁ f₂ pq f
 
+lemma supr_const_le {x : α} : (⨆ (h : ι), x) ≤ x :=
+supr_le (λ _, le_rfl)
+
+lemma le_infi_const {x : α} : x ≤ (⨅ (h : ι), x) :=
+le_infi (λ _, le_rfl)
+
 -- We will generalize this to conditionally complete lattices in `cinfi_const`.
 theorem infi_const [nonempty ι] {a : α} : (⨅ b:ι, a) = a :=
 by rw [infi, range_const, Inf_singleton]