refactor(Topology): cleaner way to get metric spaces from emetric spaces (#29321)

FormulaRabbit81 · FormulaRabbit81 · commit 8387c032b3ce · 2025-11-02T21:27:22.000Z
Change EMetricSpace.toMetricSpaceOfDist in Mathlib/Topology/MetricSpace/Basic and PseudoEMetricSpace.toPseudoMetricSpaceOfDist in Mathlib/Topology/MetricSpace/Pseudo/Defs to require nonnegativity of given distance function rather than finiteness of old edistance.
diff --git a/Mathlib/Analysis/Normed/Lp/PiLp.lean b/Mathlib/Analysis/Normed/Lp/PiLp.lean
@@ -60,7 +60,6 @@ are equivalent on `ℝ^n` for abstract (norm equivalence) reasons. Instead, we g
 We also set up the theory for `PseudoEMetricSpace` and `PseudoMetricSpace`.
 -/
 
-
 open Module Real Set Filter RCLike Bornology Uniformity Topology NNReal ENNReal WithLp
 
 noncomputable section
@@ -334,31 +333,25 @@ abbrev pseudoMetricAux : PseudoMetricSpace (PiLp p α) :=
   PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist
     (fun f g => by
       rcases p.dichotomy with (rfl | h)
-      · exact iSup_edist_ne_top_aux f g
-      · rw [edist_eq_sum (zero_lt_one.trans_le h)]
-        exact ENNReal.rpow_ne_top_of_nonneg (by positivity) <| ENNReal.sum_ne_top.2 fun _ _ ↦
-          by finiteness)
+      · simp only [dist, top_ne_zero, ↓reduceIte]
+        exact Real.iSup_nonneg fun i ↦ dist_nonneg
+      · simp only [dist]
+        split_ifs with hp
+        · linarith
+        · exact Real.iSup_nonneg fun i ↦ dist_nonneg
+        · exact rpow_nonneg (Fintype.sum_nonneg fun i ↦ by positivity) (1 / p.toReal))
     fun f g => by
     rcases p.dichotomy with (rfl | h)
     · rw [edist_eq_iSup, dist_eq_iSup]
       cases isEmpty_or_nonempty ι
-      · simp only [Real.iSup_of_isEmpty, ciSup_of_empty, ENNReal.bot_eq_zero, ENNReal.toReal_zero]
-      · refine le_antisymm (ciSup_le fun i => ?_) ?_
-        · rw [← ENNReal.ofReal_le_iff_le_toReal (iSup_edist_ne_top_aux f g), ←
-            PseudoMetricSpace.edist_dist]
-          -- Porting note: `le_iSup` needed some help
-          exact le_iSup (fun k => edist (f k) (g k)) i
-        · refine ENNReal.toReal_le_of_le_ofReal (Real.sSup_nonneg ?_) (iSup_le fun i => ?_)
-          · rintro - ⟨i, rfl⟩
-            exact dist_nonneg
-          · change PseudoMetricSpace.edist _ _ ≤ _
-            rw [PseudoMetricSpace.edist_dist]
-            -- Porting note: `le_ciSup` needed some help
-            exact ENNReal.ofReal_le_ofReal
-              (le_ciSup (Finite.bddAbove_range (fun k => dist (f k) (g k))) i)
-    · have A (i) : edist (f i) (g i) ^ p.toReal ≠ ⊤ := by finiteness
-      simp only [edist_eq_sum (zero_lt_one.trans_le h), dist_edist, ENNReal.toReal_rpow,
-        dist_eq_sum (zero_lt_one.trans_le h), ← ENNReal.toReal_sum fun i _ => A i]
+      · simp
+      · refine ENNReal.eq_of_forall_le_nnreal_iff fun r ↦ ?_
+        have : BddAbove <| .range fun i ↦ dist (f i) (g i) := Finite.bddAbove_range _
+        simp [ciSup_le_iff this]
+    · have : 0 < p.toReal := by rw [ENNReal.toReal_pos_iff_ne_top]; rintro rfl; norm_num at h
+      simp only [edist_eq_sum, edist_dist, dist_eq_sum, this]
+      rw [← ENNReal.ofReal_rpow_of_nonneg (by simp [Finset.sum_nonneg, Real.rpow_nonneg]) (by simp)]
+      simp [Real.rpow_nonneg, ENNReal.ofReal_sum_of_nonneg, ← ENNReal.ofReal_rpow_of_nonneg]
 
 attribute [local instance] PiLp.pseudoMetricAux
 
diff --git a/Mathlib/Analysis/Normed/Lp/ProdLp.lean b/Mathlib/Analysis/Normed/Lp/ProdLp.lean
@@ -342,26 +342,17 @@ abbrev prodPseudoMetricAux [PseudoMetricSpace α] [PseudoMetricSpace β] :
   PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist
     (fun f g => by
       rcases p.dichotomy with (rfl | h)
-      · exact prod_sup_edist_ne_top_aux f g
-      · rw [prod_edist_eq_add (zero_lt_one.trans_le h)]
-        finiteness)
+      · simp [prod_dist_eq_sup]
+      · simp only [dist, one_div, dite_eq_ite]
+        split_ifs with hp' <;> positivity)
     fun f g => by
     rcases p.dichotomy with (rfl | h)
-    · rw [prod_edist_eq_sup, prod_dist_eq_sup]
-      refine le_antisymm (sup_le ?_ ?_) ?_
-      · rw [← ENNReal.ofReal_le_iff_le_toReal (prod_sup_edist_ne_top_aux f g),
-          ← PseudoMetricSpace.edist_dist]
-        exact le_sup_left
-      · rw [← ENNReal.ofReal_le_iff_le_toReal (prod_sup_edist_ne_top_aux f g),
-          ← PseudoMetricSpace.edist_dist]
-        exact le_sup_right
-      · refine ENNReal.toReal_le_of_le_ofReal ?_ ?_
-        · simp only [le_sup_iff, dist_nonneg, or_self]
-        · simp [-ofReal_max]
-    · have h1 : edist f.fst g.fst ^ p.toReal ≠ ⊤ := by finiteness
-      have h2 : edist f.snd g.snd ^ p.toReal ≠ ⊤ := by finiteness
-      simp only [prod_edist_eq_add (zero_lt_one.trans_le h), dist_edist, ENNReal.toReal_rpow,
-        prod_dist_eq_add (zero_lt_one.trans_le h), ← ENNReal.toReal_add h1 h2]
+    · refine ENNReal.eq_of_forall_le_nnreal_iff fun r ↦ ?_
+      simp [prod_edist_eq_sup, prod_dist_eq_sup]
+    · have : 0 < p.toReal := by rw [ENNReal.toReal_pos_iff_ne_top]; rintro rfl; norm_num at h
+      simp only [prod_edist_eq_add, edist_dist, one_div, prod_dist_eq_add, this]
+      rw [← ENNReal.ofReal_rpow_of_nonneg, ENNReal.ofReal_add, ← ENNReal.ofReal_rpow_of_nonneg,
+        ← ENNReal.ofReal_rpow_of_nonneg] <;> simp [Real.rpow_nonneg, add_nonneg]
 
 attribute [local instance] WithLp.prodPseudoMetricAux
 
diff --git a/Mathlib/Data/ENNReal/Real.lean b/Mathlib/Data/ENNReal/Real.lean
@@ -147,6 +147,10 @@ theorem ofReal_le_ofReal_iff {p q : ℝ} (h : 0 ≤ q) :
 lemma ofReal_le_ofReal_iff' {p q : ℝ} : ENNReal.ofReal p ≤ .ofReal q ↔ p ≤ q ∨ p ≤ 0 :=
   coe_le_coe.trans Real.toNNReal_le_toNNReal_iff'
 
+@[simp, norm_cast]
+lemma ofReal_le_coe {a : ℝ} {b : ℝ≥0} : ENNReal.ofReal a ≤ b ↔ a ≤ b := by
+  simp [← ofReal_le_ofReal_iff]
+
 lemma ofReal_lt_ofReal_iff' {p q : ℝ} : ENNReal.ofReal p < .ofReal q ↔ p < q ∧ 0 < q :=
   coe_lt_coe.trans Real.toNNReal_lt_toNNReal_iff'
 
diff --git a/Mathlib/Topology/MetricSpace/Basic.lean b/Mathlib/Topology/MetricSpace/Basic.lean
@@ -73,17 +73,17 @@ uniformity are defeq in the metric space and the emetric space. In this definiti
 is given separately, to be able to prescribe some expression which is not defeq to the push-forward
 of the edistance to reals. -/
 abbrev EMetricSpace.toMetricSpaceOfDist {α : Type u} [EMetricSpace α] (dist : α → α → ℝ)
-    (edist_ne_top : ∀ x y : α, edist x y ≠ ⊤) (h : ∀ x y, dist x y = ENNReal.toReal (edist x y)) :
+    (dist_nonneg : ∀ x y, 0 ≤ dist x y) (h : ∀ x y, edist x y = .ofReal (dist x y)) :
     MetricSpace α :=
-  @MetricSpace.ofT0PseudoMetricSpace _
-    (PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist edist_ne_top h) _
+  letI := PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist dist_nonneg h
+  MetricSpace.ofT0PseudoMetricSpace _
 
 /-- One gets a metric space from an emetric space if the edistance
 is everywhere finite, by pushing the edistance to reals. We set it up so that the edist and the
 uniformity are defeq in the metric space and the emetric space. -/
-def EMetricSpace.toMetricSpace {α : Type u} [EMetricSpace α] (h : ∀ x y : α, edist x y ≠ ⊤) :
+abbrev EMetricSpace.toMetricSpace {α : Type u} [EMetricSpace α] (h : ∀ x y : α, edist x y ≠ ⊤) :
     MetricSpace α :=
-  EMetricSpace.toMetricSpaceOfDist (fun x y => ENNReal.toReal (edist x y)) h fun _ _ => rfl
+  EMetricSpace.toMetricSpaceOfDist (ENNReal.toReal <| edist · ·) (by simp) (by simp [h])
 
 /-- Metric space structure pulled back by an injective function. Injectivity is necessary to
 ensure that `dist x y = 0` only if `x = y`. -/
@@ -186,8 +186,8 @@ theorem SeparationQuotient.dist_mk {α : Type u} [PseudoMetricSpace α] (p q : 
 
 instance SeparationQuotient.instMetricSpace {α : Type u} [PseudoMetricSpace α] :
     MetricSpace (SeparationQuotient α) :=
-  EMetricSpace.toMetricSpaceOfDist dist (surjective_mk.forall₂.2 edist_ne_top) <|
-    surjective_mk.forall₂.2 dist_edist
+  EMetricSpace.toMetricSpaceOfDist dist (surjective_mk.forall₂.2 fun _ _ ↦ dist_nonneg) <|
+    surjective_mk.forall₂.2 edist_dist
 
 end EqRel
 
diff --git a/Mathlib/Topology/MetricSpace/Pseudo/Constructions.lean b/Mathlib/Topology/MetricSpace/Pseudo/Constructions.lean
@@ -143,9 +143,8 @@ variable [PseudoMetricSpace β]
 instance Prod.pseudoMetricSpaceMax : PseudoMetricSpace (α × β) :=
   let i := PseudoEMetricSpace.toPseudoMetricSpaceOfDist
     (fun x y : α × β => dist x.1 y.1 ⊔ dist x.2 y.2)
-    (fun _ _ => (max_lt (edist_lt_top _ _) (edist_lt_top _ _)).ne) fun x y => by
-      simp only [dist_edist, ← ENNReal.toReal_max (edist_ne_top _ _) (edist_ne_top _ _),
-        Prod.edist_eq]
+    (fun x y ↦ by positivity) fun x y => by
+      simp only [ENNReal.ofReal_max, Prod.edist_eq, edist_dist]
   i.replaceBornology fun s => by
     simp only [← isBounded_image_fst_and_snd, isBounded_iff_eventually, forall_mem_image, ←
       eventually_and, ← forall_and, ← max_le_iff]
diff --git a/Mathlib/Topology/MetricSpace/Pseudo/Defs.lean b/Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
@@ -994,29 +994,27 @@ is everywhere finite, by pushing the edistance to reals. We set it up so that th
 uniformity are defeq in the pseudometric space and the pseudoemetric space. In this definition, the
 distance is given separately, to be able to prescribe some expression which is not defeq to the
 push-forward of the edistance to reals. See note [reducible non-instances]. -/
-abbrev PseudoEMetricSpace.toPseudoMetricSpaceOfDist {α : Type u} [e : PseudoEMetricSpace α]
-    (dist : α → α → ℝ) (edist_ne_top : ∀ x y : α, edist x y ≠ ⊤)
-    (h : ∀ x y, dist x y = ENNReal.toReal (edist x y)) : PseudoMetricSpace α where
+abbrev PseudoEMetricSpace.toPseudoMetricSpaceOfDist {X : Type*} [e : PseudoEMetricSpace X]
+    (dist : X → X → ℝ) (dist_nonneg : ∀ x y, 0 ≤ dist x y)
+    (h : ∀ x y, edist x y = .ofReal (dist x y)) : PseudoMetricSpace X where
   dist := dist
-  dist_self x := by simp [h]
-  dist_comm x y := by simp [h, edist_comm]
+  dist_self x := by simpa [h, (dist_nonneg _ _).ge_iff_eq', -edist_self] using edist_self x
+  dist_comm x y := by simpa [h, dist_nonneg] using edist_comm x y
   dist_triangle x y z := by
-    simp only [h]
-    exact ENNReal.toReal_le_add (edist_triangle _ _ _) (edist_ne_top _ _) (edist_ne_top _ _)
+    simpa [h, dist_nonneg, add_nonneg, ← ENNReal.ofReal_add] using edist_triangle x y z
   edist := edist
-  edist_dist _ _ := by simp only [h, ENNReal.ofReal_toReal (edist_ne_top _ _)]
-  toUniformSpace := e.toUniformSpace
+  edist_dist _ _ := by simp only [h]
+  toUniformSpace := PseudoEMetricSpace.toUniformSpace
   uniformity_dist := e.uniformity_edist.trans <| by
-    simpa only [ENNReal.coe_toNNReal (edist_ne_top _ _), h]
-      using (Metric.uniformity_edist_aux fun x y : α => (edist x y).toNNReal).symm
+    simpa [h, dist_nonneg, ENNReal.coe_toNNReal_eq_toReal]
+      using (Metric.uniformity_edist_aux fun x y : X => (edist x y).toNNReal).symm
 
 /-- One gets a pseudometric space from an emetric space if the edistance
 is everywhere finite, by pushing the edistance to reals. We set it up so that the edist and the
 uniformity are defeq in the pseudometric space and the emetric space. -/
 abbrev PseudoEMetricSpace.toPseudoMetricSpace {α : Type u} [PseudoEMetricSpace α]
     (h : ∀ x y : α, edist x y ≠ ⊤) : PseudoMetricSpace α :=
-  PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun x y => ENNReal.toReal (edist x y)) h fun _ _ =>
-    rfl
+  PseudoEMetricSpace.toPseudoMetricSpaceOfDist (ENNReal.toReal <| edist · ·) (by simp) (by simp [h])
 
 /-- Build a new pseudometric space from an old one where the bundled bornology structure is provably
 (but typically non-definitionaly) equal to some given bornology structure.
diff --git a/Mathlib/Topology/MetricSpace/Pseudo/Pi.lean b/Mathlib/Topology/MetricSpace/Pseudo/Pi.lean
@@ -30,9 +30,8 @@ instance pseudoMetricSpacePi : PseudoMetricSpace (∀ b, X b) := by
     formula for the distance -/
   let i := PseudoEMetricSpace.toPseudoMetricSpaceOfDist
     (fun f g : ∀ b, X b => ((sup univ fun b => nndist (f b) (g b) : ℝ≥0) : ℝ))
-    (fun f g => ((Finset.sup_lt_iff bot_lt_top).2 fun b _ => edist_lt_top _ _).ne)
-    (fun f g => by
-      simp only [edist_pi_def, edist_nndist, ← ENNReal.coe_finset_sup, ENNReal.coe_toReal])
+    (fun f g => NNReal.zero_le_coe)
+    (fun f g => by simp [edist_pi_def])
   refine i.replaceBornology fun s => ?_
   simp only [isBounded_iff_eventually, ← forall_isBounded_image_eval_iff,
     forall_mem_image, ← Filter.eventually_all, @dist_nndist (X _)]
diff --git a/Mathlib/Topology/MetricSpace/UniformConvergence.lean b/Mathlib/Topology/MetricSpace/UniformConvergence.lean
@@ -130,11 +130,16 @@ variable [PseudoMetricSpace β]
 noncomputable instance [BoundedSpace β] : PseudoMetricSpace (α →ᵤ β) :=
   PseudoEMetricSpace.toPseudoMetricSpaceOfDist
     (fun f g ↦ ⨆ x, dist (toFun f x) (toFun g x))
-    (fun _ _ ↦ by
-      have := BoundedSpace.bounded_univ (α := β) |>.ediam_ne_top.lt_top
-      refine (iSup_le fun x ↦ EMetric.edist_le_diam_of_mem ?_ ?_).trans_lt this |>.ne
-      all_goals trivial)
-    (fun _ _ ↦ by simp [edist_def, ENNReal.toReal_iSup (fun _ ↦ edist_ne_top _ _), dist_edist])
+    (fun _ _ ↦ Real.iSup_nonneg fun i ↦ dist_nonneg)
+    fun f g ↦ by
+      cases isEmpty_or_nonempty α
+      · simp [edist_def]
+      have : BddAbove <| .range fun x ↦ dist (toFun f x) (toFun g x) := by
+        use (EMetric.diam (.univ : Set β)).toReal
+        simp +contextual [mem_upperBounds, eq_comm (a := dist _ _), ← edist_dist,
+          ← ENNReal.ofReal_le_iff_le_toReal BoundedSpace.bounded_univ.ediam_ne_top,
+          EMetric.edist_le_diam_of_mem]
+      exact ENNReal.eq_of_forall_le_nnreal_iff fun r ↦ by simp [edist_def, ciSup_le_iff this]
 
 lemma dist_def [BoundedSpace β] (f g : α →ᵤ β) :
     dist f g = ⨆ x, dist (toFun f x) (toFun g x) :=
@@ -279,17 +284,18 @@ variable [Finite 𝔖] [PseudoMetricSpace β]
 
 noncomputable instance [BoundedSpace β] : PseudoMetricSpace (α →ᵤ[𝔖] β) :=
   PseudoEMetricSpace.toPseudoMetricSpaceOfDist
-    (fun f g ↦ ⨆ x ∈ ⋃₀ 𝔖, dist (toFun 𝔖 f x) (toFun 𝔖 g x))
-    (fun _ _ ↦ by
-      have := BoundedSpace.bounded_univ (α := β) |>.ediam_ne_top.lt_top
-      exact (iSup₂_le fun x _ ↦ EMetric.edist_le_diam_of_mem (Set.mem_univ _) (Set.mem_univ _))
-        |>.trans_lt this |>.ne)
-    (fun _ _ ↦ by
-      simp only [dist_edist, edist_def, ← ENNReal.toReal_iSup (fun _ ↦ edist_ne_top _ _)]
-      rw [ENNReal.toReal_iSup]
-      have := BoundedSpace.bounded_univ (α := β) |>.ediam_ne_top.lt_top
-      refine fun x ↦ lt_of_le_of_lt (iSup_le fun hx ↦ ?_) this |>.ne
-      exact EMetric.edist_le_diam_of_mem (Set.mem_univ _) (Set.mem_univ _))
+    (fun f g ↦ ⨆ x : ⋃₀ 𝔖, dist (toFun 𝔖 f x) (toFun 𝔖 g x))
+    (fun _ _ ↦ Real.iSup_nonneg fun i ↦ dist_nonneg)
+    fun f g ↦ by
+      cases isEmpty_or_nonempty (⋃₀ 𝔖)
+      · simp_all [edist_def]
+      have : BddAbove (.range fun x : ⋃₀ 𝔖 ↦ dist (toFun 𝔖 f x) (toFun 𝔖 g x)) := by
+        use (EMetric.diam (.univ : Set β)).toReal
+        simp +contextual [mem_upperBounds, eq_comm (a := dist _ _), ← edist_dist,
+          ← ENNReal.ofReal_le_iff_le_toReal BoundedSpace.bounded_univ.ediam_ne_top,
+          EMetric.edist_le_diam_of_mem]
+      refine ENNReal.eq_of_forall_le_nnreal_iff fun r ↦ ?_
+      simp [edist_def, ciSup_le_iff this]
 
 noncomputable instance [BoundedSpace β] : BoundedSpace (α →ᵤ[𝔖] β) where
   bounded_univ := by
