Mathlib.Topology.MetricSpace.ProperSpace

ProperSpace structure

(α : Type u) [PseudoMetricSpace α]

Full source

/-- A pseudometric space is proper if all closed balls are compact. -/
class ProperSpace (α : Type u) [PseudoMetricSpace α] : Prop where
  isCompact_closedBall : ∀ x : α, ∀ r, IsCompact (closedBall x r)

Proper pseudometric space

Informal description

A pseudometric space $\alpha$ is called a proper space if every closed ball in $\alpha$ is compact. This means for any point $x \in \alpha$ and any radius $r \geq 0$, the set $\{ y \in \alpha \mid \text{dist}(x, y) \leq r \}$ is compact.

isCompact_sphere theorem

{α : Type*} [PseudoMetricSpace α] [ProperSpace α] (x : α) (r : ℝ) : IsCompact (sphere x r)

Full source

/-- In a proper pseudometric space, all spheres are compact. -/
theorem isCompact_sphere {α : Type*} [PseudoMetricSpace α] [ProperSpace α] (x : α) (r : ℝ) :
    IsCompact (sphere x r) :=
  (isCompact_closedBall x r).of_isClosed_subset isClosed_sphere sphere_subset_closedBall

Compactness of Spheres in Proper Pseudometric Spaces

Informal description

Let $\alpha$ be a proper pseudometric space. For any point $x \in \alpha$ and any radius $r \geq 0$, the sphere $\{ y \in \alpha \mid \text{dist}(x, y) = r \}$ is compact.

Metric.sphere.compactSpace instance

{α : Type*} [PseudoMetricSpace α] [ProperSpace α] (x : α) (r : ℝ) : CompactSpace (sphere x r)

Full source

/-- In a proper pseudometric space, any sphere is a `CompactSpace` when considered as a subtype. -/
instance Metric.sphere.compactSpace {α : Type*} [PseudoMetricSpace α] [ProperSpace α]
    (x : α) (r : ℝ) : CompactSpace (sphere x r) :=
  isCompact_iff_compactSpace.mp (isCompact_sphere _ _)

Compactness of Spheres in Proper Pseudometric Spaces

Informal description

For any proper pseudometric space $\alpha$, point $x \in \alpha$, and radius $r \geq 0$, the sphere $\{ y \in \alpha \mid \text{dist}(x, y) = r \}$ is a compact space when equipped with the subspace topology.

secondCountable_of_proper instance

[ProperSpace α] : SecondCountableTopology α

Full source

/-- A proper pseudo metric space is sigma compact, and therefore second countable. -/
instance (priority := 100) secondCountable_of_proper [ProperSpace α] :
    SecondCountableTopology α := by
  -- We already have `sigmaCompactSpace_of_locallyCompact_secondCountable`, so we don't
  -- add an instance for `SigmaCompactSpace`.
  suffices SigmaCompactSpace α from EMetric.secondCountable_of_sigmaCompact α
  rcases em (Nonempty α) with (⟨⟨x⟩⟩ | hn)
  · exact ⟨⟨fun n => closedBall x n, fun n => isCompact_closedBall _ _, iUnion_closedBall_nat _⟩⟩
  · exact ⟨⟨fun _ => ∅, fun _ => isCompact_empty, iUnion_eq_univ_iff.2 fun x => (hn ⟨x⟩).elim⟩⟩

Proper Spaces are Second-Countable

Informal description

Every proper pseudometric space $\alpha$ is second-countable. That is, the topology on $\alpha$ has a countable basis.

ProperSpace.of_isCompact_closedBall_of_le theorem

(R : ℝ) (h : ∀ x : α, ∀ r, R ≤ r → IsCompact (closedBall x r)) : ProperSpace α

Full source

/-- If all closed balls of large enough radius are compact, then the space is proper. Especially
useful when the lower bound for the radius is 0. -/
theorem ProperSpace.of_isCompact_closedBall_of_le (R : ℝ)
    (h : ∀ x : α, ∀ r, R ≤ r → IsCompact (closedBall x r)) : ProperSpace α :=
  ⟨fun x r => IsCompact.of_isClosed_subset (h x (max r R) (le_max_right _ _)) isClosed_closedBall
    (closedBall_subset_closedBall <| le_max_left _ _)⟩

Properness Criterion via Compactness of Large Closed Balls

Informal description

Let $\alpha$ be a pseudometric space and $R$ a real number. If for every point $x \in \alpha$ and every radius $r \geq R$, the closed ball $\overline{B}(x, r) = \{ y \in \alpha \mid \text{dist}(x, y) \leq r \}$ is compact, then $\alpha$ is a proper space.

ProperSpace.of_seq_closedBall theorem

 {β : Type*} {l : Filter β} [NeBot l] {x : α} {r : β → ℝ} (hr : Tendsto r l atTop)
  (hc : ∀ᶠ i in l, IsCompact (closedBall x (r i))) : ProperSpace α

Full source

/-- If there exists a sequence of compact closed balls with the same center
such that the radii tend to infinity, then the space is proper. -/
theorem ProperSpace.of_seq_closedBall {β : Type*} {l : Filter β} [NeBot l] {x : α} {r : β → ℝ}
    (hr : Tendsto r l atTop) (hc : ∀ᶠ i in l, IsCompact (closedBall x (r i))) :
    ProperSpace α where
  isCompact_closedBall a r :=
    let ⟨_i, hci, hir⟩ := (hc.and <| hr.eventually_ge_atTop <| r + dist a x).exists
    hci.of_isClosed_subset isClosed_closedBall <| closedBall_subset_closedBall' hir

Properness Criterion via Compact Closed Balls with Diverging Radii

Informal description

Let $\alpha$ be a pseudometric space, $\beta$ a type, and $l$ a nontrivial filter on $\beta$. Suppose there exists a point $x \in \alpha$ and a function $r : \beta \to \mathbb{R}$ such that: 1. The radii $r(i)$ tend to infinity as $i$ varies along $l$ (i.e., $\lim_{l} r = \infty$). 2. For sufficiently large $i$ (i.e., eventually along $l$), the closed ball $\overline{B}(x, r(i))$ is compact. Then $\alpha$ is a proper space.

proper_of_compact instance

[CompactSpace α] : ProperSpace α

Full source

instance (priority := 100) proper_of_compact [CompactSpace α] : ProperSpace α :=
  ⟨fun _ _ => isClosed_closedBall.isCompact⟩

Compact Spaces are Proper

Informal description

Every compact pseudometric space is a proper space. That is, in a compact pseudometric space $\alpha$, all closed balls are compact.

locallyCompact_of_proper instance

[ProperSpace α] : LocallyCompactSpace α

Full source

/-- A proper space is locally compact -/
instance (priority := 100) locallyCompact_of_proper [ProperSpace α] : LocallyCompactSpace α :=
  .of_hasBasis (fun _ => nhds_basis_closedBall) fun _ _ _ =>
    isCompact_closedBall _ _

Proper Spaces are Locally Compact

Informal description

Every proper pseudometric space $\alpha$ is locally compact. That is, every point in $\alpha$ has a neighborhood basis consisting of compact sets.

complete_of_proper instance

[ProperSpace α] : CompleteSpace α

Full source

/-- A proper space is complete -/
instance (priority := 100) complete_of_proper [ProperSpace α] : CompleteSpace α :=
  ⟨fun {f} hf => by
    /- We want to show that the Cauchy filter `f` is converging. It suffices to find a closed
      ball (therefore compact by properness) where it is nontrivial. -/
    obtain ⟨t, t_fset, ht⟩ : ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, dist x y < 1 :=
      (Metric.cauchy_iff.1 hf).2 1 zero_lt_one
    rcases hf.1.nonempty_of_mem t_fset with ⟨x, xt⟩
    have : closedBall x 1 ∈ f := mem_of_superset t_fset fun y yt => (ht y yt x xt).le
    rcases (isCompact_iff_totallyBounded_isComplete.1 (isCompact_closedBall x 1)).2 f hf
        (le_principal_iff.2 this) with
      ⟨y, -, hy⟩
    exact ⟨y, hy⟩⟩

Proper Spaces are Complete

Informal description

Every proper pseudometric space $\alpha$ is complete. That is, every Cauchy sequence in $\alpha$ converges to a point in $\alpha$.

prod_properSpace instance

 {α : Type*} {β : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] [ProperSpace α] [ProperSpace β] :
  ProperSpace (α × β)

Full source

/-- A binary product of proper spaces is proper. -/
instance prod_properSpace {α : Type*} {β : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β]
    [ProperSpace α] [ProperSpace β] : ProperSpace (α × β) where
  isCompact_closedBall := by
    rintro ⟨x, y⟩ r
    rw [← closedBall_prod_same x y]
    exact (isCompact_closedBall x r).prod (isCompact_closedBall y r)

Product of Proper Spaces is Proper

Informal description

For any two proper pseudometric spaces $\alpha$ and $\beta$, their product $\alpha \times \beta$ equipped with the supremum distance is also a proper space.

pi_properSpace instance

 {π : β → Type*} [Fintype β] [∀ b, PseudoMetricSpace (π b)] [h : ∀ b, ProperSpace (π b)] : ProperSpace (∀ b, π b)

Full source

/-- A finite product of proper spaces is proper. -/
instance pi_properSpace {π : β → Type*} [Fintype β] [∀ b, PseudoMetricSpace (π b)]
    [h : ∀ b, ProperSpace (π b)] : ProperSpace (∀ b, π b) := by
  refine .of_isCompact_closedBall_of_le 0 fun x r hr => ?_
  rw [closedBall_pi _ hr]
  exact isCompact_univ_pi fun _ => isCompact_closedBall _ _

Finite Product of Proper Spaces is Proper

Informal description

For any finite family of proper pseudometric spaces $\{\pi_b\}_{b \in \beta}$, the product space $\prod_{b \in \beta} \pi_b$ equipped with the supremum distance is also a proper space.

ProperSpace.of_isClosed theorem

{X : Type*} [PseudoMetricSpace X] [ProperSpace X] {s : Set X} (hs : IsClosed s) : ProperSpace s

Full source

/-- A closed subspace of a proper space is proper.
This is true for any proper lipschitz map. See `LipschitzWith.properSpace`. -/
lemma ProperSpace.of_isClosed {X : Type*} [PseudoMetricSpace X] [ProperSpace X]
    {s : Set X} (hs : IsClosed s) :
    ProperSpace s :=
  ⟨fun x r ↦ Topology.IsEmbedding.subtypeVal.isCompact_iff.mpr
    ((isCompact_closedBall x.1 r).of_isClosed_subset
    (hs.isClosedMap_subtype_val _ isClosed_closedBall) (Set.image_subset_iff.mpr subset_rfl))⟩

Closed Subset of a Proper Space is Proper

Informal description

Let $X$ be a proper pseudometric space and $s \subseteq X$ a closed subset. Then $s$ equipped with the induced pseudometric is also a proper space.

instProperSpaceAdditive instance

[PseudoMetricSpace X] [ProperSpace X] : ProperSpace (Additive X)

Full source

instance [PseudoMetricSpace X] [ProperSpace X] : ProperSpace (Additive X) := ‹ProperSpace X›

Proper Space Structure on Additive Groups

Informal description

For any proper pseudometric space $X$, the additive version $\text{Additive}\,X$ is also a proper pseudometric space.

instProperSpaceMultiplicative instance

[PseudoMetricSpace X] [ProperSpace X] : ProperSpace (Multiplicative X)

Full source

instance [PseudoMetricSpace X] [ProperSpace X] : ProperSpace (Multiplicative X) := ‹ProperSpace X›

Proper Space Structure on Multiplicative Groups

Informal description

For any proper pseudometric space $X$, the multiplicative group structure on $X$ is also a proper pseudometric space.

instProperSpaceOrderDual instance

[PseudoMetricSpace X] [ProperSpace X] : ProperSpace Xᵒᵈ

Full source

instance [PseudoMetricSpace X] [ProperSpace X] : ProperSpace Xᵒᵈ := ‹ProperSpace X›

Proper Space Structure on Order Duals

Informal description

For any proper pseudometric space $X$, the order dual $X^{\text{op}}$ is also a proper pseudometric space.

Main definitions and results