refactor(measure_theory/measure/regular): add inner_regular, `outer…

…_regular`, generalize (#9283)

### Regular measures

* add a non-class predicate `inner_regular` to prove some lemmas once, not twice;
* add TC `outer_regular`, drop primed lemmas;
* consistently use `≠ ∞`, `≠ 0` in the assumptions;
* drop some typeclass requirements.

### Other changes

* add a few lemmas about subtraction to `data.real.ennreal`;
* add `ennreal.add_lt_add_left`, `ennreal.add_lt_add_right`, and use them;

src/data/real/ennreal.lean

@@ -467,9 +467,15 @@ by simpa only [pos_iff_ne_zero] using ennreal.pow_pos
 lemma add_lt_add_iff_left (ha : a ≠ ∞) : a + c < a + b ↔ c < b :=
 with_top.add_lt_add_iff_left ha
 
+lemma add_lt_add_left (ha : a ≠ ∞) (h : b < c) : a + b < a + c :=
+(add_lt_add_iff_left ha).2 h
+
 lemma add_lt_add_iff_right (ha : a ≠ ∞) : c + a < b + a ↔ c < b :=
 with_top.add_lt_add_iff_right ha
 
+lemma add_lt_add_right (ha : a ≠ ∞) (h : b < c) : b + a < c + a :=
+(add_lt_add_iff_right ha).2 h
+
 instance contravariant_class_add_lt : contravariant_class ℝ≥0∞ ℝ≥0∞ (+) (<) :=
 with_top.contravariant_class_add_lt
 
@@ -773,6 +779,9 @@ begin
   rw [← coe_add, ← coe_sub, coe_lt_coe, coe_lt_coe, lt_sub_iff_right],
 end
 
+lemma lt_sub_comm : a < b - c ↔ c < b - a :=
+by rw [lt_sub_iff_add_lt, lt_sub_iff_add_lt, add_comm]
+
 lemma sub_le_self (a b : ℝ≥0∞) : a - b ≤ a :=
 ennreal.sub_le_iff_le_add.2 $ le_self_add
 
@@ -1103,6 +1112,9 @@ begin
   refine (le_div_iff_mul_le _ _).symm; simpa
 end
 
+lemma lt_div_iff_mul_lt (hb0 : b ≠ 0 ∨ c ≠ ∞) (hbt : b ≠ ∞ ∨ c ≠ 0) : c < a / b ↔ c * b < a :=
+lt_iff_lt_of_le_iff_le (div_le_iff_le_mul hb0 hbt)
+
 lemma div_le_of_le_mul (h : a ≤ b * c) : a / c ≤ b :=
 begin
   by_cases h0 : c = 0,
@@ -1133,6 +1145,8 @@ lt_iff_lt_of_le_iff_le $ le_div_iff_mul_le h0 ht
 lemma mul_lt_of_lt_div (h : a < b / c) : a * c < b :=
 by { contrapose! h, exact ennreal.div_le_of_le_mul h }
 
+lemma mul_lt_of_lt_div' (h : a < b / c) : c * a < b := mul_comm a c ▸ mul_lt_of_lt_div h
+
 lemma inv_le_iff_le_mul : (b = ∞ → a ≠ 0) → (a = ∞ → b ≠ 0) → (a⁻¹ ≤ b ↔ 1 ≤ a * b) :=
 begin
   cases a; cases b; simp [none_eq_top, some_eq_coe, mul_top, top_mul] {contextual := tt},
@@ -1227,6 +1241,8 @@ begin
   exact nnreal.half_lt_self hz
 end
 
+lemma half_le_self : a / 2 ≤ a := le_add_self.trans_eq (add_halves _)
+
 lemma sub_half (h : a ≠ ∞) : a - a / 2 = a / 2 :=
 begin
   lift a to ℝ≥0 using h,

src/measure_theory/constructions/borel_space.lean

@@ -199,6 +199,15 @@ instance subtype.opens_measurable_space {α : Type*} [topological_space α] [mea
   opens_measurable_space s :=
 ⟨by { rw [borel_comap], exact comap_mono h.1 }⟩
 
+theorem _root_.measurable_set.induction_on_open [topological_space α] [measurable_space α]
+  [borel_space α] {C : set α → Prop} (h_open : ∀ U, is_open U → C U)
+  (h_compl : ∀ t, measurable_set t → C t → C tᶜ)
+  (h_union : ∀ f : ℕ → set α, pairwise (disjoint on f) →
+    (∀ i, measurable_set (f i)) → (∀ i, C (f i)) → C (⋃ i, f i)) :
+  ∀ ⦃t⦄, measurable_set t → C t :=
+measurable_space.induction_on_inter borel_space.measurable_eq is_pi_system_is_open
+  (h_open _ is_open_empty) h_open h_compl h_union
+
 section
 variables [topological_space α] [measurable_space α] [opens_measurable_space α]
    [topological_space β] [measurable_space β] [opens_measurable_space β]
@@ -1596,6 +1605,30 @@ ae_measurable_comp_iff_of_closed_embedding (λ y : 𝕜, y • c) (closed_embedd
 
 end normed_space
 
+/-- If `s` is a compact set and `μ` is finite at `𝓝 x` for every `x ∈ s`, then `s` admits an open
+superset of finite measure. -/
+lemma is_compact.exists_open_superset_measure_lt_top' [topological_space α]
+  {s : set α} {μ : measure α} (h : is_compact s) (hμ : ∀ x ∈ s, μ.finite_at_filter (𝓝 x)) :
+  ∃ U ⊇ s, is_open U ∧ μ U < ∞ :=
+begin
+  refine is_compact.induction_on h _ _ _ _,
+  { use ∅, simp [superset] },
+  { rintro s t hst ⟨U, htU, hUo, hU⟩, exact ⟨U, hst.trans htU, hUo, hU⟩ },
+  { rintro s t ⟨U, hsU, hUo, hU⟩ ⟨V, htV, hVo, hV⟩,
+    refine ⟨U ∪ V, union_subset_union hsU htV, hUo.union hVo,
+      (measure_union_le _ _).trans_lt $ ennreal.add_lt_top.2 ⟨hU, hV⟩⟩ },
+  { intros x hx,
+    rcases (hμ x hx).exists_mem_basis (nhds_basis_opens _) with ⟨U, ⟨hx, hUo⟩, hU⟩,
+    exact ⟨U, nhds_within_le_nhds (hUo.mem_nhds hx), U, subset.rfl, hUo, hU⟩ }
+end
+
+/-- If `s` is a compact set and `μ` is a locally finite measure, then `s` admits an open superset of
+finite measure. -/
+lemma is_compact.exists_open_superset_measure_lt_top [topological_space α]
+  {s : set α} (μ : measure α) [is_locally_finite_measure μ] (h : is_compact s) :
+  ∃ U ⊇ s, is_open U ∧ μ U < ∞ :=
+h.exists_open_superset_measure_lt_top' $ λ x hx, μ.finite_at_nhds x
+
 lemma is_compact.measure_lt_top_of_nhds_within [topological_space α]
   {s : set α} {μ : measure α} (h : is_compact s) (hμ : ∀ x ∈ s, μ.finite_at_filter (𝓝[s] x)) :
   μ s < ∞ :=
@@ -1606,3 +1639,27 @@ lemma is_compact.measure_lt_top [topological_space α] {s : set α} {μ : measur
   [is_locally_finite_measure μ] (h : is_compact s) :
   μ s < ∞ :=
 h.measure_lt_top_of_nhds_within $ λ x hx, μ.finite_at_nhds_within _ _
+
+/-- Compact covering of a `σ`-compact topological space as
+`measure_theory.measure.finite_spanning_sets_in`. -/
+def measure_theory.measure.finite_spanning_sets_in_compact [topological_space α]
+  [sigma_compact_space α] (μ : measure α) [is_locally_finite_measure μ] :
+  μ.finite_spanning_sets_in {K | is_compact K} :=
+{ set := compact_covering α,
+  set_mem := is_compact_compact_covering α,
+  finite := λ n, (is_compact_compact_covering α n).measure_lt_top,
+  spanning := Union_compact_covering α }
+
+/-- A locally finite measure on a `σ`-compact topological space admits a finite spanning sequence
+of open sets. -/
+def measure_theory.measure.finite_spanning_sets_in_open [topological_space α]
+  [sigma_compact_space α] (μ : measure α) [is_locally_finite_measure μ] :
+  μ.finite_spanning_sets_in {K | is_open K} :=
+{ set := λ n, ((is_compact_compact_covering α n).exists_open_superset_measure_lt_top μ).some,
+  set_mem := λ n,
+    ((is_compact_compact_covering α n).exists_open_superset_measure_lt_top μ).some_spec.snd.1,
+  finite := λ n,
+    ((is_compact_compact_covering α n).exists_open_superset_measure_lt_top μ).some_spec.snd.2,
+  spanning := eq_univ_of_subset (Union_subset_Union $ λ n,
+    ((is_compact_compact_covering α n).exists_open_superset_measure_lt_top μ).some_spec.fst)
+    (Union_compact_covering α) }

src/measure_theory/function/continuous_map_dense.lean

@@ -92,23 +92,22 @@ begin
     obtain ⟨η, hη, hηδ⟩ := exists_between hδ,
     refine ⟨η, hη, _⟩,
     exact_mod_cast hδε' hηδ },
-  have hη_pos' : (0 : ℝ≥0∞) < ↑η := by exact_mod_cast hη_pos,
+  have hη_pos' : (0 : ℝ≥0∞) < η := ennreal.coe_pos.2 hη_pos,
   -- Use the regularity of the measure to `η`-approximate `s` by an open superset and a closed
   -- subset
-  obtain ⟨u, u_open, su, μu⟩ : ∃ u, is_open u ∧ s ⊆ u ∧ μ u < μ s + ↑η,
-  { refine hs.exists_is_open_lt_of_lt _ _,
-    simpa using (ennreal.add_lt_add_iff_left hsμ.ne).2 hη_pos' },
-  obtain ⟨F, F_closed, Fs, μF⟩ : ∃ F, is_closed F ∧ F ⊆ s ∧ μ s < μ F + ↑η :=
-    hs.exists_lt_is_closed_of_lt_top_of_pos hsμ hη_pos',
+  obtain ⟨u, su, u_open, μu⟩ : ∃ u ⊇ s, is_open u ∧ μ u < μ s + ↑η,
+  { refine s.exists_is_open_lt_of_lt _ _,
+    simpa using ennreal.add_lt_add_left hsμ.ne hη_pos' },
+  obtain ⟨F, Fs, F_closed, μF⟩ : ∃ F ⊆ s, is_closed F ∧ μ s < μ F + ↑η :=
+    hs.exists_is_closed_lt_add hsμ.ne hη_pos'.ne',
   have : disjoint uᶜ F,
   { rw [set.disjoint_iff_inter_eq_empty, set.inter_comm, ← set.subset_compl_iff_disjoint],
     simpa using Fs.trans su },
   have h_μ_sdiff : μ (u \ F) ≤ 2 * η,
   { have hFμ : μ F < ⊤ := (measure_mono Fs).trans_lt hsμ,
     refine ennreal.le_of_add_le_add_left hFμ.ne _,
     have : μ u < μ F + ↑η + ↑η,
-    { refine μu.trans _,
-      rwa ennreal.add_lt_add_iff_right (ennreal.coe_ne_top : ↑η ≠ ⊤) },
+      from μu.trans (ennreal.add_lt_add_right ennreal.coe_ne_top μF),
     convert this.le using 1,
     { rw [add_comm, ← measure_union, set.diff_union_of_subset (Fs.trans su)],
       { exact disjoint_sdiff_self_left },

src/measure_theory/integral/vitali_caratheodory.lean

@@ -108,14 +108,14 @@ begin
       { simp only [lintegral_const, zero_mul, zero_le, ennreal.coe_zero] } },
     have : μ s < μ s + ε / c,
     { have : (0 : ℝ≥0∞) < ε / c := ennreal.div_pos_iff.2 ⟨ε0, ennreal.coe_ne_top⟩,
-      simpa using (ennreal.add_lt_add_iff_left _).2 this,
+      simpa using ennreal.add_lt_add_left _ this,
       simpa only [hs, hc, lt_top_iff_ne_top, true_and, simple_func.coe_const, function.const_apply,
         lintegral_const, ennreal.coe_indicator, set.univ_inter, ennreal.coe_ne_top,
         measurable_set.univ, with_top.mul_eq_top_iff, simple_func.const_zero, or_false,
         lintegral_indicator, ennreal.coe_eq_zero, ne.def, not_false_iff, simple_func.coe_zero,
         set.piecewise_eq_indicator, simple_func.coe_piecewise, false_and, restrict_apply] using h },
-    obtain ⟨u, u_open, su, μu⟩ : ∃ u, is_open u ∧ s ⊆ u ∧ μ u < μ s + ε / c :=
-      hs.exists_is_open_lt_of_lt _ this,
+    obtain ⟨u, su, u_open, μu⟩ : ∃ u ⊇ s, is_open u ∧ μ u < μ s + ε / c :=
+      s.exists_is_open_lt_of_lt _ this,
     refine ⟨set.indicator u (λ x, c), λ x, _, u_open.lower_semicontinuous_indicator (zero_le _), _⟩,
     { simp only [simple_func.coe_const, simple_func.const_zero, simple_func.coe_zero,
         set.piecewise_eq_indicator, simple_func.coe_piecewise],
@@ -325,8 +325,8 @@ begin
         lintegral_indicator, ennreal.coe_eq_zero, ne.def, not_false_iff, simple_func.coe_zero,
         set.piecewise_eq_indicator, simple_func.coe_piecewise, false_and] using int_f,
     have : (0 : ℝ≥0∞) < ε / c := ennreal.div_pos_iff.2 ⟨ε0, ennreal.coe_ne_top⟩,
-    obtain ⟨F, F_closed, Fs, μF⟩ : ∃ F, is_closed F ∧ F ⊆ s ∧ μ s < μ F + ε / c :=
-      hs.exists_lt_is_closed_of_lt_top_of_pos μs_lt_top this,
+    obtain ⟨F, Fs, F_closed, μF⟩ : ∃ F ⊆ s, is_closed F ∧ μ s < μ F + ε / c :=
+      hs.exists_is_closed_lt_add μs_lt_top.ne this.ne',
     refine ⟨set.indicator F (λ x, c), λ x, _,
       F_closed.upper_semicontinuous_indicator (zero_le _), _⟩,
     { simp only [simple_func.coe_const, simple_func.const_zero, simple_func.coe_zero,

src/measure_theory/measure/content.lean

@@ -338,32 +338,31 @@ begin
 end
 
 /-- The measure induced by the outer measure coming from a content, on the Borel sigma-algebra. -/
-def measure : measure G := μ.outer_measure.to_measure μ.borel_le_caratheodory
+protected def measure : measure G := μ.outer_measure.to_measure μ.borel_le_caratheodory
 
 lemma measure_apply {s : set G} (hs : measurable_set s) : μ.measure s = μ.outer_measure s :=
 to_measure_apply _ _ hs
 
 /-- In a locally compact space, any measure constructed from a content is regular. -/
 instance regular [locally_compact_space G] : μ.measure.regular :=
 begin
+  haveI : μ.measure.outer_regular,
+  { refine ⟨λ A hA r (hr : _ < _), _⟩,
+    rw [μ.measure_apply hA, outer_measure_eq_infi] at hr,
+    simp only [infi_lt_iff] at hr,
+    rcases hr with ⟨U, hUo, hAU, hr⟩,
+    rw [← μ.outer_measure_of_is_open U hUo, ← μ.measure_apply hUo.measurable_set] at hr,
+    exact ⟨U, hAU, hUo, hr⟩ },
   split,
   { intros K hK,
     rw [measure_apply _ hK.measurable_set],
     exact μ.outer_measure_lt_top_of_is_compact hK },
-  { intros A hA,
-    rw [measure_apply _ hA, outer_measure_eq_infi],
-    refine binfi_le_binfi _,
-    intros U hU,
-    refine infi_le_infi _,
-    intro h2U,
-    rw [measure_apply _ hU.measurable_set, μ.outer_measure_of_is_open U hU],
-    refl' },
-  { intros U hU,
-    rw [measure_apply _ hU.measurable_set, μ.outer_measure_of_is_open U hU],
-    dsimp only [inner_content], refine bsupr_le (λ K hK, _),
-    refine le_supr_of_le K.1 _, refine le_supr_of_le K.2 _, refine le_supr_of_le hK _,
-    rw [measure_apply _ K.2.measurable_set],
-    apply le_outer_measure_compacts },
+  { intros U hU r hr,
+    rw [measure_apply _ hU.measurable_set, μ.outer_measure_of_is_open U hU] at hr,
+    simp only [inner_content, lt_supr_iff] at hr,
+    rcases hr with ⟨K, hKU, hr⟩,
+    refine ⟨K.1, hKU, K.2, hr.trans_le _⟩,
+    exact (μ.le_outer_measure_compacts K).trans (le_to_measure_apply _ _ _) },
 end
 
 end content

src/measure_theory/measure/measure_space.lean

@@ -176,6 +176,19 @@ begin
   rw [← measure_union disjoint_diff h₂ (h₁.diff h₂), union_diff_cancel h]
 end
 
+lemma le_measure_diff : μ s₁ - μ s₂ ≤ μ (s₁ \ s₂) :=
+ennreal.sub_le_iff_le_add'.2 $
+calc μ s₁ ≤ μ (s₂ ∪ s₁)        : measure_mono (subset_union_right _ _)
+      ... = μ (s₂ ∪ s₁ \ s₂)   : congr_arg μ union_diff_self.symm
+      ... ≤ μ s₂ + μ (s₁ \ s₂) : measure_union_le _ _
+
+lemma measure_diff_lt_of_lt_add (hs : measurable_set s) (ht : measurable_set t) (hst : s ⊆ t)
+  (hs' : μ s ≠ ∞) {ε : ℝ≥0∞} (h : μ t < μ s + ε) : μ (t \ s) < ε :=
+begin
+  rw [measure_diff hst ht hs hs'], rw add_comm at h,
+  exact ennreal.sub_lt_of_lt_add (measure_mono hst) h
+end
+
 lemma meas_eq_meas_of_null_diff {s t : set α}
   (hst : s ⊆ t) (h_nulldiff : μ (t.diff s) = 0) : μ s = μ t :=
 by { rw [←diff_diff_cancel_left hst, ←@measure_diff_null _ _ _ t _ h_nulldiff], refl, }
@@ -1603,6 +1616,24 @@ lemma measure_lt_top (μ : measure α) [is_finite_measure μ] (s : set α) : μ
 lemma measure_ne_top (μ : measure α) [is_finite_measure μ] (s : set α) : μ s ≠ ∞ :=
 ne_of_lt (measure_lt_top μ s)
 
+lemma measure_compl_le_add_of_le_add [is_finite_measure μ] (hs : measurable_set s)
+  (ht : measurable_set t) {ε : ℝ≥0∞} (h : μ s ≤ μ t + ε) :
+  μ tᶜ ≤ μ sᶜ + ε :=
+begin
+  rw [measure_compl ht (measure_ne_top μ _), measure_compl hs (measure_ne_top μ _),
+    ennreal.sub_le_iff_le_add],
+  calc μ univ = μ univ - μ s + μ s :
+    (ennreal.sub_add_cancel_of_le $ measure_mono s.subset_univ).symm
+  ... ≤ μ univ - μ s + (μ t + ε) : add_le_add_left h _
+  ... = _ : by rw [add_right_comm, add_assoc]
+end
+
+lemma measure_compl_le_add_iff [is_finite_measure μ] (hs : measurable_set s)
+  (ht : measurable_set t) {ε : ℝ≥0∞} :
+  μ sᶜ ≤ μ tᶜ + ε ↔ μ t ≤ μ s + ε :=
+⟨λ h, compl_compl s ▸ compl_compl t ▸ measure_compl_le_add_of_le_add hs.compl ht.compl h,
+  measure_compl_le_add_of_le_add ht hs⟩
+
 /-- The measure of the whole space with respect to a finite measure, considered as `ℝ≥0`. -/
 def measure_univ_nnreal (μ : measure α) : ℝ≥0 := (μ univ).to_nnreal
 
@@ -1924,9 +1955,15 @@ namespace finite_spanning_sets_in
 
 variables {C D : set (set α)}
 
+/-- If `μ` has finite spanning sets in `C` and `C ∩ {s | μ s < ∞} ⊆ D` then `μ` has finite spanning
+sets in `D`. -/
+protected def mono' (h : μ.finite_spanning_sets_in C) (hC : C ∩ {s | μ s < ∞} ⊆ D) :
+  μ.finite_spanning_sets_in D :=
+⟨h.set, λ i, hC ⟨h.set_mem i, h.finite i⟩, h.finite, h.spanning⟩
+
 /-- If `μ` has finite spanning sets in `C` and `C ⊆ D` then `μ` has finite spanning sets in `D`. -/
 protected def mono (h : μ.finite_spanning_sets_in C) (hC : C ⊆ D) : μ.finite_spanning_sets_in D :=
-⟨h.set, λ i, hC (h.set_mem i), h.finite, h.spanning⟩
+h.mono' (λ s hs, hC hs.1)
 
 /-- If `μ` has finite spanning sets in the collection of measurable sets `C`, then `μ` is σ-finite.
 -/
@@ -1941,7 +1978,7 @@ protected lemma ext {ν : measure α} {C : set (set α)} (hA : ‹_› = generat
 ext_of_generate_from_of_Union C _ hA hC h.spanning h.set_mem (λ i, (h.finite i).ne) h_eq
 
 protected lemma is_countably_spanning (h : μ.finite_spanning_sets_in C) : is_countably_spanning C :=
-⟨_, h.set_mem, h.spanning⟩
+⟨h.set, h.set_mem, h.spanning⟩
 
 end finite_spanning_sets_in