Documentation

Mathlib.MeasureTheory.Covering.Differentiation

Differentiation of measures #

On a second countable metric space with a measure μ, consider a Vitali family (i.e., for each x one has a family of sets shrinking to x, with a good behavior with respect to covering theorems). Consider also another measure ρ. Then, for almost every x, the ratio ρ a / μ a converges when a shrinks to x along the Vitali family, towards the Radon-Nikodym derivative of ρ with respect to μ. This is the main theorem on differentiation of measures.

This theorem is proved in this file, under the name VitaliFamily.ae_tendsto_rnDeriv. Note that, almost surely, μ a is eventually positive and finite (see VitaliFamily.ae_eventually_measure_pos and VitaliFamily.eventually_measure_lt_top), so the ratio really makes sense.

For concrete applications, one needs concrete instances of Vitali families, as provided for instance by Besicovitch.vitaliFamily (for balls) or by Vitali.vitaliFamily (for doubling measures).

Specific applications to Lebesgue density points and the Lebesgue differentiation theorem are also derived:

Sketch of proof #

Let v be a Vitali family for μ. Assume for simplicity that ρ is absolutely continuous with respect to μ, as the case of a singular measure is easier.

It is easy to see that a set s on which liminf ρ a / μ a < q satisfies ρ s ≤ q * μ s, by using a disjoint subcovering provided by the definition of Vitali families. Similarly for the limsup. It follows that a set on which ρ a / μ a oscillates has measure 0, and therefore that ρ a / μ a converges almost surely (VitaliFamily.ae_tendsto_div). Moreover, on a set where the limit is close to a constant c, one gets ρ s ∼ c μ s, using again a covering lemma as above. It follows that ρ is equal to μ.withDensity (v.limRatio ρ x), where v.limRatio ρ x is the limit of ρ a / μ a at x (which is well defined almost everywhere). By uniqueness of the Radon-Nikodym derivative, one gets v.limRatio ρ x = ρ.rnDeriv μ x almost everywhere, completing the proof.

There is a difficulty in this sketch: this argument works well when v.limRatio ρ is measurable, but there is no guarantee that this is the case, especially if one doesn't make further assumptions on the Vitali family. We use an indirect argument to show that v.limRatio ρ is always almost everywhere measurable, again based on the disjoint subcovering argument (see VitaliFamily.exists_measurable_supersets_limRatio), and then proceed as sketched above but replacing v.limRatio ρ by a measurable version called v.limRatioMeas ρ.

Counterexample #

The standing assumption in this file is that spaces are second countable. Without this assumption, measures may be zero locally but nonzero globally, which is not compatible with differentiation theory (which deduces global information from local one). Here is an example displaying this behavior.

Define a measure μ by μ s = 0 if s is covered by countably many balls of radius 1, and μ s = ∞ otherwise. This is indeed a countably additive measure, which is moreover locally finite and doubling at small scales. It vanishes on every ball of radius 1, so all the quantities in differentiation theory (defined as ratios of measures as the radius tends to zero) make no sense. However, the measure is not globally zero if the space is big enough.

References #

noncomputable def VitaliFamily.limRatio {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) (ρ : MeasureTheory.Measure α) (x : α) :

The limit along a Vitali family of ρ a / μ a where it makes sense, and garbage otherwise. Do not use this definition: it is only a temporary device to show that this ratio tends almost everywhere to the Radon-Nikodym derivative.

Equations
  • v.limRatio ρ x = limUnder (v.filterAt x) fun (a : Set α) => ρ a / μ a
Instances For
    theorem VitaliFamily.ae_eventually_measure_pos {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) [SecondCountableTopology α] :
    ∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a

    For almost every point x, sufficiently small sets in a Vitali family around x have positive measure. (This is a nontrivial result, following from the covering property of Vitali families).

    theorem VitaliFamily.eventually_measure_lt_top {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) [MeasureTheory.IsLocallyFiniteMeasure μ] (x : α) :
    ∀ᶠ (a : Set α) in v.filterAt x, μ a <

    For every point x, sufficiently small sets in a Vitali family around x have finite measure. (This is a trivial result, following from the fact that the measure is locally finite).

    theorem VitaliFamily.measure_le_of_frequently_le {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] {ρ : MeasureTheory.Measure α} (ν : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure ν] (hρ : ρ.AbsolutelyContinuous μ) (s : Set α) (hs : xs, ∃ᶠ (a : Set α) in v.filterAt x, ρ a ν a) :
    ρ s ν s

    If two measures ρ and ν have, at every point of a set s, arbitrarily small sets in a Vitali family satisfying ρ a ≤ ν a, then ρ s ≤ ν s if ρ ≪ μ.

    theorem VitaliFamily.eventually_filterAt_integrableOn {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) {E : Type u_2} [NormedAddCommGroup E] (x : α) {f : αE} (hf : MeasureTheory.LocallyIntegrable f μ) :
    ∀ᶠ (a : Set α) in v.filterAt x, MeasureTheory.IntegrableOn f a μ
    theorem VitaliFamily.ae_eventually_measure_zero_of_singular {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {ρ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.MutuallySingular μ) :
    ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (a : Set α) => ρ a / μ a) (v.filterAt x) (nhds 0)

    If a measure ρ is singular with respect to μ, then for μ almost every x, the ratio ρ a / μ a tends to zero when a shrinks to x along the Vitali family. This makes sense as μ a is eventually positive by ae_eventually_measure_pos.

    theorem VitaliFamily.null_of_frequently_le_of_frequently_ge {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {ρ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ) {c : NNReal} {d : NNReal} (hcd : c < d) (s : Set α) (hc : xs, ∃ᶠ (a : Set α) in v.filterAt x, ρ a c * μ a) (hd : xs, ∃ᶠ (a : Set α) in v.filterAt x, d * μ a ρ a) :
    μ s = 0

    A set of points s satisfying both ρ a ≤ c * μ a and ρ a ≥ d * μ a at arbitrarily small sets in a Vitali family has measure 0 if c < d. Indeed, the first inequality should imply that ρ s ≤ c * μ s, and the second one that ρ s ≥ d * μ s, a contradiction if 0 < μ s.

    theorem VitaliFamily.ae_tendsto_div {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {ρ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ) :
    ∀ᵐ (x : α) ∂μ, ∃ (c : ENNReal), Filter.Tendsto (fun (a : Set α) => ρ a / μ a) (v.filterAt x) (nhds c)

    If ρ is absolutely continuous with respect to μ, then for almost every x, the ratio ρ a / μ a converges as a shrinks to x along a Vitali family for μ.

    theorem VitaliFamily.ae_tendsto_limRatio {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {ρ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ) :
    ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (a : Set α) => ρ a / μ a) (v.filterAt x) (nhds (v.limRatio ρ x))
    theorem VitaliFamily.exists_measurable_supersets_limRatio {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {ρ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ) {p : NNReal} {q : NNReal} (hpq : p < q) :
    ∃ (a : Set α) (b : Set α), MeasurableSet a MeasurableSet b {x : α | v.limRatio ρ x < p} a {x : α | q < v.limRatio ρ x} b μ (a b) = 0

    Given two thresholds p < q, the sets {x | v.limRatio ρ x < p} and {x | q < v.limRatio ρ x} are obviously disjoint. The key to proving that v.limRatio ρ is almost everywhere measurable is to show that these sets have measurable supersets which are also disjoint, up to zero measure. This is the content of this lemma.

    A measurable version of v.limRatio ρ. Do not use this definition: it is only a temporary device to show that v.limRatio is almost everywhere equal to the Radon-Nikodym derivative.

    Equations
    Instances For
      theorem VitaliFamily.ae_tendsto_limRatioMeas {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {ρ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ) :
      ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (a : Set α) => ρ a / μ a) (v.filterAt x) (nhds (v.limRatioMeas x))
      theorem VitaliFamily.measure_le_mul_of_subset_limRatioMeas_lt {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {ρ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ) {p : NNReal} {s : Set α} (h : s {x : α | v.limRatioMeas x < p}) :
      ρ s p * μ s

      If, for all x in a set s, one has frequently ρ a / μ a < p, then ρ s ≤ p * μ s, as proved in measure_le_of_frequently_le. Since ρ a / μ a tends almost everywhere to v.limRatioMeas hρ x, the same property holds for sets s on which v.limRatioMeas hρ < p.

      theorem VitaliFamily.mul_measure_le_of_subset_lt_limRatioMeas {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {ρ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ) {q : NNReal} {s : Set α} (h : s {x : α | q < v.limRatioMeas x}) :
      q * μ s ρ s

      If, for all x in a set s, one has frequently q < ρ a / μ a, then q * μ s ≤ ρ s, as proved in measure_le_of_frequently_le. Since ρ a / μ a tends almost everywhere to v.limRatioMeas hρ x, the same property holds for sets s on which q < v.limRatioMeas.

      theorem VitaliFamily.measure_limRatioMeas_top {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {ρ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ) :
      μ {x : α | v.limRatioMeas x = } = 0

      The points with v.limRatioMeas hρ x = ∞ have measure 0 for μ.

      theorem VitaliFamily.measure_limRatioMeas_zero {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {ρ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ) :
      ρ {x : α | v.limRatioMeas x = 0} = 0

      The points with v.limRatioMeas hρ x = 0 have measure 0 for ρ.

      theorem VitaliFamily.withDensity_le_mul {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {ρ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ) {s : Set α} (hs : MeasurableSet s) {t : NNReal} (ht : 1 < t) :
      (μ.withDensity (v.limRatioMeas )) s t ^ 2 * ρ s

      As an intermediate step to show that μ.withDensity (v.limRatioMeas hρ) = ρ, we show here that μ.withDensity (v.limRatioMeas hρ) ≤ t^2 ρ for any t > 1.

      theorem VitaliFamily.le_mul_withDensity {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {ρ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ) {s : Set α} (hs : MeasurableSet s) {t : NNReal} (ht : 1 < t) :
      ρ s t * (μ.withDensity (v.limRatioMeas )) s

      As an intermediate step to show that μ.withDensity (v.limRatioMeas hρ) = ρ, we show here that ρ ≤ t μ.withDensity (v.limRatioMeas hρ) for any t > 1.

      theorem VitaliFamily.withDensity_limRatioMeas_eq {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {ρ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ) :
      μ.withDensity (v.limRatioMeas ) = ρ
      theorem VitaliFamily.ae_tendsto_rnDeriv_of_absolutelyContinuous {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {ρ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure ρ] (hρ : ρ.AbsolutelyContinuous μ) :
      ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (a : Set α) => ρ a / μ a) (v.filterAt x) (nhds (ρ.rnDeriv μ x))

      Weak version of the main theorem on differentiation of measures: given a Vitali family v for a locally finite measure μ, and another locally finite measure ρ, then for μ-almost every x the ratio ρ a / μ a converges, when a shrinks to x along the Vitali family, towards the Radon-Nikodym derivative of ρ with respect to μ.

      This version assumes that ρ is absolutely continuous with respect to μ. The general version without this superfluous assumption is VitaliFamily.ae_tendsto_rnDeriv.

      theorem VitaliFamily.ae_tendsto_rnDeriv {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] (ρ : MeasureTheory.Measure α) [MeasureTheory.IsLocallyFiniteMeasure ρ] :
      ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (a : Set α) => ρ a / μ a) (v.filterAt x) (nhds (ρ.rnDeriv μ x))

      Main theorem on differentiation of measures: given a Vitali family v for a locally finite measure μ, and another locally finite measure ρ, then for μ-almost every x the ratio ρ a / μ a converges, when a shrinks to x along the Vitali family, towards the Radon-Nikodym derivative of ρ with respect to μ.

      Lebesgue density points #

      theorem VitaliFamily.ae_tendsto_measure_inter_div_of_measurableSet {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {s : Set α} (hs : MeasurableSet s) :
      ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (a : Set α) => μ (s a) / μ a) (v.filterAt x) (nhds (s.indicator 1 x))

      Given a measurable set s, then μ (s ∩ a) / μ a converges when a shrinks to a typical point x along a Vitali family. 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 VitaliFamily.ae_tendsto_measure_inter_div {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] (s : Set α) :
      ∀ᵐ (x : α) ∂μ.restrict s, Filter.Tendsto (fun (a : Set α) => μ (s a) / μ a) (v.filterAt x) (nhds 1)

      Given an arbitrary set s, then μ (s ∩ a) / μ a converges to 1 when a shrinks to a typical point of s along a Vitali family. This shows that almost every point of s is a Lebesgue density point for s. A stronger version for measurable sets is given in ae_tendsto_measure_inter_div_of_measurableSet.

      Lebesgue differentiation theorem #

      theorem VitaliFamily.ae_tendsto_lintegral_div' {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {f : αENNReal} (hf : Measurable f) (h'f : ∫⁻ (y : α), f yμ ) :
      ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (a : Set α) => (∫⁻ (y : α) in a, f yμ) / μ a) (v.filterAt x) (nhds (f x))
      theorem VitaliFamily.ae_tendsto_lintegral_div {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {f : αENNReal} (hf : AEMeasurable f μ) (h'f : ∫⁻ (y : α), f yμ ) :
      ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (a : Set α) => (∫⁻ (y : α) in a, f yμ) / μ a) (v.filterAt x) (nhds (f x))
      theorem VitaliFamily.ae_tendsto_lintegral_nnnorm_sub_div'_of_integrable {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) {E : Type u_2} [NormedAddCommGroup E] [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {f : αE} (hf : MeasureTheory.Integrable f μ) (h'f : MeasureTheory.StronglyMeasurable f) :
      ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (a : Set α) => (∫⁻ (y : α) in a, f y - f x‖₊μ) / μ a) (v.filterAt x) (nhds 0)
      theorem VitaliFamily.ae_tendsto_lintegral_nnnorm_sub_div_of_integrable {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) {E : Type u_2} [NormedAddCommGroup E] [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {f : αE} (hf : MeasureTheory.Integrable f μ) :
      ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (a : Set α) => (∫⁻ (y : α) in a, f y - f x‖₊μ) / μ a) (v.filterAt x) (nhds 0)
      theorem VitaliFamily.ae_tendsto_lintegral_nnnorm_sub_div {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) {E : Type u_2} [NormedAddCommGroup E] [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {f : αE} (hf : MeasureTheory.LocallyIntegrable f μ) :
      ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (a : Set α) => (∫⁻ (y : α) in a, f y - f x‖₊μ) / μ a) (v.filterAt x) (nhds 0)
      theorem VitaliFamily.ae_tendsto_average_norm_sub {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) {E : Type u_2} [NormedAddCommGroup E] [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] {f : αE} (hf : MeasureTheory.LocallyIntegrable f μ) :
      ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (a : Set α) => ⨍ (y : α) in a, f y - f xμ) (v.filterAt x) (nhds 0)

      Lebesgue differentiation theorem: for almost every point x, the average of ‖f y - f x‖ on a tends to 0 as a shrinks to x along a Vitali family.

      theorem VitaliFamily.ae_tendsto_average {α : Type u_1} [MetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (v : VitaliFamily μ) {E : Type u_2} [NormedAddCommGroup E] [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] [NormedSpace E] [CompleteSpace E] {f : αE} (hf : MeasureTheory.LocallyIntegrable f μ) :
      ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (a : Set α) => ⨍ (y : α) in a, f yμ) (v.filterAt x) (nhds (f x))

      Lebesgue differentiation theorem: for almost every point x, the average of f on a tends to f x as a shrinks to x along a Vitali family.