Theorems · Theorem · measure theory

Besicovitch.tendsto_filterAt

∀ {α : Type u_1} [inst : MetricSpace α] [inst_1 : SecondCountableTopology α] [inst_2 : MeasurableSpace α]
  [inst_3 : OpensMeasurableSpace α] [inst_4 : HasBesicovitchCovering α] (μ : MeasureTheory.Measure α)
  [inst_5 : 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.

Defined in

Mathlib.MeasureTheory.Covering.Besicovitch

Cited by

4 results in Mathlib

Foundations

Depth 201 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MetricSpaceSecondCountableTopologyMeasurableSpaceOpensMeasurableSpaceHasBesicovitchCoveringMeasureTheory.SFinite