Besicovitch covering theorems

The topological Besicovitch covering theorem ensures that, in a nice metric space, there exists a number N such that, from any family of balls with bounded radii, one can extract N families, each made of disjoint balls, covering together all the centers of the initial family.

By "nice metric space", we mean a technical property stated as follows: there exists no satellite configuration of N + 1 points (with a given parameter τ > 1). Such a configuration is a family of N + 1 balls, where the first N balls all intersect the last one, but none of them contains the center of another one and their radii are controlled. This property is for instance satisfied by finite-dimensional real vector spaces.

In this file, we prove the topological Besicovitch covering theorem, in Besicovitch.exist_disjoint_covering_families.

The measurable Besicovitch theorem ensures that, in the same class of metric spaces, if at every point one considers a class of balls of arbitrarily small radii, called admissible balls, then one can cover almost all the space by a family of disjoint admissible balls. It is deduced from the topological Besicovitch theorem, and proved in Besicovitch.exists_disjoint_closedBall_covering_ae.

This implies that balls of small radius form a Vitali family in such spaces. Therefore, theorems on differentiation of measures hold as a consequence of general results. We restate them in this context to make them more easily usable.

Main definitions and results

• SatelliteConfig α N τ is the type of all satellite configurations of N + 1 points in the metric space α, with parameter τ.
• HasBesicovitchCovering is a class recording that there exist N and τ > 1 such that there is no satellite configuration of N + 1 points with parameter τ.
• exist_disjoint_covering_families is the topological Besicovitch covering theorem: from any family of balls one can extract finitely many disjoint subfamilies covering the same set.
• exists_disjoint_closedBall_covering is the measurable Besicovitch covering theorem: from any family of balls with arbitrarily small radii at every point, one can extract countably many disjoint balls covering almost all the space. While the value of N is relevant for the precise statement of the topological Besicovitch theorem, it becomes irrelevant for the measurable one. Therefore, this statement is expressed using the Prop-valued typeclass HasBesicovitchCovering.

We also restate the following specialized versions of general theorems on differentiation of measures:

• Besicovitch.ae_tendsto_rnDeriv ensures that ρ (closedBall x r) / μ (closedBall x r) tends almost surely to the Radon-Nikodym derivative of ρ with respect to μ at x.
• Besicovitch.ae_tendsto_measure_inter_div states that almost every point in an arbitrary set s is a Lebesgue density point, i.e., μ (s ∩ closedBall x r) / μ (closedBall x r) tends to 1 as r tends to 0. A stronger version for measurable sets is given in Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet.

Implementation

Sketch of proof of the topological Besicovitch theorem:

We choose balls in a greedy way. First choose a ball with maximal radius (or rather, since there is no guarantee the maximal radius is realized, a ball with radius within a factor τ of the supremum). Then, remove all balls whose center is covered by the first ball, and choose among the remaining ones a ball with radius close to maximum. Go on forever until there is no available center (this is a transfinite induction in general).

Then define inductively a coloring of the balls. A ball will be of color i if it intersects already chosen balls of color 0, ..., i - 1, but none of color i. In this way, balls of the same color form a disjoint family, and the space is covered by the families of the different colors.

The nontrivial part is to show that at most N colors are used. If one needs N + 1 colors, consider the first time this happens. Then the corresponding ball intersects N balls of the different colors. Moreover, the inductive construction ensures that the radii of all the balls are controlled: they form a satellite configuration with N + 1 balls (essentially by definition of satellite configurations). Since we assume that there are no such configurations, this is a contradiction.

Sketch of proof of the measurable Besicovitch theorem:

From the topological Besicovitch theorem, one can find a disjoint countable family of balls covering a proportion > 1 / (N + 1) of the space. Taking a large enough finite subset of these balls, one gets the same property for finitely many balls. Their union is closed. Therefore, any point in the complement has around it an admissible ball not intersecting these finitely many balls. Applying again the topological Besicovitch theorem, one extracts from these a disjoint countable subfamily covering a proportion > 1 / (N + 1) of the remaining points, and then even a disjoint finite subfamily. Then one goes on again and again, covering at each step a positive proportion of the remaining points, while remaining disjoint from the already chosen balls. The union of all these balls is the desired almost everywhere covering.

Satellite configurations

structure Besicovitch.SatelliteConfig (α : Type u_1) [MetricSpace α] (N : ℕ) (τ : ℝ) : Type u_1

A satellite configuration is a configuration of N+1 points that shows up in the inductive construction for the Besicovitch covering theorem. It depends on some parameter τ ≥ 1.

This is a family of balls (indexed by i : Fin N.succ, with center c i and radius r i) such that the last ball intersects all the other balls (condition inter), and given any two balls there is an order between them, ensuring that the first ball does not contain the center of the other one, and the radius of the second ball can not be larger than the radius of the first ball (up to a factor τ). This order corresponds to the order of choice in the inductive construction: otherwise, the second ball would have been chosen before. This is the condition h.

Finally, the last ball is chosen after all the other ones, meaning that h can be strengthened by keeping only one side of the alternative in hlast.

• c : Fin N.succ → α
• r : Fin N.succ → ℝ
• rpos : ∀ (i : Fin N.succ), 0 < self.r i
• h : Pairwise fun (i j : Fin N.succ) => self.r i ≤ dist (self.c i) (self.c j) ∧ self.r j ≤ τ * self.r i ∨ self.r j ≤ dist (self.c j) (self.c i) ∧ self.r i ≤ τ * self.r j
• hlast : ∀ i < Fin.last N, self.r i ≤ dist (self.c i) (self.c (Fin.last N)) ∧ self.r (Fin.last N) ≤ τ * self.r i
• inter : ∀ i < Fin.last N, dist (self.c i) (self.c (Fin.last N)) ≤ self.r i + self.r (Fin.last N)

def Mathlib.Meta.Positivity.evalBesicovitchSatelliteConfigR : Mathlib.Meta.Positivity.PositivityExt

Extension for the positivity tactic: Besicovitch.SatelliteConfig.r.

class HasBesicovitchCovering (α : Type u_1) [MetricSpace α] : Prop

A metric space has the Besicovitch covering property if there exist N and τ > 1 such that there are no satellite configuration of parameter τ with N+1 points. This is the condition that guarantees that the measurable Besicovitch covering theorem holds. It is satisfied by finite-dimensional real vector spaces.

• no_satelliteConfig : ∃ (N : ℕ) (τ : ℝ), 1 < τ ∧ IsEmpty (Besicovitch.SatelliteConfig α N τ)

instance Besicovitch.SatelliteConfig.instInhabited {α : Type u_1} {τ : ℝ} [Inhabited α] [MetricSpace α] : Inhabited (Besicovitch.SatelliteConfig α 0 τ)

There is always a satellite configuration with a single point.

Equations

• One or more equations did not get rendered due to their size.

theorem Besicovitch.SatelliteConfig.inter' {α : Type u_1} [MetricSpace α] {N : ℕ} {τ : ℝ} (a : Besicovitch.SatelliteConfig α N τ) (i : Fin N.succ) : dist (a.c i) (a.c (Fin.last N)) ≤ a.r i + a.r (Fin.last N)

theorem Besicovitch.SatelliteConfig.hlast' {α : Type u_1} [MetricSpace α] {N : ℕ} {τ : ℝ} (a : Besicovitch.SatelliteConfig α N τ) (i : Fin N.succ) (h : 1 ≤ τ) : a.r (Fin.last N) ≤ τ * a.r i

Extracting disjoint subfamilies from a ball covering

structure Besicovitch.BallPackage (β : Type u_1) (α : Type u_2) : Type (max u_1 u_2)

A ball package is a family of balls in a metric space with positive bounded radii.

• c : β → α
• r : β → ℝ
• rpos : ∀ (b : β), 0 < self.r b
• r_bound : ℝ
• r_le : ∀ (b : β), self.r b ≤ self.r_bound

def Besicovitch.unitBallPackage (α : Type u_1) : Besicovitch.BallPackage α α

The ball package made of unit balls.

Equations

• Besicovitch.unitBallPackage α = { c := id, r := fun (x : α) => 1, rpos := ⋯, r_bound := 1, r_le := ⋯ }

instance Besicovitch.BallPackage.instInhabited (α : Type u_1) : Inhabited (Besicovitch.BallPackage α α)

Equations

• Besicovitch.BallPackage.instInhabited α = { default := Besicovitch.unitBallPackage α }

structure Besicovitch.TauPackage (β : Type u_1) (α : Type u_2) extends Besicovitch.BallPackage β α : Type (max u_1 u_2)

A Besicovitch tau-package is a family of balls in a metric space with positive bounded radii, together with enough data to proceed with the Besicovitch greedy algorithm. We register this in a single structure to make sure that all our constructions in this algorithm only depend on one variable.

• c : β → α
• r : β → ℝ
• rpos : ∀ (b : β), 0 < self.r b
• r_bound : ℝ
• r_le : ∀ (b : β), self.r b ≤ self.r_bound
• τ : ℝ
• one_lt_tau : 1 < self.τ

instance Besicovitch.TauPackage.instInhabited (α : Type u_1) : Inhabited (Besicovitch.TauPackage α α)

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

noncomputable def Besicovitch.TauPackage.index {α : Type u_1} [MetricSpace α] {β : Type u} [Nonempty β] (p : Besicovitch.TauPackage β α) : Ordinal.{u} → β

Choose inductively large balls with centers that are not contained in the union of already chosen balls. This is a transfinite induction.

Equations

• One or more equations did not get rendered due to their size.

def Besicovitch.TauPackage.iUnionUpTo {α : Type u_1} [MetricSpace α] {β : Type u} [Nonempty β] (p : Besicovitch.TauPackage β α) (i : Ordinal.{u}) : Set α

The set of points that are covered by the union of balls selected at steps < i.

Equations

• p.iUnionUpTo i = ⋃ (j : { j : Ordinal.{?u.10} // j < i }), Metric.ball (p.c (p.index ↑j)) (p.r (p.index ↑j))

theorem Besicovitch.TauPackage.monotone_iUnionUpTo {α : Type u_1} [MetricSpace α] {β : Type u} [Nonempty β] (p : Besicovitch.TauPackage β α) : Monotone p.iUnionUpTo

def Besicovitch.TauPackage.R {α : Type u_1} [MetricSpace α] {β : Type u} [Nonempty β] (p : Besicovitch.TauPackage β α) (i : Ordinal.{u}) : ℝ

Supremum of the radii of balls whose centers are not yet covered at step i.

Equations

• p.R i = ⨆ (b : { b : β // p.c b ∉ p.iUnionUpTo i }), p.r ↑b

@[irreducible]

noncomputable def Besicovitch.TauPackage.color {α : Type u_1} [MetricSpace α] {β : Type u} [Nonempty β] (p : Besicovitch.TauPackage β α) : Ordinal.{u} → ℕ

Group the balls into disjoint families, by assigning to a ball the smallest color for which it does not intersect any already chosen ball of this color.

Equations

• One or more equations did not get rendered due to their size.

def Besicovitch.TauPackage.lastStep {α : Type u_1} [MetricSpace α] {β : Type u} [Nonempty β] (p : Besicovitch.TauPackage β α) : Ordinal.{u}

p.lastStep is the first ordinal where the construction stops making sense, i.e., f returns garbage since there is no point left to be chosen. We will only use ordinals before this step.

Equations

• p.lastStep = sInf {i : Ordinal.{?u.35} | ¬∃ (b : β), p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}

theorem Besicovitch.TauPackage.lastStep_nonempty {α : Type u_1} [MetricSpace α] {β : Type u} [Nonempty β] (p : Besicovitch.TauPackage β α) : {i : Ordinal.{u} | ¬∃ (b : β), p.c b ∉ p.iUnionUpTo i ∧ p.R i ≤ p.τ * p.r b}.Nonempty

theorem Besicovitch.TauPackage.mem_iUnionUpTo_lastStep {α : Type u_1} [MetricSpace α] {β : Type u} [Nonempty β] (p : Besicovitch.TauPackage β α) (x : β) : p.c x ∈ p.iUnionUpTo p.lastStep

Every point is covered by chosen balls, before p.lastStep.

theorem Besicovitch.TauPackage.color_lt {α : Type u_1} [MetricSpace α] {β : Type u} [Nonempty β] (p : Besicovitch.TauPackage β α) {i : Ordinal.{u}} (hi : i < p.lastStep) {N : ℕ} (hN : IsEmpty (Besicovitch.SatelliteConfig α N p.τ)) : p.color i < N

If there are no configurations of satellites with N+1 points, one never uses more than N distinct families in the Besicovitch inductive construction.

theorem Besicovitch.exist_disjoint_covering_families {α : Type u_1} [MetricSpace α] {β : Type u} {N : ℕ} {τ : ℝ} (hτ : 1 < τ) (hN : IsEmpty (Besicovitch.SatelliteConfig α N τ)) (q : Besicovitch.BallPackage β α) : ∃ (s : Fin N → Set β), (∀ (i : Fin N), (s i).PairwiseDisjoint fun (j : β) => Metric.closedBall (q.c j) (q.r j)) ∧ Set.range q.c ⊆ ⋃ (i : Fin N), ⋃ j ∈ s i, Metric.ball (q.c j) (q.r j)

The topological Besicovitch covering theorem: there exist finitely many families of disjoint balls covering all the centers in a package. More specifically, one can use N families if there are no satellite configurations with N+1 points.

The measurable Besicovitch covering theorem

theorem Besicovitch.exist_finset_disjoint_balls_large_measure {α : Type u_1} [MetricSpace α] [SecondCountableTopology α] [MeasurableSpace α] [OpensMeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] {N : ℕ} {τ : ℝ} (hτ : 1 < τ) (hN : IsEmpty (Besicovitch.SatelliteConfig α N τ)) (s : Set α) (r : α → ℝ) (rpos : ∀ x ∈ s, 0 < r x) (rle : ∀ x ∈ s, r x ≤ 1) : ∃ (t : Finset α), ↑t ⊆ s ∧ μ (s \ ⋃ x ∈ t, Metric.closedBall x (r x)) ≤ ↑N / (↑N + 1) * μ s ∧ (↑t).PairwiseDisjoint fun (x : α) => Metric.closedBall x (r x)

Consider, for each x in a set s, a radius r x ∈ (0, 1]. Then one can find finitely many disjoint balls of the form closedBall x (r x) covering a proportion 1/(N+1) of s, if there are no satellite configurations with N+1 points.

theorem Besicovitch.exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux {α : Type u_1} [MetricSpace α] [SecondCountableTopology α] [MeasurableSpace α] [OpensMeasurableSpace α] [HasBesicovitchCovering α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (f : α → Set ℝ) (s : Set α) (hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Set.Ioo 0 δ).Nonempty) : ∃ (t : Set (α × ℝ)), t.Countable ∧ (∀ p ∈ t, p.1 ∈ s) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, Metric.closedBall p.1 p.2) = 0 ∧ t.PairwiseDisjoint fun (p : α × ℝ) => Metric.closedBall p.1 p.2

The measurable Besicovitch covering theorem. Assume that, for any x in a set s, one is given a set of admissible closed balls centered at x, with arbitrarily small radii. Then there exists a disjoint covering of almost all s by admissible closed balls centered at some points of s. This version requires that the underlying measure is finite, and that the space has the Besicovitch covering property (which is satisfied for instance by normed real vector spaces). It expresses the conclusion in a slightly awkward form (with a subset of α × ℝ) coming from the proof technique. For a version assuming that the measure is sigma-finite, see exists_disjoint_closedBall_covering_ae_aux. For a version giving the conclusion in a nicer form, see exists_disjoint_closedBall_covering_ae.

theorem Besicovitch.exists_disjoint_closedBall_covering_ae_aux {α : Type u_1} [MetricSpace α] [SecondCountableTopology α] [MeasurableSpace α] [OpensMeasurableSpace α] [HasBesicovitchCovering α] (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] (f : α → Set ℝ) (s : Set α) (hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Set.Ioo 0 δ).Nonempty) : ∃ (t : Set (α × ℝ)), t.Countable ∧ (∀ p ∈ t, p.1 ∈ s) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, Metric.closedBall p.1 p.2) = 0 ∧ t.PairwiseDisjoint fun (p : α × ℝ) => Metric.closedBall p.1 p.2

The measurable Besicovitch covering theorem. Assume that, for any x in a set s, one is given a set of admissible closed balls centered at x, with arbitrarily small radii. Then there exists a disjoint covering of almost all s by admissible closed balls centered at some points of s. This version requires that the underlying measure is sigma-finite, and that the space has the Besicovitch covering property (which is satisfied for instance by normed real vector spaces). It expresses the conclusion in a slightly awkward form (with a subset of α × ℝ) coming from the proof technique. For a version giving the conclusion in a nicer form, see exists_disjoint_closedBall_covering_ae.

theorem Besicovitch.exists_disjoint_closedBall_covering_ae {α : Type u_1} [MetricSpace α] [SecondCountableTopology α] [MeasurableSpace α] [OpensMeasurableSpace α] [HasBesicovitchCovering α] (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] (f : α → Set ℝ) (s : Set α) (hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Set.Ioo 0 δ).Nonempty) (R : α → ℝ) (hR : ∀ x ∈ s, 0 < R x) : ∃ (t : Set α) (r : α → ℝ), t.Countable ∧ t ⊆ s ∧ (∀ x ∈ t, r x ∈ f x ∩ Set.Ioo 0 (R x)) ∧ μ (s \ ⋃ x ∈ t, Metric.closedBall x (r x)) = 0 ∧ t.PairwiseDisjoint fun (x : α) => Metric.closedBall x (r x)

The measurable Besicovitch covering theorem. Assume that, for any x in a set s, one is given a set of admissible closed balls centered at x, with arbitrarily small radii. Then there exists a disjoint covering of almost all s by admissible closed balls centered at some points of s. We can even require that the radius at x is bounded by a given function R x. (Take R = 1 if you don't need this additional feature). This version requires that the underlying measure is sigma-finite, and that the space has the Besicovitch covering property (which is satisfied for instance by normed real vector spaces).

theorem Besicovitch.exists_closedBall_covering_tsum_measure_le {α : Type u_1} [MetricSpace α] [SecondCountableTopology α] [MeasurableSpace α] [OpensMeasurableSpace α] [HasBesicovitchCovering α] (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] [μ.OuterRegular] {ε : ENNReal} (hε : ε ≠ 0) (f : α → Set ℝ) (s : Set α) (hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Set.Ioo 0 δ).Nonempty) : ∃ (t : Set α) (r : α → ℝ), t.Countable ∧ t ⊆ s ∧ (∀ x ∈ t, r x ∈ f x) ∧ s ⊆ ⋃ x ∈ t, Metric.closedBall x (r x) ∧ ∑' (x : ↑t), μ (Metric.closedBall (↑x) (r ↑x)) ≤ μ s + ε

In a space with the Besicovitch property, any set s can be covered with balls whose measures add up to at most μ s + ε, for any positive ε. This works even if one restricts the set of allowed radii around a point x to a set f x which accumulates at 0.

Consequences on differentiation of measures

def Besicovitch.vitaliFamily {α : Type u_1} [MetricSpace α] [SecondCountableTopology α] [MeasurableSpace α] [OpensMeasurableSpace α] [HasBesicovitchCovering α] (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] : VitaliFamily μ

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.

Equations

• Besicovitch.vitaliFamily μ = { setsAt := fun (x : α) => (fun (r : ℝ) => Metric.closedBall x r) '' Set.Ioi 0, measurableSet := ⋯, nonempty_interior := ⋯, nontrivial := ⋯, covering := ⋯ }

theorem Besicovitch.tendsto_filterAt {α : Type u_1} [MetricSpace α] [SecondCountableTopology α] [MeasurableSpace α] [OpensMeasurableSpace α] [HasBesicovitchCovering α] (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] (x : α) : Filter.Tendsto (fun (r : ℝ) => Metric.closedBall x r) (nhdsWithin 0 (Set.Ioi 0)) ((Besicovitch.vitaliFamily μ).filterAt x)

The main feature of the Besicovitch Vitali family is that its filter at a point x corresponds to convergence along closed balls. We record one of the two implications here, which will enable us to deduce specific statements on differentiation of measures in this context from the general versions.

theorem Besicovitch.ae_tendsto_rnDeriv {β : Type u} [MetricSpace β] [MeasurableSpace β] [BorelSpace β] [SecondCountableTopology β] [HasBesicovitchCovering β] (ρ μ : MeasureTheory.Measure β) [MeasureTheory.IsLocallyFiniteMeasure μ] [MeasureTheory.IsLocallyFiniteMeasure ρ] : ∀ᵐ (x : β) ∂μ, Filter.Tendsto (fun (r : ℝ) => ρ (Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (ρ.rnDeriv μ x))

In a space with the Besicovitch covering property, the ratio of the measure of balls converges almost surely to the Radon-Nikodym derivative.

theorem Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet {β : Type u} [MetricSpace β] [MeasurableSpace β] [BorelSpace β] [SecondCountableTopology β] [HasBesicovitchCovering β] (μ : MeasureTheory.Measure β) [MeasureTheory.IsLocallyFiniteMeasure μ] {s : Set β} (hs : MeasurableSet s) : ∀ᵐ (x : β) ∂μ, Filter.Tendsto (fun (r : ℝ) => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (s.indicator 1 x))

Given a measurable set s, then μ (s ∩ closedBall x r) / μ (closedBall x r) converges when r tends to 0, for almost every x. The limit is 1 for x ∈ s and 0 for x ∉ s. This shows that almost every point of s is a Lebesgue density point for s. A version for non-measurable sets holds, but it only gives the first conclusion, see ae_tendsto_measure_inter_div.

theorem Besicovitch.ae_tendsto_measure_inter_div {β : Type u} [MetricSpace β] [MeasurableSpace β] [BorelSpace β] [SecondCountableTopology β] [HasBesicovitchCovering β] (μ : MeasureTheory.Measure β) [MeasureTheory.IsLocallyFiniteMeasure μ] (s : Set β) : ∀ᵐ (x : β) ∂μ.restrict s, Filter.Tendsto (fun (r : ℝ) => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)

Given an arbitrary set s, then μ (s ∩ closedBall x r) / μ (closedBall x r) converges to 1 when r tends to 0, for almost every x in s. This shows that almost every point of s is a Lebesgue density point for s. A stronger version holds for measurable sets, see ae_tendsto_measure_inter_div_of_measurableSet.

See also IsUnifLocDoublingMeasure.ae_tendsto_measure_inter_div.