feat(measure_theory/covering/vitali_family): define Vitali families (#…

…10057)

Vitali families are families of sets (for instance balls around each point in vector spaces) that satisfy covering theorems. Their main feature is that differentiation of measure theorems hold along Vitali families. This PR is a stub defining Vitali families, and giving examples of them thanks to the Besicovitch and Vitali covering theorems.

The differentiation theorem is left for another PR.

src/data/set/pairwise.lean

@@ -184,6 +184,19 @@ lemma pairwise.set_pairwise (h : pairwise r) (s : set α) : s.pairwise r := λ x
 
 end pairwise
 
+lemma pairwise_subtype_iff_pairwise_set {α : Type*} (s : set α) (r : α → α → Prop) :
+  pairwise (λ (x : s) (y : s), r x y) ↔ s.pairwise r :=
+begin
+  split,
+  { assume h x hx y hy hxy,
+    exact h ⟨x, hx⟩ ⟨y, hy⟩ (by simpa only [subtype.mk_eq_mk, ne.def]) },
+  { rintros h ⟨x, hx⟩ ⟨y, hy⟩ hxy,
+    simp only [subtype.mk_eq_mk, ne.def] at hxy,
+    exact h x hx y hy hxy }
+end
+
+alias pairwise_subtype_iff_pairwise_set ↔ pairwise.set_of_subtype set.pairwise.subtype
+
 namespace set
 section semilattice_inf_bot
 variables [semilattice_inf_bot α] {s t : set ι} {f g : ι → α}
@@ -202,9 +215,9 @@ lemma pairwise_disjoint.mono_on (hs : s.pairwise_disjoint f) (h : ∀ ⦃i⦄, i
 lemma pairwise_disjoint.mono (hs : s.pairwise_disjoint f) (h : g ≤ f) : s.pairwise_disjoint g :=
 hs.mono_on (λ i _, h i)
 
-lemma pairwise_disjoint_empty : (∅ : set ι).pairwise_disjoint f := pairwise_empty _
+@[simp] lemma pairwise_disjoint_empty : (∅ : set ι).pairwise_disjoint f := pairwise_empty _
 
-lemma pairwise_disjoint_singleton (i : ι) (f : ι → α) : pairwise_disjoint {i} f :=
+@[simp] lemma pairwise_disjoint_singleton (i : ι) (f : ι → α) : pairwise_disjoint {i} f :=
 pairwise_singleton i _
 
 lemma pairwise_disjoint_insert {i : ι} :

src/measure_theory/covering/besicovitch.lean

@@ -6,6 +6,7 @@ Authors: Sébastien Gouëzel
 import topology.metric_space.basic
 import set_theory.cardinal_ordinal
 import measure_theory.integral.lebesgue
+import measure_theory.covering.vitali_family
 
 /-!
 # Besicovitch covering theorems
@@ -848,4 +849,58 @@ begin
     rwa [← im_t, A.pairwise_disjoint_image] at v_disj }
 end
 
+/-- In a space with the Besicovitch covering property, the set of closed balls with positive radius
+forms a Vitali family. This is essentially a restatement of the measurable Besicovitch theorem. -/
+protected def vitali_family [second_countable_topology α] [has_besicovitch_covering α]
+  [measurable_space α] [opens_measurable_space α] (μ : measure α) [sigma_finite μ] :
+  vitali_family μ :=
+{ sets_at := λ x, (λ (r : ℝ), closed_ball x r) '' (Ioi (0 : ℝ)),
+  measurable_set' := begin
+    assume x y hy,
+    obtain ⟨r, rpos, rfl⟩ : ∃ (r : ℝ), 0 < r ∧ closed_ball x r = y,
+      by simpa only [mem_image, mem_Ioi] using hy,
+    exact is_closed_ball.measurable_set
+  end,
+  nonempty_interior := begin
+    assume x y hy,
+    obtain ⟨r, rpos, rfl⟩ : ∃ (r : ℝ), 0 < r ∧ closed_ball x r = y,
+      by simpa only [mem_image, mem_Ioi] using hy,
+    simp only [nonempty.mono ball_subset_interior_closed_ball, rpos, nonempty_ball],
+  end,
+  nontrivial := λ x ε εpos, ⟨closed_ball x ε, mem_image_of_mem _ εpos, subset.refl _⟩,
+  covering := begin
+    assume s f fsubset ffine,
+    let g : α → set ℝ := λ x, {r | 0 < r ∧ closed_ball x r ∈ f x},
+    have A : ∀ x ∈ s, (g x).nonempty,
+    { assume x xs,
+      obtain ⟨t, tf, ht⟩ : ∃ (t : set α) (H : t ∈ f x), t ⊆ closed_ball x 1 :=
+        ffine x xs 1 zero_lt_one,
+      obtain ⟨r, rpos, rfl⟩ : ∃ (r : ℝ), 0 < r ∧ closed_ball x r = t,
+        by simpa using fsubset x xs tf,
+      exact ⟨r, rpos, tf⟩ },
+    have B : ∀ x ∈ s, g x ⊆ Ioi (0 : ℝ),
+    { assume x xs r hr,
+      replace hr : 0 < r ∧ closed_ball x r ∈ f x, by simpa only using hr,
+      exact hr.1 },
+    have C : ∀ x ∈ s, Inf (g x) ≤ 0,
+    { assume x xs,
+      have g_bdd : bdd_below (g x) := ⟨0, λ r hr, hr.1.le⟩,
+      refine le_of_forall_le_of_dense (λ ε εpos, _),
+      obtain ⟨t, tf, ht⟩ : ∃ (t : set α) (H : t ∈ f x), t ⊆ closed_ball x ε := ffine x xs ε εpos,
+      obtain ⟨r, rpos, rfl⟩ : ∃ (r : ℝ), 0 < r ∧ closed_ball x r = t,
+        by simpa using fsubset x xs tf,
+      rcases le_total r ε with H|H,
+      { exact (cInf_le g_bdd ⟨rpos, tf⟩).trans H },
+      { have : closed_ball x r = closed_ball x ε :=
+          subset.antisymm ht (closed_ball_subset_closed_ball H),
+        rw this at tf,
+        exact cInf_le g_bdd ⟨εpos, tf⟩ } },
+    obtain ⟨t, r, t_count, ts, tg, μt, tdisj⟩ : ∃ (t : set α) (r : α → ℝ), countable t
+      ∧ t ⊆ s ∧ (∀ x ∈ t, r x ∈ g x)
+      ∧ μ (s \ (⋃ (x ∈ t), closed_ball x (r x))) = 0
+      ∧ t.pairwise_disjoint (λ x, closed_ball x (r x)) :=
+        exists_disjoint_closed_ball_covering_ae μ g s A B C,
+    exact ⟨t, λ x, closed_ball x (r x), ts, tdisj, λ x xt, (tg x xt).2, μt⟩,
+  end }
+
 end besicovitch

src/measure_theory/covering/vitali.lean

@@ -5,6 +5,7 @@ Authors: Sébastien Gouëzel
 -/
 import topology.metric_space.basic
 import measure_theory.constructions.borel_space
+import measure_theory.covering.vitali_family
 
 /-!
 # Vitali covering theorems
@@ -26,6 +27,10 @@ where `μ` is a doubling measure and `t` is a family of balls). Consider a set `
 family is fine, i.e., every point of `s` belongs to arbitrarily small elements of `t`. Then one
 can extract from `t` a disjoint subfamily that covers almost all `s`. It is proved in
 `vitali.exists_disjoint_covering_ae`.
+
+A way to restate this theorem is to say that the set of closed sets `a` with nonempty interior
+covering a fixed proportion `1/C` of the ball `closed_ball x (3 * diam a)` forms a Vitali family.
+This version is given in `vitali.vitali_family`.
 -/
 
 variables {α : Type*}
@@ -427,4 +432,79 @@ begin
   ... ≤ ε : ennreal.mul_div_le,
 end
 
+/-- Assume that around every point there are arbitrarily small scales at which the measure is
+doubling. Then the set of closed sets `a` with nonempty interior covering a fixed proportion `1/C`
+of the ball `closed_ball x (3 * diam a)` forms a Vitali family. This is essentially a restatement
+of the measurable Vitali theorem. -/
+protected def vitali_family [metric_space α] [measurable_space α] [opens_measurable_space α]
+  [second_countable_topology α] (μ : measure α) [is_locally_finite_measure μ] (C : ℝ≥0)
+  (h : ∀ x (ε > 0), ∃ r ∈ Ioc (0 : ℝ) ε, μ (closed_ball x (6 * r)) ≤ C * μ (closed_ball x r)) :
+  vitali_family μ :=
+{ sets_at := λ x, {a | x ∈ a ∧ is_closed a ∧ (interior a).nonempty ∧
+                      μ (closed_ball x (3 * diam a)) ≤ C * μ a},
+  measurable_set' := λ x a ha, ha.2.1.measurable_set,
+  nonempty_interior := λ x a ha, ha.2.2.1,
+  nontrivial := λ x ε εpos, begin
+    obtain ⟨r, ⟨rpos, rε⟩, μr⟩ : ∃ r ∈ Ioc (0 : ℝ) ε,
+      μ (closed_ball x (6 * r)) ≤ C * μ (closed_ball x r) := h x ε εpos,
+    refine ⟨closed_ball x r, ⟨_, is_closed_ball, _, _⟩, closed_ball_subset_closed_ball rε⟩,
+    { simp only [rpos.le, mem_closed_ball, dist_self] },
+    { exact (nonempty_ball.2 rpos).mono (ball_subset_interior_closed_ball) },
+    { apply le_trans (measure_mono (closed_ball_subset_closed_ball _)) μr,
+      have : diam (closed_ball x r) ≤ 2 * r := diam_closed_ball rpos.le,
+      linarith }
+  end,
+  covering := begin
+    assume s f fsubset ffine,
+    rcases eq_empty_or_nonempty s with rfl|H,
+    { exact ⟨∅, λ _, ∅, by simp, by simp⟩ },
+    haveI : inhabited α, { choose x hx using H, exact ⟨x⟩ },
+    let t := ⋃ (x ∈ s), f x,
+    have A₁ : ∀ x ∈ s, ∀ (ε : ℝ), 0 < ε → (∃ a ∈ t, x ∈ a ∧ a ⊆ closed_ball x ε),
+    { assume x xs ε εpos,
+      rcases ffine x xs ε εpos with ⟨a, xa, hax⟩,
+      exact ⟨a, mem_bUnion xs xa, (fsubset x xs xa).1, hax⟩ },
+    have A₂ : ∀ a ∈ t, (interior a).nonempty,
+    { rintros a ha,
+      rcases mem_bUnion_iff.1 ha with ⟨x, xs, xa⟩,
+      exact (fsubset x xs xa).2.2.1 },
+    have A₃ : ∀ a ∈ t, is_closed a,
+    { rintros a ha,
+      rcases mem_bUnion_iff.1 ha with ⟨x, xs, xa⟩,
+      exact (fsubset x xs xa).2.1 },
+    have A₄ : ∀ a ∈ t, ∃ x ∈ a, μ (closed_ball x (3 * diam a)) ≤ C * μ a,
+    { rintros a ha,
+      rcases mem_bUnion_iff.1 ha with ⟨x, xs, xa⟩,
+      exact ⟨x, (fsubset x xs xa).1, (fsubset x xs xa).2.2.2⟩ },
+    obtain ⟨u, ut, u_count, u_disj, μu⟩ :
+      ∃ u ⊆ t, u.countable ∧ u.pairwise disjoint ∧ μ (s \ ⋃ a ∈ u, a) = 0 :=
+        exists_disjoint_covering_ae μ s t A₁ A₂ A₃ C A₄,
+    have : ∀ a ∈ u, ∃ x ∈ s, a ∈ f x := λ a ha, mem_bUnion_iff.1 (ut ha),
+    choose! x hx using this,
+    have inj_on_x : inj_on x u,
+    { assume a ha b hb hab,
+      have A : (a ∩ b).nonempty,
+      { refine ⟨x a, mem_inter ((fsubset _ (hx a ha).1 (hx a ha).2).1) _⟩,
+        rw hab,
+        exact (fsubset _ (hx b hb).1 (hx b hb).2).1 },
+      contrapose A,
+      have : disjoint a b := u_disj a ha b hb A,
+      simpa only [← not_disjoint_iff_nonempty_inter] },
+    refine ⟨x '' u, function.inv_fun_on x u, _, _, _, _⟩,
+    { assume y hy,
+      rcases (mem_image _ _ _).1 hy with ⟨a, au, rfl⟩,
+      exact (hx a au).1 },
+    { rw [inj_on_x.pairwise_disjoint_image],
+      assume a ha b hb hab,
+      simp only [function.on_fun, function.inv_fun_on_eq' inj_on_x, ha, hb, (∘)],
+      exact u_disj a ha b hb hab },
+    { assume y hy,
+      rcases (mem_image _ _ _).1 hy with ⟨a, ha, rfl⟩,
+      rw function.inv_fun_on_eq' inj_on_x ha,
+      exact (hx a ha).2 },
+    { rw [bUnion_image],
+      convert μu using 3,
+      exact bUnion_congr (λ a ha, function.inv_fun_on_eq' inj_on_x ha) }
+  end }
+
 end vitali