Besicovitch covering: density points, subspaces and Lebesgue differentiation

For a null-measurable set s, the proportion of the complement sᶜ in a set of positive finite measure is one minus the proportion of s. Consequently, if the proportion of s along a family of such sets tends to d, that of sᶜ tends to 1 - d; in particular s has density one along the family exactly when sᶜ has density zero along it. This lets density arguments estimate the complement, where measures add, and return to density-one points.

For a locally finite measure on a second-countable metric space with its Borel σ-algebra and the Besicovitch covering property, Mathlib's density theorem Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet identifies the limit of μ (s ∩ closedBall x r) / μ (closedBall x r) almost everywhere for a measurable set. We extend it to null-measurable sets and record its set form: a null-measurable set agrees almost everywhere with its set of density-one points. That set is a canonical representative of the μ-a.e. class of s, since it depends only on that class.

The Besicovitch covering property passes to subspaces (Isometry.hasBesicovitchCovering), so an open subset of a finite-dimensional real normed space has it too. This lets differentiation theorems apply to measures that are only locally finite on an open set, such as derivative measures of functions of locally bounded variation. For such measures, the Besicovitch Vitali family gives the Lebesgue differentiation theorem along concentric closed balls, Besicovitch.ae_tendsto_average_closedBall.

theorem MeasureTheory.NullMeasurableSet.tendsto_measure_compl_inter_div {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {μ : Measure α} {s : Set α} (hs : NullMeasurableSet s μ) {l : Filter ι} {u : ι → Set α} (hu : ∀ᶠ (i : ι) in l, μ (u i) ≠ 0 ∧ μ (u i) ≠ ⊤) {d : ENNReal} (h : Filter.Tendsto (fun (i : ι) => μ (s ∩ u i) / μ (u i)) l (nhds d)) : Filter.Tendsto (fun (i : ι) => μ (sᶜ ∩ u i) / μ (u i)) l (nhds (1 - d))

For a null-measurable set s, along sets of positive finite measure, if the proportion of s tends to d then the proportion of sᶜ tends to 1 - d.

theorem MeasureTheory.NullMeasurableSet.tendsto_measure_compl_inter_div_iff {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] {μ : Measure α} {s : Set α} (hs : NullMeasurableSet s μ) {l : Filter ι} {u : ι → Set α} (hu : ∀ᶠ (i : ι) in l, μ (u i) ≠ 0 ∧ μ (u i) ≠ ⊤) : Filter.Tendsto (fun (i : ι) => μ (sᶜ ∩ u i) / μ (u i)) l (nhds 0) ↔ Filter.Tendsto (fun (i : ι) => μ (s ∩ u i) / μ (u i)) l (nhds 1)

For a null-measurable set s, along sets of positive finite measure the proportion of sᶜ tends to zero exactly when the proportion of s tends to one.

theorem MeasureTheory.NullMeasurableSet.ae_tendsto_measure_inter_div {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {s : Set α} [MetricSpace α] [SecondCountableTopology α] [BorelSpace α] [HasBesicovitchCovering α] [IsLocallyFiniteMeasure μ] (hs : NullMeasurableSet 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))

Lebesgue's density theorem for a null-measurable set s: at almost every point x, the proportion of s in the closed ball around x tends to the value at x of the indicator of s. This extends Besicovitch.ae_tendsto_measure_inter_div_of_measurableSet to null-measurable sets.

theorem MeasureTheory.NullMeasurableSet.ae_eq_setOf_tendsto_measure_inter_div {α : Type u_1} [MeasurableSpace α] {μ : Measure α} {s : Set α} [MetricSpace α] [SecondCountableTopology α] [BorelSpace α] [HasBesicovitchCovering α] [IsLocallyFiniteMeasure μ] (hs : NullMeasurableSet s μ) : s =ᵐ[μ] {x : α | Filter.Tendsto (fun (r : ℝ) => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)}

A null-measurable set agrees almost everywhere with its set of density points with respect to μ, the points at which its proportion of closed balls tends to one.

The Besicovitch covering property for subspaces

theorem Isometry.hasBesicovitchCovering {α : Type u_1} {β : Type u_2} [MetricSpace α] [MetricSpace β] [HasBesicovitchCovering β] {f : α → β} (hf : Isometry f) : HasBesicovitchCovering α

The Besicovitch covering property passes along isometric embeddings: a satellite configuration in the domain maps to one in the codomain.

instance Subtype.hasBesicovitchCovering {α : Type u_1} [MetricSpace α] [HasBesicovitchCovering α] (p : α → Prop) : HasBesicovitchCovering (Subtype p)

A subspace of a metric space with the Besicovitch covering property has it too.

Differentiation along concentric closed balls

theorem Besicovitch.ae_tendsto_average_closedBall {β : Type u_1} {F : Type u_2} [MetricSpace β] [MeasurableSpace β] [BorelSpace β] [SecondCountableTopology β] [HasBesicovitchCovering β] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (μ : MeasureTheory.Measure β) [MeasureTheory.IsLocallyFiniteMeasure μ] {f : β → F} (hf : MeasureTheory.LocallyIntegrable f μ) : ∀ᵐ (x : β) ∂μ, Filter.Tendsto (fun (r : ℝ) => ⨍ (y : β) in Metric.closedBall x r, f y ∂μ) (nhdsWithin 0 (Set.Ioi 0)) (nhds (f x))

Lebesgue's differentiation theorem for a locally finite measure in a space with the Besicovitch covering property: for a locally integrable function f, at almost every point x the averages of f over the closed balls around x tend to f x.