feat(measure_theory/constructions/borel_space): decomposing the measu…

…re of a set into slices (#10096)

Also add the fact that `μ (to_measurable μ t ∩ s) = μ (t ∩ s)`, and useful variations around this fact.

src/measure_theory/constructions/borel_space.lean

@@ -1144,7 +1144,6 @@ lemma measurable_limsup {f : ℕ → δ → α} (hf : ∀ i, measurable (f i)) :
   measurable (λ x, limsup at_top (λ i, f i x)) :=
 measurable_limsup' hf at_top_countable_basis (λ i, countable_encodable _)
 
-
 end complete_linear_order
 
 section conditionally_complete_linear_order
@@ -1194,6 +1193,61 @@ instance ereal.borel_space : borel_space ereal := ⟨rfl⟩
 instance complex.measurable_space : measurable_space ℂ := borel ℂ
 instance complex.borel_space : borel_space ℂ := ⟨rfl⟩
 
+/-- One can cut out `ℝ≥0∞` into the sets `{0}`, `Ico (t^n) (t^(n+1))` for `n : ℤ` and `{∞}`. This
+gives a way to compute the measure of a set in terms of sets on which a given function `f` does not
+fluctuate by more than `t`. -/
+lemma measure_eq_measure_preimage_add_measure_tsum_Ico_zpow [measurable_space α] (μ : measure α)
+  {f : α → ℝ≥0∞} (hf : measurable f) {s : set α} (hs : measurable_set s) {t : ℝ≥0} (ht : 1 < t) :
+  μ s = μ (s ∩ f⁻¹' {0}) + μ (s ∩ f⁻¹' {∞}) + ∑' (n : ℤ), μ (s ∩ f⁻¹' (Ico (t^n) (t^(n+1)))) :=
+begin
+  have A : μ s = μ (s ∩ f⁻¹' {0}) + μ (s ∩ f⁻¹' (Ioi 0)),
+  { rw ← measure_union,
+    { congr' 1,
+      ext x,
+      have : 0 = f x ∨ 0 < f x := eq_or_lt_of_le bot_le,
+      rw eq_comm at this,
+      simp only [←and_or_distrib_left, this, mem_singleton_iff, mem_inter_eq, and_true,
+        mem_union_eq, mem_Ioi, mem_preimage], },
+    { apply disjoint_left.2 (λ x hx h'x, _),
+      have : 0 < f x := h'x.2,
+      exact lt_irrefl 0 (this.trans_le hx.2.le) },
+    { exact hs.inter (hf (measurable_set_singleton _)) },
+    { exact hs.inter (hf measurable_set_Ioi) } },
+  have B : μ (s ∩ f⁻¹' (Ioi 0)) = μ (s ∩ f⁻¹' {∞}) + μ (s ∩ f⁻¹' (Ioo 0 ∞)),
+  { rw ← measure_union,
+    { rw ← inter_union_distrib_left,
+      congr,
+      ext x,
+      simp only [mem_singleton_iff, mem_union_eq, mem_Ioo, mem_Ioi, mem_preimage],
+      have H : f x = ∞ ∨ f x < ∞ := eq_or_lt_of_le le_top,
+      cases H,
+      { simp only [H, eq_self_iff_true, or_false, with_top.zero_lt_top, not_top_lt, and_false] },
+      { simp only [H, H.ne, and_true, false_or] } },
+    { apply disjoint_left.2 (λ x hx h'x, _),
+      have : f x < ∞ := h'x.2.2,
+      exact lt_irrefl _ (this.trans_le (le_of_eq hx.2.symm)) },
+    { exact hs.inter (hf (measurable_set_singleton _)) },
+    { exact hs.inter (hf measurable_set_Ioo) } },
+  have C : μ (s ∩ f⁻¹' (Ioo 0 ∞)) = ∑' (n : ℤ), μ (s ∩ f⁻¹' (Ico (t^n) (t^(n+1)))),
+  { rw [← measure_Union, ennreal.Ioo_zero_top_eq_Union_Ico_zpow (ennreal.one_lt_coe_iff.2 ht)
+         ennreal.coe_ne_top, preimage_Union, inter_Union],
+    { assume i j,
+      simp only [function.on_fun],
+      wlog h : i ≤ j := le_total i j using [i j, j i] tactic.skip,
+      { assume hij,
+        replace hij : i + 1 ≤ j := lt_of_le_of_ne h hij,
+        apply disjoint_left.2 (λ x hx h'x, lt_irrefl (f x) _),
+        calc f x < t ^ (i + 1) : hx.2.2
+        ... ≤ t ^ j : ennreal.zpow_le_of_le (ennreal.one_le_coe_iff.2 ht.le) hij
+        ... ≤ f x : h'x.2.1 },
+      { assume hij,
+        rw disjoint.comm,
+        exact this hij.symm } },
+    { assume n,
+      exact hs.inter (hf measurable_set_Ico) } },
+  rw [A, B, C, add_assoc],
+end
+
 section metric_space
 
 variables [metric_space α] [measurable_space α] [opens_measurable_space α]

src/measure_theory/measure/finite_measure_weak_convergence.lean

@@ -140,7 +140,7 @@ by { funext, simp [← ennreal.coe_eq_coe], }
 
 @[simp, norm_cast] lemma coe_fn_smul (c : ℝ≥0) (μ : finite_measure α) :
   (⇑(c • μ) : set α → ℝ≥0) = c • (⇑μ : set α → ℝ≥0) :=
-by { funext, simp [← ennreal.coe_eq_coe], refl, }
+by { funext, simp [← ennreal.coe_eq_coe], }
 
 instance : add_comm_monoid (finite_measure α) :=
 finite_measure.coe_injective.add_comm_monoid

src/measure_theory/measure/measure_space.lean

@@ -462,6 +462,29 @@ lemma measure_union_add_inter' (hs : measurable_set s) (t : set α) :
 by rw [union_comm, inter_comm, measure_union_add_inter t hs, add_comm]
 namespace measure
 
+/-- If `u` is a superset of `t` with the same measure (both sets possibly non-measurable), then
+for any measurable set `s` one also has `μ (t ∩ s) = μ (u ∩ s)`. -/
+lemma measure_inter_eq_of_measure_eq {s t u : set α} (hs : measurable_set s)
+  (h : μ t = μ u) (htu : t ⊆ u) (ht_ne_top : μ t ≠ ∞) :
+  μ (t ∩ s) = μ (u ∩ s) :=
+begin
+  rw h at ht_ne_top,
+  refine le_antisymm (measure_mono (inter_subset_inter_left _ htu)) _,
+  have A : μ (u ∩ s) + μ (u \ s) ≤ μ (t ∩ s) + μ (u \ s) := calc
+    μ (u ∩ s) + μ (u \ s) = μ u : measure_inter_add_diff _ hs
+    ... = μ t : h.symm
+    ... = μ (t ∩ s) + μ (t \ s) : (measure_inter_add_diff _ hs).symm
+    ... ≤ μ (t ∩ s) + μ (u \ s) :
+      add_le_add le_rfl (measure_mono (diff_subset_diff htu subset.rfl)),
+  have B : μ (u \ s) ≠ ∞ := (lt_of_le_of_lt (measure_mono (diff_subset _ _)) ht_ne_top.lt_top).ne,
+  exact ennreal.le_of_add_le_add_right B A
+end
+
+lemma measure_to_measurable_inter {s t : set α} (hs : measurable_set s) (ht : μ t ≠ ∞) :
+  μ (to_measurable μ t ∩ s) = μ (t ∩ s) :=
+(measure_inter_eq_of_measure_eq hs (measure_to_measurable t).symm
+  (subset_to_measurable μ t) ht).symm
+
 /-! ### The `ℝ≥0∞`-module of measures -/
 
 instance [measurable_space α] : has_zero (measure α) :=
@@ -514,7 +537,7 @@ rfl
   ⇑(c • μ) = c • μ :=
 rfl
 
-theorem smul_apply {m : measurable_space α} (c : ℝ≥0∞) (μ : measure α) (s : set α) :
+@[simp] theorem smul_apply {m : measurable_space α} (c : ℝ≥0∞) (μ : measure α) (s : set α) :
   (c • μ) s = c * μ s :=
 rfl
 
@@ -526,6 +549,52 @@ injective.module ℝ≥0∞ ⟨to_outer_measure, zero_to_outer_measure, add_to_o
   ⇑(c • μ) = c • μ :=
 rfl
 
+@[simp] theorem coe_nnreal_smul_apply {m : measurable_space α} (c : ℝ≥0) (μ : measure α)
+  (s : set α) :
+  (c • μ) s = c * μ s :=
+rfl
+
+lemma measure_eq_left_of_subset_of_measure_add_eq {s t : set α}
+  (h : (μ + ν) t ≠ ∞) (h' : s ⊆ t) (h'' : (μ + ν) s = (μ + ν) t) :
+  μ s = μ t :=
+begin
+  refine le_antisymm (measure_mono h') _,
+  have : μ t + ν t ≤ μ s + ν t := calc
+    μ t + ν t = μ s + ν s : h''.symm
+    ... ≤ μ s + ν t : add_le_add le_rfl (measure_mono h'),
+  apply ennreal.le_of_add_le_add_right _ this,
+  simp only [not_or_distrib, ennreal.add_eq_top, pi.add_apply, ne.def, coe_add] at h,
+  exact h.2
+end
+
+lemma measure_eq_right_of_subset_of_measure_add_eq {s t : set α}
+  (h : (μ + ν) t ≠ ∞) (h' : s ⊆ t) (h'' : (μ + ν) s = (μ + ν) t) :
+  ν s = ν t :=
+begin
+  rw add_comm at h'' h,
+  exact measure_eq_left_of_subset_of_measure_add_eq h h' h''
+end
+
+lemma measure_to_measurable_add_inter_left {s t : set α}
+  (hs : measurable_set s) (ht : (μ + ν) t ≠ ∞) :
+  μ (to_measurable (μ + ν) t ∩ s) = μ (t ∩ s) :=
+begin
+  refine (measure_inter_eq_of_measure_eq hs _ (subset_to_measurable _ _) _).symm,
+  { refine measure_eq_left_of_subset_of_measure_add_eq _ (subset_to_measurable _ _)
+      (measure_to_measurable t).symm,
+    rwa measure_to_measurable t, },
+  { simp only [not_or_distrib, ennreal.add_eq_top, pi.add_apply, ne.def, coe_add] at ht,
+    exact ht.1 }
+end
+
+lemma measure_to_measurable_add_inter_right {s t : set α}
+  (hs : measurable_set s) (ht : (μ + ν) t ≠ ∞) :
+  ν (to_measurable (μ + ν) t ∩ s) = ν (t ∩ s) :=
+begin
+  rw add_comm at ht ⊢,
+  exact measure_to_measurable_add_inter_left hs ht
+end
+
 /-! ### The complete lattice of measures -/
 
 /-- Measures are partially ordered.

src/measure_theory/measure/measure_space_def.lean

@@ -180,7 +180,8 @@ lemma exists_measurable_superset_forall_eq {ι} [encodable ι] (μ : ι → meas
 by simpa only [← measure_eq_trim]
   using outer_measure.exists_measurable_superset_forall_eq_trim (λ i, (μ i).to_outer_measure) s
 
-/-- A measurable set `t ⊇ s` such that `μ t = μ s`. -/
+/-- A measurable set `t ⊇ s` such that `μ t = μ s`. It even satisifies `μ (t ∩ u) = μ (s ∩ u)` for
+any measurable set `u`, see `measure_to_measurable_inter`. -/
 def to_measurable (μ : measure α) (s : set α) : set α :=
 classical.some (exists_measurable_superset μ s)
 

src/measure_theory/measure/regular.lean

@@ -257,6 +257,17 @@ lemma _root_.set.exists_is_open_lt_add [outer_regular μ] (A : set α) (hA : μ
   ∃ U ⊇ A, is_open U ∧ μ U < μ A + ε :=
 A.exists_is_open_lt_of_lt _ (ennreal.lt_add_right hA hε)
 
+lemma _root_.set.exists_is_open_le_add (A : set α) (μ : measure α) [outer_regular μ]
+  {ε : ℝ≥0∞} (hε : ε ≠ 0) :
+  ∃ U ⊇ A, is_open U ∧ μ U ≤ μ A + ε :=
+begin
+  rcases le_or_lt ∞ (μ A) with H|H,
+  { exact ⟨univ, subset_univ _, is_open_univ,
+      by simp only [top_le_iff.mp H, ennreal.top_add, le_top]⟩ },
+  { rcases A.exists_is_open_lt_add H.ne hε with ⟨U, AU, U_open, hU⟩,
+    exact ⟨U, AU, U_open, hU.le⟩ }
+end
+
 lemma _root_.measurable_set.exists_is_open_diff_lt [opens_measurable_space α]
   [outer_regular μ] {A : set α} (hA : measurable_set A)
   (hA' : μ A ≠ ∞) {ε : ℝ≥0∞} (hε : ε ≠ 0) :