English
Let w and δ be a sequence of centers and radii with δ → 0+, and assume x lies eventually in the balls centered at w_j with radius K δ_j. Then the balls B(w_j, δ_j) converge to the Vitali filter at x as j → ∞.
Русский
Пусть w_j — последовательность центров, δ_j — последовательность радиусов с δ_j → 0+, и пусть x принадлежит шарикам B(w_j, K δ_j) для больших j. Тогда шарики B(w_j, δ_j) сходятся к фильтру Vitali в x при j → ∞.
LaTeX
$$$(\forall w, \delta)\ (\delta \to 0^+ \,)\ dist(x,w_j) \le K\,\delta_j \implies (\closedBall (w_j) (\delta_j)) \to ((\mathrm{vitaliFamily} μ K).\text{filterAt } x).$$$
Lean4
theorem tendsto_closedBall_filterAt {K : ℝ} {x : α} {ι : Type*} {l : Filter ι} (w : ι → α) (δ : ι → ℝ)
(δlim : Tendsto δ l (𝓝[>] 0)) (xmem : ∀ᶠ j in l, x ∈ closedBall (w j) (K * δ j)) :
Tendsto (fun j => closedBall (w j) (δ j)) l ((vitaliFamily μ K).filterAt x) :=
by
refine (vitaliFamily μ K).tendsto_filterAt_iff.mpr ⟨?_, fun ε hε => ?_⟩
· filter_upwards [xmem, δlim self_mem_nhdsWithin] with j hj h'j
exact closedBall_mem_vitaliFamily_of_dist_le_mul μ hj h'j
· rcases l.eq_or_neBot with rfl | h
· simp
have hK : 0 ≤ K := by
rcases (xmem.and (δlim self_mem_nhdsWithin)).exists with ⟨j, hj, h'j⟩
have : 0 ≤ K * δ j := nonempty_closedBall.1 ⟨x, hj⟩
exact (mul_nonneg_iff_left_nonneg_of_pos (mem_Ioi.1 h'j)).1 this
have δpos := eventually_mem_of_tendsto_nhdsWithin δlim
replace δlim := tendsto_nhds_of_tendsto_nhdsWithin δlim
replace hK : 0 < K + 1 := by linarith
apply (((Metric.tendsto_nhds.mp δlim _ (div_pos hε hK)).and δpos).and xmem).mono
rintro j ⟨⟨hjε, hj₀ : 0 < δ j⟩, hx⟩ y hy
replace hjε : (K + 1) * δ j < ε := by simpa [abs_eq_self.mpr hj₀.le] using (lt_div_iff₀' hK).mp hjε
simp only [mem_closedBall] at hx hy ⊢
linarith [dist_triangle_right y x (w j)]
