Vitali.exists_disjoint_covering_ae
theorem Vitali.exists_disjoint_covering_ae :
∀ {α : Type u_1} {ι : Type u_2} [inst : MetricSpace α] [inst_1 : MeasurableSpace α]
[inst_2 : OpensMeasurableSpace α] [inst_3 : SecondCountableTopology α] (μ : MeasureTheory.Measure α)
[inst_4 : MeasureTheory.IsLocallyFiniteMeasure μ] (s : Set α) (t : Set ι) (C : NNReal) (r : ι → ℝ) (c : ι → α)
(B : ι → Set α),
(∀ a ∈ t, B a ⊆ Metric.closedBall (c a) (r a)) →
(∀ a ∈ t, ↑↑μ (Metric.closedBall (c a) (3 * r a)) ≤ ↑C * ↑↑μ (B a)) →
(∀ a ∈ t, (interior (B a)).Nonempty) →
(∀ a ∈ t, IsClosed (B a)) →
(∀ x ∈ s, ∀ ε > 0, ∃ a ∈ t, r a ≤ ε ∧ c a = x) →
∃ u ⊆ t, u.Countable ∧ u.PairwiseDisjoint B ∧ ↑↑μ (s \ ⋃ a ∈ u, B a) = 0
The Vitali Covering Theorem in the realm of measure theory is as follows. Suppose we have a measure space `α` with a metric, a second countable topological structure, a measure `μ` that is locally finite, and a set `s` within this space. We also have a family of sets `t`, a nonnegative real number `C`, functions `r` and `c` that map each element of `t` to a real number and a point in the space respectively, and a function `B` that maps each element of `t` to a set in the space.
Assume the following conditions are met:
1. Each set `B a` for `a ∈ t` is a subset of the closed ball around `c a` with radius `r a`.
2. The measure of the closed ball around `c a` with radius `3 * r a` is at most `C` times the measure of `B a` for every `a ∈ t`.
3. Each set `B a` for `a ∈ t` has a nonempty interior.
4. Each set `B a` for `a ∈ t` is closed.
5. Each point `x` in `s` belongs to arbitrarily small sets `B a`, `a ∈ t`.
Then, the theorem states that there exists a countable subfamily `u` of `t` such that `u` forms a pairwise disjoint family under `B` and the measure of the set `s` minus the union of all sets `B a` for `a ∈ u` is zero. This means we can find a disjoint subfamily in `t` that covers almost all of the set `s`.
More concisely: Given a measure space with a metric, a second countable topology, a locally finite measure, and a set, if there exists a family of sets satisfying certain conditions including being subsets of closed balls, having measures bounded by a constant times their ball radii, nonempty interiors, closures, and arbitrarily small intersections with the given set, then there exist countably many sets in the family that cover all but a measure-zero subset of the set.
|
Vitali.exists_disjoint_subfamily_covering_enlargment
theorem Vitali.exists_disjoint_subfamily_covering_enlargment :
∀ {α : Type u_1} {ι : Type u_2} (B : ι → Set α) (t : Set ι) (δ : ι → ℝ) (τ : ℝ),
1 < τ →
(∀ a ∈ t, 0 ≤ δ a) →
∀ (R : ℝ),
(∀ a ∈ t, δ a ≤ R) →
(∀ a ∈ t, (B a).Nonempty) →
∃ u ⊆ t, u.PairwiseDisjoint B ∧ ∀ a ∈ t, ∃ b ∈ u, (B a ∩ B b).Nonempty ∧ δ a ≤ τ * δ b
The **Vitali Covering Theorem** states that given a set `t` of subsets of a type, indexed by `ι`, we can extract a disjoint subfamily `u` such that the `τ`-enlargment of this family covers all elements of `t`, where `τ > 1` is a given fixed number. The enlargment is considered in terms of a function `δ` (representing "radius" or "diameter"), which is positive and bounded on all elements of `t`. The requirement is that for every element `a` of `t`, there should be an element `b` of `u` of size larger than `a`'s size, scaled by `τ`, i.e., `δ b ≥ δ a / τ`.
The theorem is stated more broadly, with an indexed family of sets `B a` for `a ∈ t`, for wider applicability. For every `a ∈ t`, `(B a)` must be nonempty. The theorem ensures the existence of a subfamily `u ⊆ t` that is pairwise disjoint and for each `a ∈ t`, there is a `b ∈ u` such that `(B a ∩ B b)` is nonempty and `δ a ≤ τ * δ b`.
More concisely: Given a set of subsets of a type indexed by ι, with a fixed number τ > 1 and a bounded, positive function δ, there exists a disjoint subfamily with the property that for every element a, there is a larger element b in the subfamily with non-empty intersection and scaled diameter relation. (δb ≥ δa/τ)
|
Vitali.exists_disjoint_subfamily_covering_enlargment_closedBall
theorem Vitali.exists_disjoint_subfamily_covering_enlargment_closedBall :
∀ {α : Type u_1} {ι : Type u_2} [inst : MetricSpace α] (t : Set ι) (x : ι → α) (r : ι → ℝ) (R : ℝ),
(∀ a ∈ t, r a ≤ R) →
∃ u ⊆ t,
(u.PairwiseDisjoint fun a => Metric.closedBall (x a) (r a)) ∧
∀ a ∈ t, ∃ b ∈ u, Metric.closedBall (x a) (r a) ⊆ Metric.closedBall (x b) (5 * r b)
The Vitali covering theorem for closed balls states that for any type `α` (equipped with a metric space structure), an index type `ι`, a family `t` of indices, a function `x` mapping each index to a point in `α`, a function `r` assigning a real number to each index (representing radii of the balls), and a real number `R`, if each radius `r(a)` for `a` in `t` is less than or equal to `R`, then there exists a subfamily `u` of `t` (i.e., `u` is a subset of `t`) that is pairwise disjoint (i.e., any two different elements in `u` have disjoint closed balls) such that each closed ball in `t` (centered at `x(a)` with radius `r(a)`) is covered by a larger closed ball in `u` (specifically, centered at the same point but with radius 5 times the original radius).
In other words, we can find a collection of non-overlapping closed balls that, when expanded by a factor of 5, cover all the closed balls in the original family.
More concisely: Given a metric space `(α, d)`, a family `{B(x(i), r(i))}_{i ∈ ι}` of closed balls with pairwise disjoint open balls and radii `r(i)` less than or equal to `R`, there exists a subfamily `{B(x(j), 5r(j))}_{j ∈ J}` that covers the original family.
|