feat(Topology/MetricSpace): the L^p direct sum of metric spaces (#40212)

Endow the direct sum `ι →₀ X` of `ι`-many copies of a metric space `X` with the L^p metric for any `1 ≤ p < ∞`.

`p = ∞` is theoretically possible too but currently annoying due to defects in our tactics/`WithTop` API. I am leaving it as future work.

[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/What.20topology.20on.20Finsupp.3F/with/600119738)

Author: YaelDillies

Mathlib.lean

@@ -2180,6 +2180,7 @@ public import Mathlib.Analysis.Normed.Group.Tannery
 public import Mathlib.Analysis.Normed.Group.Ultra
 public import Mathlib.Analysis.Normed.Group.Uniform
 public import Mathlib.Analysis.Normed.Group.ZeroAtInfty
+public import Mathlib.Analysis.Normed.Lp.Finsupp
 public import Mathlib.Analysis.Normed.Lp.LpEquiv
 public import Mathlib.Analysis.Normed.Lp.Matrix
 public import Mathlib.Analysis.Normed.Lp.MeasurableSpace

Mathlib/Algebra/MvPolynomial/SchwartzZippel.lean

@@ -197,7 +197,6 @@ lemma schwartz_zippel_totalDegree {n} {p : MvPolynomial (Fin n) R} (hp : p ≠ 0
     _ = p.totalDegree / #S := by
       obtain rfl | hs := S.eq_empty_or_nonempty
       · simp
-        simp only [← _root_.bot_eq_zero, sup_bot]
       simp_rw [totalDegree, Nat.cast_finsetSup]
       rw [sup_div₀ (by positivity)]
       simp [← sum_div, Finsupp.sum_fintype]

Mathlib/Algebra/Order/Monoid/Canonical/Basic.lean

@@ -15,15 +15,6 @@ public import Mathlib.Algebra.Order.Sub.Unbundled.Basic
 
 public section
 
-namespace Finset
-variable {ι α : Type*} [AddCommMonoid α] [LinearOrder α] [OrderBot α] [CanonicallyOrderedAdd α]
-  {s : Finset ι} {f : ι → α}
-
-@[simp] lemma sup_eq_zero : s.sup f = 0 ↔ ∀ i ∈ s, f i = 0 := by simp [← bot_eq_zero']
-@[simp] lemma sup'_eq_zero (hs) : s.sup' hs f = 0 ↔ ∀ i ∈ s, f i = 0 := by simp [sup'_eq_sup]
-
-end Finset
-
 namespace Set
 variable {α : Type*} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α]
   [Sub α] [OrderedSub α] {β : Type*} {f : α → β} {k : α}

Mathlib/Analysis/InnerProductSpace/PiL2.lean

@@ -1321,7 +1321,7 @@ open Matrix LinearMap EuclideanSpace in
 theorem InnerProductSpace.symm_toEuclideanLin_rankOne {𝕜 m n : Type*} [RCLike 𝕜] [Fintype m]
     [Fintype n] [DecidableEq n] (x : EuclideanSpace 𝕜 m) (y : EuclideanSpace 𝕜 n) :
     toEuclideanLin.symm (rankOne 𝕜 x y) = .vecMulVec x (star y) := by
-  simp [toLpLin, toMatrix', ← ext_iff, vecMulVec_apply, inner_single_right, mul_comm]
+  simp [toLpLin, toMatrix', ← Matrix.ext_iff, vecMulVec_apply, inner_single_right, mul_comm]
 
 namespace FiniteDimensional
 variable [Unique ι] (h : Module.finrank 𝕜 E = 1) {v : E} (hv : ‖v‖ = 1)

Mathlib/Analysis/Normed/Lp/Finsupp.lean

@@ -0,0 +1,102 @@
+/-
+Copyright (c) 2026 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+module
+
+public import Mathlib.Algebra.BigOperators.Finsupp.Basic
+public import Mathlib.Analysis.Normed.Lp.WithLp
+public import Mathlib.Analysis.SpecialFunctions.Pow.NNReal
+public import Mathlib.Topology.MetricSpace.Basic
+
+import Mathlib.Algebra.Order.BigOperators.Group.Finset
+import Mathlib.Analysis.MeanInequalities
+import Mathlib.Data.ENNReal.BigOperators
+import Mathlib.Tactic.Positivity.Finset
+
+/-!
+# Direct sum of metric spaces
+
+This files endows the direct sum `ι →₀ X` of `ι`-many copies of a metric space `X` with the
+L^p metric.
+
+## TODO
+
+Allow the L^∞ metric too. Currently, there is no easy way to perform the proofs:
+`match` on `ℝ≥0∞` exposes the underlying `Option` and `induction p using ENNReal.recTopCoe` in the
+`EMetricSpace` instance chokes on the `PseudoEMetricSpace` one.
+-/
+
+open scoped ENNReal NNReal
+
+public section
+
+namespace Finsupp
+variable {ι X : Type*} [Zero X] {p : ℝ≥0} [Fact (1 ≤ p)]
+
+/-- The L^1 extended metric on `ι`-many copies of a metric space `X` -/
+noncomputable instance [PseudoEMetricSpace X] : PseudoEMetricSpace (WithLp p <| ι →₀ X) where
+  edist f g :=
+  ((f.ofLp.zipWith edist (edist_self _) g.ofLp).sum fun i r ↦ r ^ (p : ℝ)) ^ (p⁻¹ : ℝ)
+  edist_self f := by
+    have : 0 < p := zero_lt_one.trans_le Fact.out
+    simp [sum, *]
+  edist_comm f g := by
+    simp only [sum, zipWith_apply, edist_comm]
+    congr 2
+    ext i
+    simp [edist_comm]
+  edist_triangle f g h := by
+    classical
+    have : 0 < p := zero_lt_one.trans_le Fact.out
+    let s := f.ofLp.support ∪ g.ofLp.support ∪ h.ofLp.support
+    rw [sum_of_support_subset (s := s) _ (by grind [support_zipWith]) _ (by simp [*]),
+      sum_of_support_subset (s := s) _ (by grind [support_zipWith]) _ (by simp [*]),
+      sum_of_support_subset (s := s) _ (by grind [support_zipWith]) _ (by simp [*])]
+    simp only [zipWith_apply, ← one_div]
+    grw [← ENNReal.Lp_add_le _ _ _ (mod_cast Fact.out)]
+    gcongr
+    exact edist_triangle ..
+
+lemma edist_def [PseudoEMetricSpace X] {p : ℝ≥0} [Fact (1 ≤ p)]
+    (f g : WithLp p <| ι →₀ X) :
+    edist f g =
+      ((f.ofLp.zipWith edist (edist_self _) g.ofLp).sum fun _i r ↦ r ^ (p : ℝ)) ^ (p⁻¹ : ℝ) := rfl
+
+/-- The L^1 extended metric on `ι`-many copies of a metric space `X` -/
+noncomputable instance [EMetricSpace X] : EMetricSpace (WithLp p <| ι →₀ X) where
+  eq_of_edist_eq_zero {f g} hfg := by simp_all [edist_def, sum, WithLp.ext_iff, DFunLike.ext_iff]
+
+/-- The L^1 metric on `ι`-many copies of a metric space `X` -/
+noncomputable instance [PseudoMetricSpace X] : PseudoMetricSpace (WithLp p <| ι →₀ X) :=
+  PseudoEMetricSpace.toPseudoMetricSpaceOfDist
+    (fun f g ↦ ((f.ofLp.zipWith dist (dist_self _) g.ofLp).sum fun i r ↦ r ^ (p : ℝ)) ^ (p⁻¹ : ℝ))
+    (fun f g ↦ by dsimp [sum]; positivity) fun f g ↦ by
+      simp only [edist_def, sum, zipWith_apply, ← coe_nnreal_ennreal_nndist, NNReal.zero_le_coe,
+        ← ENNReal.coe_rpow_of_nonneg, ← ENNReal.ofNNReal_finsetSum, inv_nonneg, ← coe_nndist,
+        ← NNReal.coe_rpow, ← NNReal.coe_sum, ENNReal.ofReal_coe_nnreal, ENNReal.coe_inj]
+      congr! 2
+      ext i
+      simp [← coe_nndist, ← coe_nnreal_ennreal_nndist]
+
+lemma dist_def [PseudoMetricSpace X] (f g : WithLp p <| ι →₀ X) :
+    dist f g =
+      ((f.ofLp.zipWith dist (dist_self _) g.ofLp).sum fun _i r ↦ r ^ (p : ℝ)) ^ (p⁻¹ : ℝ) := rfl
+
+lemma nndist_def [PseudoMetricSpace X] (f g : WithLp p <| ι →₀ X) :
+    nndist f g =
+      ((f.ofLp.zipWith nndist (nndist_self _) g.ofLp).sum fun _i r ↦ r ^ (p : ℝ)) ^ (p⁻¹ : ℝ) := by
+  ext
+  simp only [coe_nndist, dist_def, sum, zipWith_apply, NNReal.coe_sum, NNReal.coe_rpow]
+  congr 2
+  ext i
+  simp [← coe_nndist]
+
+/-- The L^1 metric on `ι`-many copies of a metric space `X` -/
+noncomputable instance [MetricSpace X] : MetricSpace (WithLp p <| ι →₀ X) :=
+  EMetricSpace.toMetricSpaceOfDist
+    (fun f g ↦ ((f.ofLp.zipWith dist (dist_self _) g.ofLp).sum fun i r ↦ r ^ (p : ℝ)) ^ (p⁻¹ : ℝ))
+    (fun f g ↦ by dsimp [sum]; positivity) fun f g ↦ by rw [edist_dist, dist_def]
+
+end Finsupp

Mathlib/Analysis/Normed/Lp/WithLp.lean

@@ -101,6 +101,9 @@ variable {K V}
 lemma ofLp_toLp (x : V) : ofLp (toLp p x) = x := rfl
 @[simp] lemma toLp_ofLp (x : WithLp p V) : toLp p (ofLp x) = x := rfl
 
+lemma ext_iff {x y : WithLp p V} : x = y ↔ x.ofLp = y.ofLp :=
+  (WithLp.equiv p V).injective.eq_iff.symm
+
 lemma ofLp_surjective : Function.Surjective (@ofLp p V) :=
   Function.RightInverse.surjective <| ofLp_toLp _
 

Mathlib/Data/ENNReal/Basic.lean

@@ -191,6 +191,12 @@ instance : Inhabited ℝ≥0∞ := ⟨0⟩
 def recTopCoe {C : ℝ≥0∞ → Sort*} (top : C ∞) (coe : ∀ x : ℝ≥0, C x) (x : ℝ≥0∞) : C x :=
   WithTop.recTopCoe top coe x
 
+@[simp] lemma recTopCoe_top {C : ℝ≥0∞ → Sort*} (top : C ∞) (coe : ∀ x : ℝ≥0, C x) :
+    recTopCoe top coe ∞ = top := rfl
+
+@[simp] lemma recTopCoe_ofNNReal {C : ℝ≥0∞ → Sort*} (top : C ∞) (coe : ∀ x : ℝ≥0, C x) (x : ℝ≥0) :
+    recTopCoe top coe x = coe x := rfl
+
 instance canLift : CanLift ℝ≥0∞ ℝ≥0 ofNNReal (· ≠ ∞) := WithTop.canLift
 
 @[simp] theorem none_eq_top : (none : ℝ≥0∞) = ∞ := rfl

Mathlib/Data/Finset/Lattice/Fold.lean

@@ -260,6 +260,10 @@ theorem sup_mem (s : Set α) (w₁ : ⊥ ∈ s) (w₂ : ∀ᵉ (x ∈ s) (y ∈
 protected theorem sup_eq_bot_iff (f : β → α) (S : Finset β) : S.sup f = ⊥ ↔ ∀ s ∈ S, f s = ⊥ := by
   classical induction S using Finset.induction <;> simp [*]
 
+@[to_additive (attr := simp)]
+lemma sup_eq_one [One α] [IsBotOneClass α] : s.sup f = 1 ↔ ∀ i ∈ s, f i = 1 := by
+  simp [← bot_eq_one]
+
 @[to_dual (attr := simp)]
 lemma sup_disjSum (s : Finset β) (t : Finset γ) (f : β ⊕ γ → α) :
     (s.disjSum t).sup f = (s.sup fun x ↦ f (.inl x)) ⊔ (t.sup fun x ↦ f (.inr x)) :=
@@ -663,14 +667,18 @@ end Sup'
 
 section Sup
 
-variable [SemilatticeSup α] [OrderBot α]
+variable [SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α}
 
 @[to_dual]
-theorem sup'_eq_sup {s : Finset β} (H : s.Nonempty) (f : β → α) : s.sup' H f = s.sup f :=
+theorem sup'_eq_sup (H : s.Nonempty) (f : β → α) : s.sup' H f = s.sup f :=
   le_antisymm (sup'_le H f fun _ => le_sup) (Finset.sup_le fun _ => le_sup' f)
 
+@[to_additive (attr := simp)]
+lemma sup'_eq_one [One α] [IsBotOneClass α] (hs) : s.sup' hs f = 1 ↔ ∀ i ∈ s, f i = 1 := by
+  simp [sup'_eq_sup]
+
 @[to_dual]
-theorem coe_sup_of_nonempty {s : Finset β} (h : s.Nonempty) (f : β → α) :
+theorem coe_sup_of_nonempty (h : s.Nonempty) (f : β → α) :
     (↑(s.sup f) : WithBot α) = s.sup ((↑) ∘ f) := by simp only [← sup'_eq_sup h, coe_sup' h]
 
 end Sup

Mathlib/Data/NNReal/Defs.lean

@@ -165,6 +165,7 @@ theorem _root_.Real.le_coe_toNNReal (r : ℝ) : r ≤ Real.toNNReal r :=
   le_max_left r 0
 
 @[bound] theorem coe_nonneg (r : ℝ≥0) : (0 : ℝ) ≤ r := r.2
+@[simp] lemma not_toReal_neg {r : ℝ≥0} : ¬ r.toReal < 0 := r.coe_nonneg.not_gt
 
 @[simp, norm_cast] theorem coe_mk (a : ℝ) (ha) : toReal (.mk a ha) = a := rfl