English
Let μ be a measure on α with the Besicovitch covering property. Then, at any point x, the family of closed balls centered at x with radius r, as r decreases to 0, converges to the Besicovitch Vitali filter at x. In other words, the map r ↦ closedBall(x,r) tends to the filterAt x of the Vitali family (μ).
Русский
Пусть μ — мера на α, удовлетворяющая свойству покрытия Бесицовича. Тогда при любой точке x семейство закрытых шаров centered at x с радиусами r, стремящимися к 0, сходится к фильтру Бесицовича Витали в точке x. Иными словами, отображение r ↦ closedBall(x,r) стремится к фильтруAt x Vitali-множества (μ).
LaTeX
$$$$\\operatorname{Tendsto}\\left(\\lambda r,\\;\\overline{B}(x,r)\\right)\\left(\\mathcal{N}_{>0}(0)\\right)\\left((Besicovitch.vitaliFamily\\;\\mu).filterAt x\\right)$$$$
Lean4
/-- 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 tendsto_filterAt (μ : Measure α) [SFinite μ] (x : α) :
Tendsto (fun r => closedBall x r) (𝓝[>] 0) ((Besicovitch.vitaliFamily μ).filterAt x) :=
by
intro s hs
simp only [mem_map]
obtain ⟨ε, εpos, hε⟩ :
∃ (ε : ℝ), ε > 0 ∧ ∀ a : Set α, a ∈ (Besicovitch.vitaliFamily μ).setsAt x → a ⊆ closedBall x ε → a ∈ s :=
(VitaliFamily.mem_filterAt_iff _).1 hs
filter_upwards [Ioc_mem_nhdsGT εpos] with _r hr
apply hε
· exact mem_image_of_mem _ hr.1
· exact closedBall_subset_closedBall hr.2
