exists_iUnion_ball_eq_radius_pos_lt
theorem exists_iUnion_ball_eq_radius_pos_lt :
∀ {α : Type u} {ι : Type v} [inst : MetricSpace α] [inst_1 : ProperSpace α] {c : ι → α} {r : ι → ℝ},
(∀ (i : ι), 0 < r i) →
(∀ (x : α), {i | x ∈ Metric.ball (c i) (r i)}.Finite) →
⋃ i, Metric.ball (c i) (r i) = Set.univ →
∃ r', ⋃ i, Metric.ball (c i) (r' i) = Set.univ ∧ ∀ (i : ι), r' i ∈ Set.Ioo 0 (r i)
The Shrinking Lemma for coverings by open balls in a proper metric space states that, for a given proper metric space type `α` and an index set type `ι`, assuming a metric space structure and a proper space structure on `α`, if we have two functions `c : ι → α` and `r : ι → ℝ` such that the radius `r i` is positive for each `i` in `ι` and the open balls `Metric.ball (c i) (r i)` form a point-finite open cover of the space (that is, each point in the space is contained in only finitely many of these balls), and this cover equals the universal set `Set.univ` (i.e., it covers the entire space), then it is possible to find a new function `r' : ι → ℝ` such that the open balls `Metric.ball (c i) (r' i)` also cover the entire space and the radius `r' i` of each new ball is strictly less than the radius `r i` of the corresponding old ball, while still being positive. In other words, we can "shrink" the balls in the cover to get a new cover where each ball is smaller than before.
More concisely: Given a proper metric space and a point-finite, positive radius open cover of it by balls, there exists a new cover with strictly smaller radii that still covers the entire space.
|
exists_locallyFinite_subset_iUnion_ball_radius_lt
theorem exists_locallyFinite_subset_iUnion_ball_radius_lt :
∀ {α : Type u} [inst : MetricSpace α] [inst_1 : ProperSpace α] {s : Set α},
IsClosed s →
∀ {R : α → ℝ},
(∀ x ∈ s, 0 < R x) →
∃ ι c r r',
(∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
(LocallyFinite fun i => Metric.ball (c i) (r' i)) ∧ s ⊆ ⋃ i, Metric.ball (c i) (r i)
This theorem states that given a function `R : α → ℝ` on a proper metric space that may be discontinuous, and a closed set `s` in `α` where the function `R` is positive, there exists a collection of pairs of balls `Metric.ball (c i) (r i)` and `Metric.ball (c i) (r' i)` such that:
* All the centers of these balls are in the set `s`;
* For every index `i`, the radius `r i` is positive and less than `r' i` which is less than `R (c i)`;
* The family of balls `Metric.ball (c i) (r' i)` is locally finite, meaning that for each point in the space, there is a neighborhood that intersects with only finitely many of these balls;
* The balls `Metric.ball (c i) (r i)` cover the set `s`, meaning that every point in `s` is in at least one of these balls.
This theorem is a direct consequence of the principles `refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set` and `exists_subset_iUnion_ball_radius_pos_lt`, whose implementation details are suppressed.
More concisely: Given a proper metric space `α` with a discontinuous function `R : α → ℝ` that is positive on a closed set `s ⊆ α`, there exists a locally finite collection of pairs of balls `(c i, r i)` and `(c i, r' i)` with centers in `s` and radii `r i > 0` and `r' i < R (c i)` such that the smaller balls cover `s`.
|
exists_subset_iUnion_ball_radius_lt
theorem exists_subset_iUnion_ball_radius_lt :
∀ {α : Type u} {ι : Type v} [inst : MetricSpace α] [inst_1 : ProperSpace α] {c : ι → α} {s : Set α} {r : ι → ℝ},
IsClosed s →
(∀ x ∈ s, {i | x ∈ Metric.ball (c i) (r i)}.Finite) →
s ⊆ ⋃ i, Metric.ball (c i) (r i) → ∃ r', s ⊆ ⋃ i, Metric.ball (c i) (r' i) ∧ ∀ (i : ι), r' i < r i
The **Shrinking lemma** for coverings by open balls in a proper metric space is a theorem stating that given a closed subset `s` of a proper metric space, and a point-finite open cover of `s` by open balls (with centers `c i` and radius `r i`), the cover can be "shrunk" to a new cover by open balls such that each new ball has a strictly smaller radius than its corresponding original ball. More formally, if `s` is a subset of the union of `Metric.ball (c i) (r i)` for all `i`, there exists a new radius function `r'` such that `s` is a subset of the union of `Metric.ball (c i) (r' i)` for all `i`, and for each `i`, `r' i` is less than `r i`. This version of the theorem assumes that `fun x ↦ ball (c i) (r i)` is a locally finite covering and provides a covering indexed by the same type.
More concisely: Given a closed subset of a proper metric space and a point-finite open cover by open balls, there exists a new cover with strictly smaller radii such that the original cover is a subset of the new cover.
|
exists_locallyFinite_iUnion_eq_ball_radius_lt
theorem exists_locallyFinite_iUnion_eq_ball_radius_lt :
∀ {α : Type u} [inst : MetricSpace α] [inst_1 : ProperSpace α] {R : α → ℝ},
(∀ (x : α), 0 < R x) →
∃ ι c r r',
(∀ (i : ι), 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
(LocallyFinite fun i => Metric.ball (c i) (r' i)) ∧ ⋃ i, Metric.ball (c i) (r i) = Set.univ
The theorem `exists_locallyFinite_iUnion_eq_ball_radius_lt` states that for any positive (possibly discontinuous) function `R : α → ℝ` on a proper metric space `α`, there exists a collection of pairs of balls `Metric.ball (c i) (r i)` and `Metric.ball (c i) (r' i)` such that the following conditions are satisfied:
- For each `i`, we have `0 < r i < r' i < R (c i)`.
- The family of balls `Metric.ball (c i) (r' i)` is locally finite, which means that for every point in the space, there exists a neighborhood of the point that intersects with only finitely many balls in the family.
- The union of the balls `Metric.ball (c i) (r i)` covers the entire space, that is, every point in the space belongs to at least one of these balls.
This theorem is a consequence of `refinement_of_locallyCompact_sigmaCompact_of_nhds_basis` and `exists_iUnion_ball_eq_radius_pos_lt` or `exists_locallyFinite_subset_iUnion_ball_radius_lt`.
More concisely: Given a proper metric space and a positive, possibly discontinuous function, there exist locally finite collections of balls with strictly increasing radii such that their unions cover the entire space and each point belongs to at most finitely many balls.
|
exists_subset_iUnion_ball_radius_pos_lt
theorem exists_subset_iUnion_ball_radius_pos_lt :
∀ {α : Type u} {ι : Type v} [inst : MetricSpace α] [inst_1 : ProperSpace α] {c : ι → α} {s : Set α} {r : ι → ℝ},
(∀ (i : ι), 0 < r i) →
IsClosed s →
(∀ x ∈ s, {i | x ∈ Metric.ball (c i) (r i)}.Finite) →
s ⊆ ⋃ i, Metric.ball (c i) (r i) →
∃ r', s ⊆ ⋃ i, Metric.ball (c i) (r' i) ∧ ∀ (i : ι), r' i ∈ Set.Ioo 0 (r i)
This is a theorem about coverings by open balls in a proper metric space, often called the "shrinking lemma". The theorem states that given a closed subset of a proper metric space, if it is covered by a finite collection of open balls such that each ball has a positive radius, then we can find a new collection of open balls with smaller radii that also cover the subset. More formally, for any types `α` and `ι`, a metric space `α`, a collection of points `c : ι → α`, a set `s : Set α`, and a radius function `r : ι → ℝ`, if each radius is positive, `s` is a closed set, each point in `s` is covered by a finite number of the balls, and `s` is a subset of the union of all the balls, then there exists a new radius function `r'` such that `s` is still a subset of the union of the balls with the new radii and each new radius is strictly less than the corresponding old radius.
More concisely: Given a closed subset of a proper metric space, if it is covered by a finite collection of open balls with positive radii, then there exists a new collection of open balls with strictly smaller radii that still cover the subset.
|
exists_iUnion_ball_eq_radius_lt
theorem exists_iUnion_ball_eq_radius_lt :
∀ {α : Type u} {ι : Type v} [inst : MetricSpace α] [inst_1 : ProperSpace α] {c : ι → α} {r : ι → ℝ},
(∀ (x : α), {i | x ∈ Metric.ball (c i) (r i)}.Finite) →
⋃ i, Metric.ball (c i) (r i) = Set.univ →
∃ r', ⋃ i, Metric.ball (c i) (r' i) = Set.univ ∧ ∀ (i : ι), r' i < r i
This theorem is known as the shrinking lemma for coverings by open balls in a proper metric space. It states that given a type `α` which is a metric space and also a proper space, and given a function `c` from `ι` to `α` (which assigns points in the space to each index `ι`) and a real-valued function `r` on `ι` (which assigns a radius value to each index `ι`), such that for every point `x` in the space `α`, the set of all indices `i` for which `x` belongs to the open ball centered at `c i` with radius `r i` is finite, and the union of all such open balls covers the entire space `α`, then there exists a new real-valued function `r'` on `ι`, such that the union of all open balls centered at `c i` with radius `r' i` still covers the entire space, but each of the new balls has a radius `r' i` which is strictly smaller than the old radius `r i`.
More concisely: Given a proper metric space `α` with a function `c: ι → α` and a real-valued function `r: ι → ℝ` such that the union of open balls centered at `c i` with radius `r i` covers `α`, there exists a new real-valued function `r': ι → ℝ` such that the union of open balls centered at `c i` with radius `r' i` still covers `α` and each new radius `r' i` is strictly smaller than the old radius `r i`.
|