English
Under the Besicovitch framework, if there is no satellite configuration with N points, the colors assigned up to any stage i stay below N; more precisely, color i < N for all i < lastStep when such configurations do not exist.
Русский
В рамках Бесиковитча, если конфигурации спутников из N точек не существует, цвета для всех стадий остаются меньше N; то есть color i < N для всех i < lastStep, если конфигурации отсутствуют.
LaTeX
$$$\forall i < p.lastStep,\; p.color(i) < N$ при отсутствии SatelliteConfig α N p.τ.$$
Lean4
/-- The measurable **Besicovitch covering theorem**.
Assume that, for any `x` in a set `s`, one is given a set of admissible closed balls centered at
`x`, with arbitrarily small radii. Then there exists a disjoint covering of almost all `s` by
admissible closed balls centered at some points of `s`.
This version requires the underlying measure to be sigma-finite, and the space to have the
Besicovitch covering property (which is satisfied for instance by normed real vector spaces).
It expresses the conclusion in a slightly awkward form (with a subset of `α × ℝ`) coming from the
proof technique.
For a version giving the conclusion in a nicer form, see `exists_disjoint_closedBall_covering_ae`.
-/
theorem exists_disjoint_closedBall_covering_ae_aux (μ : Measure α) [SFinite μ] (f : α → Set ℝ) (s : Set α)
(hf : ∀ x ∈ s, ∀ δ > 0, (f x ∩ Ioo 0 δ).Nonempty) :
∃ t : Set (α × ℝ),
t.Countable ∧
(∀ p ∈ t, p.1 ∈ s) ∧
(∀ p ∈ t, p.2 ∈ f p.1) ∧
μ (s \ ⋃ (p : α × ℝ) (_ : p ∈ t), closedBall p.1 p.2) = 0 ∧
t.PairwiseDisjoint fun p => closedBall p.1 p.2 :=
by
/- This is deduced from the finite measure case, by using a finite measure with respect to which
the initial sigma-finite measure is absolutely continuous. -/
rcases exists_isFiniteMeasure_absolutelyContinuous μ with ⟨ν, hν, hμν, -⟩
rcases exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux ν f s hf with ⟨t, t_count, ts, tr, tν, tdisj⟩
exact ⟨t, t_count, ts, tr, hμν tν, tdisj⟩
