English
Given a locally integrable function f, almost every x has the property that, for all j, the restriction of f to the ball B(w_j, δ_j) is integrable with respect to μ.
Русский
Для локально интегрируемой функции f почти для всякого x верно, что для всех j ограничение f на шаре B(w_j, δ_j) интегрируемо по μ.
LaTeX
$$$\forall x,\ almostEvery a in v.filterAt x,\ IntegrableOn f a μ$.$$
Lean4
/-- 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 ae_eventually_measure_pos [SecondCountableTopology α] : ∀ᵐ x ∂μ, ∀ᶠ a in v.filterAt x, 0 < μ a :=
by
set s := {x | ¬∀ᶠ a in v.filterAt x, 0 < μ a} with hs
simp -zeta only [not_lt, not_eventually, nonpos_iff_eq_zero] at hs
change μ s = 0
let f : α → Set (Set α) := fun _ => {a | μ a = 0}
have h : v.FineSubfamilyOn f s := by
intro x hx ε εpos
rw [hs] at hx
simp only [frequently_filterAt_iff, gt_iff_lt, mem_setOf_eq] at hx
rcases hx ε εpos with ⟨a, a_sets, ax, μa⟩
exact ⟨a, ⟨a_sets, μa⟩, ax⟩
refine le_antisymm ?_ bot_le
calc
μ s ≤ ∑' x : h.index, μ (h.covering x) := h.measure_le_tsum
_ = ∑' x : h.index, 0 := by congr; ext1 x; exact h.covering_mem x.2
_ = 0 := by simp only [tsum_zero]
