English
Vitali covering theorem with a parametrized family of sets: there exists a disjoint subfamily whose unions and densities satisfy a coherent covering inequality.
Русский
Теорема Витали о покрытии с параметризованной семейством множеств: существует непересекаемая подподборка, чья сумма плотностей удовлетворяет требуемой неравенности покрытия.
LaTeX
$$$\exists u ⊆ t,\ u.Countable ∧ u.PairwiseDisjoint B ∧ ∀ a∈t, ∃ b∈u, (B a ∩ B b).Nonempty ∧ δ a ≤ τ δ b.$$$
Lean4
/-- Assume that around every point there are arbitrarily small scales at which the measure is
doubling. Then the set of closed sets `a` with nonempty interior contained in `closedBall x r` and
covering a fixed proportion `1/C` of the ball `closedBall x (3 * r)` forms a Vitali family.
This is essentially a restatement of the measurable Vitali theorem. -/
protected def vitaliFamily [PseudoMetricSpace α] [MeasurableSpace α] [OpensMeasurableSpace α]
[SecondCountableTopology α] (μ : Measure α) [IsLocallyFiniteMeasure μ] (C : ℝ≥0)
(h : ∀ x, ∃ᶠ r in 𝓝[>] 0, μ (closedBall x (3 * r)) ≤ C * μ (closedBall x r)) : VitaliFamily μ
where
setsAt x := {a | IsClosed a ∧ (interior a).Nonempty ∧ ∃ r, a ⊆ closedBall x r ∧ μ (closedBall x (3 * r)) ≤ C * μ a}
measurableSet _ _ ha := ha.1.measurableSet
nonempty_interior _ _ ha := ha.2.1
nontrivial x ε
εpos :=
by
obtain ⟨r, μr, rpos, rε⟩ : ∃ r, μ (closedBall x (3 * r)) ≤ C * μ (closedBall x r) ∧ r ∈ Ioc (0 : ℝ) ε :=
((h x).and_eventually (Ioc_mem_nhdsGT εpos)).exists
refine ⟨closedBall x r, ⟨isClosed_closedBall, ?_, ⟨r, Subset.rfl, μr⟩⟩, closedBall_subset_closedBall rε⟩
exact (nonempty_ball.2 rpos).mono ball_subset_interior_closedBall
covering := by
intro s f fsubset ffine
let t : Set (ℝ × α × Set α) :=
{p |
p.2.2 ⊆ closedBall p.2.1 p.1 ∧
μ (closedBall p.2.1 (3 * p.1)) ≤ C * μ p.2.2 ∧
(interior p.2.2).Nonempty ∧ IsClosed p.2.2 ∧ p.2.2 ∈ f p.2.1 ∧ p.2.1 ∈ s}
have A : ∀ x ∈ s, ∀ ε : ℝ, ε > 0 → ∃ p, p ∈ t ∧ p.1 ≤ ε ∧ p.2.1 = x :=
by
intro x xs ε εpos
rcases ffine x xs ε εpos with ⟨a, ha, h'a⟩
rcases fsubset x xs ha with ⟨a_closed, a_int, ⟨r, ar, μr⟩⟩
refine ⟨⟨min r ε, x, a⟩, ⟨?_, ?_, a_int, a_closed, ha, xs⟩, min_le_right _ _, rfl⟩
· rcases min_cases r ε with (h' | h') <;> rwa [h'.1]
· apply le_trans ?_ μr
gcongr
apply min_le_left
rcases
exists_disjoint_covering_ae μ s t C (fun p => p.1) (fun p => p.2.1) (fun p => p.2.2) (fun p hp => hp.1)
(fun p hp => hp.2.1) (fun p hp => hp.2.2.1) (fun p hp => hp.2.2.2.1) A with
⟨t', t't, _, t'_disj, μt'⟩
refine ⟨(fun p : ℝ × α × Set α => p.2) '' t', ?_, ?_, ?_, ?_⟩
· rintro - ⟨q, hq, rfl⟩
exact (t't hq).2.2.2.2.2
· rintro p ⟨q, hq, rfl⟩ p' ⟨q', hq', rfl⟩ hqq'
exact t'_disj hq hq' (ne_of_apply_ne _ hqq')
· rintro - ⟨q, hq, rfl⟩
exact (t't hq).2.2.2.2.1
· convert μt' using 3
rw [biUnion_image]
