Shrinking lemma in a proper metric space

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_iUnion_ball_radius_lt {α : Type u} {ι : Type v} [MetricSpace α] [ProperSpace α] {c : ι → α} {s : Set α} {r : ι → ℝ} (hs : IsClosed s) (uf : ∀ 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 fun x ↦ ball (c i) (r i) is a locally finite covering and provides a covering indexed by the same type.

theorem exists_iUnion_ball_eq_radius_lt {α : Type u} {ι : Type v} [MetricSpace α] [ProperSpace α] {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.

theorem exists_subset_iUnion_ball_radius_pos_lt {α : Type u} {ι : Type v} [MetricSpace α] [ProperSpace α] {c : ι → α} {s : Set α} {r : ι → ℝ} (hr : ∀ (i : ι), 0 < r i) (hs : IsClosed s) (uf : ∀ 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.

theorem exists_iUnion_ball_eq_radius_pos_lt {α : Type u} {ι : Type v} [MetricSpace α] [ProperSpace α] {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.

theorem exists_locallyFinite_subset_iUnion_ball_radius_lt {α : Type u} [MetricSpace α] [ProperSpace α] {s : Set α} (hs : IsClosed s) {R : α → ℝ} (hR : ∀ 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)) ∧ (LocallyFinite fun (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_locallyCompact_sigmaCompact_of_nhds_basis_set and exists_subset_iUnion_ball_radius_pos_lt.

theorem exists_locallyFinite_iUnion_eq_ball_radius_lt {α : Type u} [MetricSpace α] [ProperSpace α] {R : α → ℝ} (hR : ∀ (x : α), 0 < R x) : ∃ (ι : Type u) (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

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_locallyCompact_sigmaCompact_of_nhds_basis and exists_iUnion_ball_eq_radius_pos_lt or exists_locallyFinite_subset_iUnion_ball_radius_lt.