Proper spaces and compact exhaustions with diverging distance

A pseudometric space is proper, that is, its closed balls are compact, exactly when it admits an increasing sequence of compact sets K n covering it such that the distance from a fixed point p tends to infinity along every sequence q with q n ∉ K n.

In a proper space the closed balls closedBall p n form such an exhaustion. Conversely, the divergence condition alone makes every bounded set lie in some K n, so monotonicity and covering are unnecessary for this direction. The base point p is arbitrary on both sides.

This is the equivalence of assertions (b) and (e) in do Carmo's statement of the Hopf–Rinow theorem. It holds in every pseudometric space; the Riemannian structure plays no role.

Main results

• TauCeti.exists_subset_of_isBounded_of_tendsto_dist: under the divergence condition, every bounded set lies in some K n.
• TauCeti.properSpace_of_isCompact_of_tendsto_dist: compact K n with the divergence condition make the space proper.
• TauCeti.exists_isCompact_monotone_iUnion_eq_univ_tendsto_dist: a proper space has an exhaustion by compact sets with the divergence condition, namely by the closed balls about p.
• TauCeti.properSpace_iff_exists_isCompact_monotone_iUnion_eq_univ_tendsto_dist: the equivalence.
• IsOpen.exists_iUnion_isOpen_isCompact_closure: in a proper space, every open set is the union of an increasing sequence of open sets with compact closures inside it.
• TopologicalSpace.Opens.exists_monotone_isCompact_closure_iUnion_eq: the same exhaustion of an open set Ω, as a sequence of Opens whose traces on the subspace Ω cover it.
• TopologicalSpace.Opens.exists_isCompact_closure_subset_succ_iUnion_eq: an exhaustion of an open set Ω by open sets with compact closures, each closure inside the next set.

References

• M. P. do Carmo, Riemannian Geometry, Birkhäuser, 1992, Ch. 7, §2, Thm. 2.8, the equivalence of assertions (b) and (e).

theorem TauCeti.exists_subset_of_isBounded_of_tendsto_dist {α : Type u_1} [PseudoMetricSpace α] {p : α} {K : ℕ → Set α} (hK : ∀ (q : ℕ → α), (∀ (n : ℕ), q n ∉ K n) → Filter.Tendsto (fun (n : ℕ) => dist p (q n)) Filter.atTop Filter.atTop) {s : Set α} (hs : Bornology.IsBounded s) : ∃ (n : ℕ), s ⊆ K n

If the distance from p tends to infinity along every sequence q with q n ∉ K n, then every bounded set is contained in some K n.

theorem TauCeti.properSpace_of_isCompact_of_tendsto_dist {α : Type u_1} [PseudoMetricSpace α] {p : α} {K : ℕ → Set α} (hKc : ∀ (n : ℕ), IsCompact (K n)) (hK : ∀ (q : ℕ → α), (∀ (n : ℕ), q n ∉ K n) → Filter.Tendsto (fun (n : ℕ) => dist p (q n)) Filter.atTop Filter.atTop) : ProperSpace α

A pseudometric space is proper if it has a sequence of compact sets K n such that the distance from some point p tends to infinity along every sequence q with q n ∉ K n.

This is the implication from assertion (e) to assertion (b) in do Carmo's Hopf–Rinow theorem. Neither monotonicity of K nor ⋃ n, K n = univ is needed.

theorem TauCeti.exists_isCompact_monotone_iUnion_eq_univ_tendsto_dist {α : Type u_1} [PseudoMetricSpace α] [ProperSpace α] (p : α) : ∃ (K : ℕ → Set α), (∀ (n : ℕ), IsCompact (K n)) ∧ Monotone K ∧ ⋃ (n : ℕ), K n = Set.univ ∧ ∀ (q : ℕ → α), (∀ (n : ℕ), q n ∉ K n) → Filter.Tendsto (fun (n : ℕ) => dist p (q n)) Filter.atTop Filter.atTop

In a proper pseudometric space, the closed balls closedBall p n form an increasing sequence of compact sets covering the space along which the distance from p diverges: if q n ∉ K n for every n, then dist p (q n) tends to infinity.

This is the implication from assertion (b) to assertion (e) in do Carmo's Hopf–Rinow theorem.

theorem TauCeti.properSpace_iff_exists_isCompact_monotone_iUnion_eq_univ_tendsto_dist {α : Type u_1} [PseudoMetricSpace α] (p : α) : ProperSpace α ↔ ∃ (K : ℕ → Set α), (∀ (n : ℕ), IsCompact (K n)) ∧ Monotone K ∧ ⋃ (n : ℕ), K n = Set.univ ∧ ∀ (q : ℕ → α), (∀ (n : ℕ), q n ∉ K n) → Filter.Tendsto (fun (n : ℕ) => dist p (q n)) Filter.atTop Filter.atTop

Properness via a compact exhaustion. A pseudometric space is proper if and only if, for a given point p, it is the union of an increasing sequence of compact sets K n such that the distance from p tends to infinity along every sequence q with q n ∉ K n.

This is the equivalence of assertions (b) and (e) in do Carmo's Hopf–Rinow theorem.

theorem IsOpen.exists_iUnion_isOpen_isCompact_closure {α : Type u_1} [PseudoMetricSpace α] [ProperSpace α] {U : Set α} (hU : IsOpen U) : ∃ (V : ℕ → Set α), (∀ (n : ℕ), IsOpen (V n)) ∧ (∀ (n : ℕ), IsCompact (closure (V n))) ∧ (∀ (n : ℕ), closure (V n) ⊆ U) ∧ Monotone V ∧ ⋃ (n : ℕ), V n = U

Exhaustion of an open set. In a proper pseudometric space, an open set U is the union of an increasing sequence of open sets V n whose closures are compact subsets of U.

theorem TopologicalSpace.Opens.exists_monotone_isCompact_closure_iUnion_eq {α : Type u_1} [PseudoMetricSpace α] [ProperSpace α] (Ω : Opens α) : ∃ (V : ℕ → Opens α), (∀ (n : ℕ), IsCompact (closure ↑(V n))) ∧ (∀ (n : ℕ), closure ↑(V n) ⊆ ↑Ω) ∧ Monotone V ∧ ⋃ (n : ℕ), ↑(V n) = ↑Ω ∧ ⋃ (n : ℕ), Subtype.val ⁻¹' ↑(V n) = Set.univ

Exhaustion of an open set by opens. In a proper pseudometric space, an open set Ω is the union of an increasing sequence of open sets V n whose closures are compact subsets of Ω; the traces of the V n on the subspace Ω cover it.

theorem TopologicalSpace.Opens.exists_isCompact_closure_subset_succ_iUnion_eq {α : Type u_1} [PseudoMetricSpace α] [ProperSpace α] (Ω : Opens α) : ∃ (V : ℕ → Opens α), (∀ (n : ℕ), IsCompact (closure ↑(V n))) ∧ (∀ (n : ℕ), closure ↑(V n) ⊆ ↑(V (n + 1))) ∧ ⋃ (n : ℕ), ↑(V n) = ↑Ω

Nested exhaustion of an open set. In a proper pseudometric space, an open set Ω is the union of a sequence of open sets V n with compact closures, the closure of each lying in the next. It is a subsequence of the exhaustion TopologicalSpace.Opens.exists_monotone_isCompact_closure_iUnion_eq.