Shrinking lemma in a proper metric space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove a few versions of the shrinking lemma for coverings by balls in a proper (pseudo) metric space.

Tags #

shrinking lemma, metric space

theorem exists_subset_Union_ball_radius_lt {α : Type u} {ι : Type v} [metric_space α] [proper_space α] {c : ι → α} {s : set α} {r : ι → ℝ} (hs : is_closed s) (uf : ∀ (x : α), x ∈ s → {i : ι | x ∈ metric.ball (c i) (r i)}.finite) (us : s ⊆ ⋃ (i : ι), metric.ball (c i) (r i)) :

∃ (r' : ι → ℝ), (s ⊆ ⋃ (i : ι), metric.ball (c i) (r' i)) ∧ ∀ (i : ι), r' i < r i

Shrinking lemma for coverings by open balls in a proper metric space. A point-finite open cover of a closed subset of a proper metric space by open balls can be shrunk to a new cover by open balls so that each of the new balls has strictly smaller radius than the old one. This version assumes that λ x, ball (c i) (r i) is a locally finite covering and provides a covering indexed by the same type.

source

theorem exists_Union_ball_eq_radius_lt {α : Type u} {ι : Type v} [metric_space α] [proper_space α] {c : ι → α} {r : ι → ℝ} (uf : ∀ (x : α), {i : ι | x ∈ metric.ball (c i) (r i)}.finite) (uU : (⋃ (i : ι), metric.ball (c i) (r i)) = set.univ) :

∃ (r' : ι → ℝ), (⋃ (i : ι), metric.ball (c i) (r' i)) = set.univ ∧ ∀ (i : ι), r' i < r i

Shrinking lemma for coverings by open balls in a proper metric space. A point-finite open cover of a proper metric space by open balls can be shrunk to a new cover by open balls so that each of the new balls has strictly smaller radius than the old one.

source

theorem exists_subset_Union_ball_radius_pos_lt {α : Type u} {ι : Type v} [metric_space α] [proper_space α] {c : ι → α} {s : set α} {r : ι → ℝ} (hr : ∀ (i : ι), 0 < r i) (hs : is_closed s) (uf : ∀ (x : α), x ∈ s → {i : ι | x ∈ metric.ball (c i) (r i)}.finite) (us : 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)

Shrinking lemma for coverings by open balls in a proper metric space. A point-finite open cover of a closed subset of a proper metric space by nonempty open balls can be shrunk to a new cover by nonempty open balls so that each of the new balls has strictly smaller radius than the old one.

source

theorem exists_Union_ball_eq_radius_pos_lt {α : Type u} {ι : Type v} [metric_space α] [proper_space α] {c : ι → α} {r : ι → ℝ} (hr : ∀ (i : ι), 0 < r i) (uf : ∀ (x : α), {i : ι | x ∈ metric.ball (c i) (r i)}.finite) (uU : (⋃ (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)

Shrinking lemma for coverings by open balls in a proper metric space. A point-finite open cover of a proper metric space by nonempty open balls can be shrunk to a new cover by nonempty open balls so that each of the new balls has strictly smaller radius than the old one.

source

theorem exists_locally_finite_subset_Union_ball_radius_lt {α : Type u} [metric_space α] [proper_space α] {s : set α} (hs : is_closed s) {R : α → ℝ} (hR : ∀ (x : α), x ∈ s → 0 < R x) :

∃ (ι : Type u) (c : ι → α) (r r' : ι → ℝ), (∀ (i : ι), c i ∈ s ∧ 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧ locally_finite (λ (i : ι), metric.ball (c i) (r' i)) ∧ s ⊆ ⋃ (i : ι), metric.ball (c i) (r i)

Let R : α → ℝ be a (possibly discontinuous) function on a proper metric space. Let s be a closed set in α such that R is positive on s. Then there exists a collection of pairs of balls metric.ball (c i) (r i), metric.ball (c i) (r' i) such that

all centers belong to s;
for all i we have 0 < r i < r' i < R (c i);
the family of balls metric.ball (c i) (r' i) is locally finite;
the balls metric.ball (c i) (r i) cover s.

This is a simple corollary of refinement_of_locally_compact_sigma_compact_of_nhds_basis_set and exists_subset_Union_ball_radius_pos_lt.

source

theorem exists_locally_finite_Union_eq_ball_radius_lt {α : Type u} [metric_space α] [proper_space α] {R : α → ℝ} (hR : ∀ (x : α), 0 < R x) :

∃ (ι : Type u) (c : ι → α) (r r' : ι → ℝ), (∀ (i : ι), 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧ locally_finite (λ (i : ι), metric.ball (c i) (r' i)) ∧ (⋃ (i : ι), metric.ball (c i) (r i)) = set.univ

Let R : α → ℝ be a (possibly discontinuous) positive function on a proper metric space. Then there exists a collection of pairs of balls metric.ball (c i) (r i), metric.ball (c i) (r' i) such that

for all i we have 0 < r i < r' i < R (c i);
the family of balls metric.ball (c i) (r' i) is locally finite;
the balls metric.ball (c i) (r i) cover the whole space.

This is a simple corollary of refinement_of_locally_compact_sigma_compact_of_nhds_basis and exists_Union_ball_eq_radius_pos_lt or exists_locally_finite_subset_Union_ball_radius_lt.