dist is closed map

Stream: Is there code for X?

[Andrew Yang]

Do we have that dist x : E → ℝ is a closed map? Something like the following:

import Mathlib

variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]

lemma Metric.cthickening_sphere [Nontrivial E] {x : E} (r s : ℝ) (hr : 0 ≤ r) (hs : 0 ≤ s) :
    Metric.cthickening s (Metric.sphere x r) = dist x ⁻¹' Metric.closedBall r s := by
  ext a
  constructor
  · intro hb
    simp only [Set.mem_preimage, mem_closedBall]
    refine le_of_forall_gt fun c hc ↦ ?_
    have := lt_of_le_of_lt (mem_cthickening_iff.mp hb)
      ((ENNReal.ofReal_lt_ofReal_iff (hs.trans_lt hc)).mpr hc)
    obtain ⟨y, hy, hyc⟩ := EMetric.infEdist_lt_iff.mp this
    replace hyc : dist a y < c := by
      simpa [edist_dist, ENNReal.ofReal_lt_iff_lt_toReal, hs.trans hc.le] using hyc
    refine lt_of_le_of_lt ?_ hyc
    simpa [← show dist y x = r by simpa [SeminormedAddCommGroup.dist_eq] using hy, dist_comm x]
      using dist_dist_dist_le_left a y x
  · intro H
    obtain rfl | hax := eq_or_ne a x
    · replace H : |r| ≤ s := by simpa [SeminormedAddCommGroup.dist_eq] using H
      obtain ⟨b, hb⟩ := (NormedSpace.sphere_nonempty (x := a) (r := r)).mpr hr
      exact Metric.mem_cthickening_of_dist_le _ b _ _ hb (.trans
        (by simp_all [SeminormedAddCommGroup.dist_eq, norm_sub_rev, le_abs_self]) H)
    refine Metric.mem_cthickening_of_dist_le _ (x + (r / ‖a - x‖) • (a - x)) _ _ ?_ ?_
    · simpa [norm_smul, hax, sub_eq_zero]
    · trans ‖1 - r / ‖a - x‖‖ * ‖a - x‖
      · rw [← norm_smul, sub_smul, one_smul, sub_sub, SeminormedAddCommGroup.dist_eq]
      · rw [Real.norm_eq_abs, ← abs_norm, ← abs_mul, sub_mul]
        simpa [hax, SeminormedAddCommGroup.dist_eq, norm_sub_rev x, sub_eq_zero] using H

lemma isClosedMap_nndist [ProperSpace E] (x : E) : IsClosedMap (nndist x) := by
  cases subsingleton_or_nontrivial E
  · exact fun _ _ ↦ (Set.subsingleton_of_subsingleton.image _).isClosed
  intro s hs
  rw [← isOpen_compl_iff, Metric.isOpen_iff]
  simp only [Set.mem_compl_iff, Set.mem_image, not_exists, not_and]
  intro r hr
  simp only [gt_iff_lt, Set.subset_def, Metric.mem_ball, Set.mem_compl_iff, Set.mem_image,
    not_exists, not_and]
  obtain ⟨δ, hδ, h⟩ := Disjoint.exists_cthickenings (by
    simpa [Set.disjoint_iff_inter_eq_empty, Set.ext_iff, norm_sub_rev, ← NNReal.coe_inj,
      SeminormedAddCommGroup.dist_eq, imp_not_comm (a := _ = _)] using hr) (isCompact_sphere x r) hs
  refine ⟨δ, hδ, fun y hy l hls hd ↦ ?_⟩
  refine Set.subset_compl_iff_disjoint_left.mpr h (Metric.self_subset_cthickening _ hls) ?_
  rw [← NNReal.coe_inj, coe_nndist] at hd
  simpa [-Metric.mem_cthickening_iff, Metric.cthickening_sphere, hδ.le, hd] using hy.le

lemma isClosedMap_dist [ProperSpace E] (x : E) :
    IsClosedMap (dist x) :=
  (PseudoEMetricSpace.isometry_induced NNReal.toReal).isClosedEmbedding.isClosedMap.comp
    (isClosedMap_nndist x)

[Eric Wieser]

Maybe I should revive my PR that adds a typeclass to generalize NormedSpace.sphere_nonempty

[Anatole Dedecker]

I think the most efficient proof would be to use docs#isProperMap_iff_tendsto_cocompact, docs#tendsto_dist_left_cocompact_atTop, and docs#IsProperMap.isClosedMap

[Anatole Dedecker]

(Then this holds in any proper metric space)

[Anatole Dedecker]

One sensible thing to do would be to define "bornologically proper"/"cobounded" maps, which tend to cobounded along cobounded, and show that they coincide with proper maps in proper metric spaces.

[Anatole Dedecker]

Actually, the full statement for Mathlib should be: a metric space is proper iff dist x is proper for any x.

[Andrew Yang]

#32710

[Andrew Yang]

I also have these but I don't need them so I won't be PRing them unless mathlib actually wants them.

lemma image_nndist_ball {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [Nontrivial E] (x y : E) (r : ℝ) :
    nndist x '' Metric.ball y r = Metric.ball (nndist x y) r := by
  ext ⟨z, hz⟩
  simp only [Set.mem_image, Metric.mem_ball, ← NNReal.coe_inj, coe_nndist, NNReal.dist_eq,
    dist_comm x, NNReal.coe_mk]
  refine ⟨fun ⟨z, hz', hz''⟩ ↦ hz'' ▸ (abs_dist_sub_le z y x).trans_lt hz', fun H ↦ ?_⟩
  obtain rfl | hxy := eq_or_ne y x
  · obtain ⟨x, hx⟩ := (NormedSpace.sphere_nonempty (x := y)).mpr hz
    exact ⟨x, by simp_all [dist_eq_norm, abs_eq_self.mpr], by simpa⟩
  refine ⟨x + (z / ‖y - x‖) • (y - x), ?_, ?_⟩
  · refine lt_of_le_of_lt ?_ H
    trans ‖1 - (z / ‖y - x‖)‖ * ‖y - x‖
    · rw [← norm_smul, dist_eq_norm', ← sub_sub, sub_smul, one_smul]
    · rw [Real.norm_eq_abs, ← abs_norm, ← abs_mul, sub_mul]
      simp [sub_eq_zero, hxy, dist_eq_norm, abs_sub_comm]
  · simp [norm_smul, sub_eq_zero, hxy, hz]

open Metric in
lemma NormedSpace.isOpenQuotientMap_nndist {E : Type*} [NormedAddCommGroup E]
    [NormedSpace ℝ E] [Nontrivial E] (x : E) :
    IsOpenQuotientMap (nndist x) where
  surjective r :=
    have ⟨y, hy⟩ := (NormedSpace.sphere_nonempty (x := x)).mpr r.2
    ⟨y, by simpa [NormedAddCommGroup.dist_eq, ← NNReal.coe_inj, norm_sub_rev] using hy⟩
  continuous := by fun_prop
  isOpenMap := isOpenMap_iff_nhds_le.mpr fun r ↦ (nhds_basis_ball.map (nndist x)).ge_iff.mpr
    fun ε _ ↦ (image_nndist_ball x r ε ▸ Metric.isOpen_ball).mem_nhds (by simpa [image_nndist_ball])