English
If the neighborhood filter at x has a basis, then the Vitali filter at x has a basis consisting of subsets of each basis element drawn from v.setsAt x.
Русский
Если у локального фильтра в точке x есть базис, то фильтр Vitali в x имеет базис, состоящий из подмножеств элементов базиса, принадлежащих v.setsAt x.
LaTeX
$$$ (nhds x).HasBasis p s \\Rightarrow (v.filterAt x).HasBasis p (\\lambda i, \\{t\\in v.setsAt x \\mid t\\subseteq s(i)\\}).$$$
Lean4
/-- One can enlarge a Vitali family by adding to the sets `f x` at `x` all sets which are not
contained in a `δ`-neighborhood on `x`. This does not change the local filter at a point, but it
can be convenient to get a nicer global behavior. -/
def enlarge (v : VitaliFamily μ) (δ : ℝ) (δpos : 0 < δ) : VitaliFamily μ
where
setsAt x := v.setsAt x ∪ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
measurableSet := by
rintro x s (hs | hs)
exacts [v.measurableSet _ _ hs, hs.1]
nonempty_interior := by
rintro x s (hs | hs)
exacts [v.nonempty_interior _ _ hs, hs.2.1]
nontrivial := by
intro x ε εpos
rcases v.nontrivial x ε εpos with ⟨s, hs, h's⟩
exact ⟨s, mem_union_left _ hs, h's⟩
covering := by
intro s f fset ffine
let g : X → Set (Set X) := fun x => f x ∩ v.setsAt x
have : ∀ x ∈ s, ∀ ε : ℝ, ε > 0 → ∃ t ∈ g x, t ⊆ closedBall x ε :=
by
intro x hx ε εpos
obtain ⟨t, tf, ht⟩ : ∃ t ∈ f x, t ⊆ closedBall x (min ε δ) := ffine x hx (min ε δ) (lt_min εpos δpos)
rcases fset x hx tf with (h't | h't)
· exact ⟨t, ⟨tf, h't⟩, ht.trans (closedBall_subset_closedBall (min_le_left _ _))⟩
· refine False.elim (h't.2.2 ?_)
exact ht.trans (closedBall_subset_closedBall (min_le_right _ _))
rcases v.covering s g (fun x _ => inter_subset_right) this with ⟨t, ts, tdisj, tg, μt⟩
exact ⟨t, ts, tdisj, fun p hp => (tg p hp).1, μt⟩
