From 6638be9e2cc8bae31685d0fccea4c9d2de88d076 Mon Sep 17 00:00:00 2001
From: prendagast <chriscamano007@gmail.com>
Date: Thu, 15 Jun 2023 14:49:23 -0700
Subject: [PATCH 01/16] Lipschitz_ext

---
 Mathlib/Topology/MetricSpace/Kuratowski.lean | 87 ++++++++++++++++----
 1 file changed, 73 insertions(+), 14 deletions(-)

diff --git a/Mathlib/Topology/MetricSpace/Kuratowski.lean b/Mathlib/Topology/MetricSpace/Kuratowski.lean
index c964112f36378..5c0c3437713ed 100644
--- a/Mathlib/Topology/MetricSpace/Kuratowski.lean
+++ b/Mathlib/Topology/MetricSpace/Kuratowski.lean
@@ -14,7 +14,9 @@ import Mathlib.Topology.Sets.Compacts
 /-!
 # The Kuratowski embedding
 
-Any separable metric space can be embedded isometrically in `ℓ^∞(ℝ)`.
+Any separable metric space can be embedded isometrically in `ℓ^∞(ℕ, ℝ)`.
+Any partially defined Lipschitz map into `ℓ^∞` can be extended to the whole space.
+
 -/
 
 
@@ -22,11 +24,9 @@ noncomputable section
 
 set_option linter.uppercaseLean3 false
 
-open Set Metric TopologicalSpace
-
-open scoped ENNReal
+open Set Metric TopologicalSpace NNReal ENNReal
 
-local notation "ℓ_infty_ℝ" => lp (fun n : ℕ => ℝ) ∞
+notation "ℓ^∞(" ι ") " => lp (fun i : ι => ℝ ) ∞
 
 universe u v w
 
@@ -34,15 +34,15 @@ variable {α : Type u} {β : Type v} {γ : Type w}
 
 namespace KuratowskiEmbedding
 
-/-! ### Any separable metric space can be embedded isometrically in ℓ^∞(ℝ) -/
+/-! ### Any separable metric space can be embedded isometrically in ℓ^∞(ℕ, ℝ) -/
 
 
-variable {f g : ℓ_infty_ℝ} {n : ℕ} {C : ℝ} [MetricSpace α] (x : ℕ → α) (a b : α)
+variable {f g : ℓ^∞(ℕ)} {n : ℕ} {C : ℝ} [MetricSpace α] (x : ℕ → α) (a b : α)
 
 /-- A metric space can be embedded in `l^∞(ℝ)` via the distances to points in
 a fixed countable set, if this set is dense. This map is given in `kuratowskiEmbedding`,
 without density assumptions. -/
-def embeddingOfSubset : ℓ_infty_ℝ :=
+def embeddingOfSubset : ℓ^∞(ℕ) :=
   ⟨fun n => dist a (x n) - dist (x 0) (x n), by
     apply memℓp_infty
     use dist a (x 0)
@@ -93,9 +93,9 @@ theorem embeddingOfSubset_isometry (H : DenseRange x) : Isometry (embeddingOfSub
   simpa [dist_comm] using this
 #align Kuratowski_embedding.embedding_of_subset_isometry KuratowskiEmbedding.embeddingOfSubset_isometry
 
-/-- Every separable metric space embeds isometrically in `ℓ_infty_ℝ`. -/
+/-- Every separable metric space embeds isometrically in `ℓ^∞(ℕ)`. -/
 theorem exists_isometric_embedding (α : Type u) [MetricSpace α] [SeparableSpace α] :
-    ∃ f : α → ℓ_infty_ℝ, Isometry f := by
+    ∃ f : α → ℓ^∞(ℕ), Isometry f := by
   cases' (univ : Set α).eq_empty_or_nonempty with h h
   · use fun _ => 0; intro x; exact absurd h (Nonempty.ne_empty ⟨x, mem_univ x⟩)
   · -- We construct a map x : ℕ → α with dense image
@@ -112,12 +112,16 @@ end KuratowskiEmbedding
 
 open TopologicalSpace KuratowskiEmbedding
 
-/-- The Kuratowski embedding is an isometric embedding of a separable metric space in `ℓ^∞(ℝ)`. -/
-def kuratowskiEmbedding (α : Type u) [MetricSpace α] [SeparableSpace α] : α → ℓ_infty_ℝ :=
+/-- The Kuratowski embedding is an isometric embedding of a separable metric space in `ℓ^∞(ℕ, ℝ)`. -/
+def kuratowskiEmbedding (α : Type u) [MetricSpace α] [SeparableSpace α] : α → ℓ^∞(ℕ) :=
   Classical.choose (KuratowskiEmbedding.exists_isometric_embedding α)
 #align Kuratowski_embedding kuratowskiEmbedding
 
-/-- The Kuratowski embedding is an isometry. -/
+/--
+    The Kuratowski embedding is an isometry.
+    Theorem 2.1 of Metric Embeddings and Lipschitz Extensions by Assaf Naor
+    https://web.math.princeton.edu/~naor/homepage%20files/embeddings_extensions.pdf
+ -/
 protected theorem kuratowskiEmbedding.isometry (α : Type u) [MetricSpace α] [SeparableSpace α] :
     Isometry (kuratowskiEmbedding α) :=
   Classical.choose_spec (exists_isometric_embedding α)
@@ -125,8 +129,63 @@ protected theorem kuratowskiEmbedding.isometry (α : Type u) [MetricSpace α] [S
 
 /-- Version of the Kuratowski embedding for nonempty compacts -/
 nonrec def NonemptyCompacts.kuratowskiEmbedding (α : Type u) [MetricSpace α] [CompactSpace α]
-    [Nonempty α] : NonemptyCompacts ℓ_infty_ℝ where
+    [Nonempty α] : NonemptyCompacts ℓ^∞(ℕ) where
   carrier := range (kuratowskiEmbedding α)
   isCompact' := isCompact_range (kuratowskiEmbedding.isometry α).continuous
   nonempty' := range_nonempty _
 #align nonempty_compacts.Kuratowski_embedding NonemptyCompacts.kuratowskiEmbedding
+
+theorem lipschitzWith_const [PseudoMetricSpace α] [PseudoMetricSpace β] (b: β) (K : ℝ≥0):
+  LipschitzWith K (fun _ : α ↦ b):= by
+  intro x y; simp
+
+/--
+    A function `f : α → (ι → ℝ)` which is `K`-Lipschitz on a subset `s` admits a `K`-Lipschitz
+    extension to the whole space.
+
+    Theorem 2.2 of Metric Embeddings and Lipschitz Extensions by Assaf Naor
+    https://web.math.princeton.edu/~naor/homepage%20files/embeddings_extensions.pdf
+-/
+theorem LipschitzOnWith.extend_linf [PseudoMetricSpace α] {s : Set α} {f : α → ℓ^∞(ι)}
+    {K : ℝ≥0} (hfl : LipschitzOnWith K f s): ∃ g : α → ℓ^∞(ι), LipschitzWith K g ∧ EqOn f g s := by
+  -- Construct the coordinate-wise extensions
+  have : ∀ i : ι, ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn (fun x => f x i) g s
+  · intro i
+    apply LipschitzOnWith.extend_real -- use the nonlinear Hahn-Banach theorem here!
+    rw [lipschitzOnWith_iff_dist_le_mul] at hfl ⊢
+    intro x hx y hy
+    calc
+      dist (f x i) (f y i) ≤ dist (f x) (f y) := lp.norm_apply_le_norm top_ne_zero (f x - f y) i
+      _ ≤ K * dist x y := hfl x hx y hy
+  choose g hg using this
+  rcases s.eq_empty_or_nonempty with rfl | ⟨a₀, ha₀_in_s⟩
+  . exact ⟨fun _ ↦ 0, lipschitzWith_const 0 K, by simp⟩
+  · let f_ext : α → ι → ℝ := fun x i ↦ g i x
+    -- Show that the extensions are uniformly bounded
+    have hf_extb : ∀ a : α, Memℓp (f_ext a) ∞
+    · intro a
+      let M : ℝ := ‖f a₀‖
+      use K * dist a a₀ + M
+      rintro - ⟨i, rfl⟩
+      rcases hg i with ⟨hgl, hgr⟩
+      calc
+        |g i a| = |g i a - f a₀ i + f a₀ i| := by simp
+        _ ≤ |g i a - f a₀ i| + |f a₀ i| := abs_add _ _
+        _ ≤ |g i a - g i a₀| + |g i a₀ - f a₀ i| + |f a₀ i| := by gcongr; apply abs_sub_le
+        _ = |g i a - g i a₀| + |f a₀ i| := by simp [hgr ha₀_in_s]
+        _ ≤ ↑K * dist a a₀ + |f a₀ i| := by
+            gcongr
+            exact lipschitzWith_iff_dist_le_mul.1 hgl a a₀
+        _ ≤ ↑K * dist a a₀ + M := by
+            gcongr
+            exact lp.norm_apply_le_norm top_ne_zero (f a₀) i
+    -- Construct witness by bundling the function with its certificate of membership in ℓ^∞
+    let f_ext' : α → ℓ^∞(ι) := fun i ↦ ⟨f_ext i, hf_extb i⟩
+    refine ⟨f_ext', ?_, ?_⟩
+    · rw [lipschitzWith_iff_dist_le_mul]
+      intro x y
+      apply lp.norm_le_of_forall_le; positivity
+      exact fun i ↦ lipschitzWith_iff_dist_le_mul.mp (hg i).1 x y
+    · intro a hyp
+      ext i
+      exact (hg i).2 hyp

From 2c8a90f073ffe5c64e81dfb47dbbba71e190bebf Mon Sep 17 00:00:00 2001
From: prendagast <chriscamano007@gmail.com>
Date: Thu, 15 Jun 2023 14:56:11 -0700
Subject: [PATCH 02/16] Moved lip_const

---
 Mathlib/Topology/MetricSpace/Kuratowski.lean | 6 +-----
 Mathlib/Topology/MetricSpace/Lipschitz.lean  | 3 +++
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Topology/MetricSpace/Kuratowski.lean b/Mathlib/Topology/MetricSpace/Kuratowski.lean
index 5c0c3437713ed..3fd26323699c3 100644
--- a/Mathlib/Topology/MetricSpace/Kuratowski.lean
+++ b/Mathlib/Topology/MetricSpace/Kuratowski.lean
@@ -135,10 +135,6 @@ nonrec def NonemptyCompacts.kuratowskiEmbedding (α : Type u) [MetricSpace α] [
   nonempty' := range_nonempty _
 #align nonempty_compacts.Kuratowski_embedding NonemptyCompacts.kuratowskiEmbedding
 
-theorem lipschitzWith_const [PseudoMetricSpace α] [PseudoMetricSpace β] (b: β) (K : ℝ≥0):
-  LipschitzWith K (fun _ : α ↦ b):= by
-  intro x y; simp
-
 /--
     A function `f : α → (ι → ℝ)` which is `K`-Lipschitz on a subset `s` admits a `K`-Lipschitz
     extension to the whole space.
@@ -159,7 +155,7 @@ theorem LipschitzOnWith.extend_linf [PseudoMetricSpace α] {s : Set α} {f : α
       _ ≤ K * dist x y := hfl x hx y hy
   choose g hg using this
   rcases s.eq_empty_or_nonempty with rfl | ⟨a₀, ha₀_in_s⟩
-  . exact ⟨fun _ ↦ 0, lipschitzWith_const 0 K, by simp⟩
+  . exact ⟨fun _ ↦ 0, LipschitzWith.const' 0, by simp⟩
   · let f_ext : α → ι → ℝ := fun x i ↦ g i x
     -- Show that the extensions are uniformly bounded
     have hf_extb : ∀ a : α, Memℓp (f_ext a) ∞
diff --git a/Mathlib/Topology/MetricSpace/Lipschitz.lean b/Mathlib/Topology/MetricSpace/Lipschitz.lean
index 22528e3b68008..7ab78f9e986f0 100644
--- a/Mathlib/Topology/MetricSpace/Lipschitz.lean
+++ b/Mathlib/Topology/MetricSpace/Lipschitz.lean
@@ -200,6 +200,9 @@ protected theorem const (b : β) : LipschitzWith 0 fun _ : α => b := fun x y =>
   simp only [edist_self, zero_le]
 #align lipschitz_with.const LipschitzWith.const
 
+protected theorem const' (b : β) {K : ℝ≥0} : LipschitzWith K fun _ : α => b := fun x y => by
+  simp only [edist_self, zero_le]
+
 protected theorem id : LipschitzWith 1 (@id α) :=
   LipschitzWith.of_edist_le fun _ _ => le_rfl
 #align lipschitz_with.id LipschitzWith.id

From 108f22c50d192d60d093d9c24cd919826d94cd31 Mon Sep 17 00:00:00 2001
From: prendagast <chriscamano007@gmail.com>
Date: Thu, 15 Jun 2023 15:04:08 -0700
Subject: [PATCH 03/16] fixed line break error

---
 Mathlib/Topology/MetricSpace/Kuratowski.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Topology/MetricSpace/Kuratowski.lean b/Mathlib/Topology/MetricSpace/Kuratowski.lean
index 3fd26323699c3..a9d0a3096e99d 100644
--- a/Mathlib/Topology/MetricSpace/Kuratowski.lean
+++ b/Mathlib/Topology/MetricSpace/Kuratowski.lean
@@ -26,7 +26,7 @@ set_option linter.uppercaseLean3 false
 
 open Set Metric TopologicalSpace NNReal ENNReal
 
-notation "ℓ^∞(" ι ") " => lp (fun i : ι => ℝ ) ∞
+local notation "ℓ^∞(" ι ") " => lp (fun i : ι => ℝ ) ∞
 
 universe u v w
 
@@ -112,7 +112,8 @@ end KuratowskiEmbedding
 
 open TopologicalSpace KuratowskiEmbedding
 
-/-- The Kuratowski embedding is an isometric embedding of a separable metric space in `ℓ^∞(ℕ, ℝ)`. -/
+/-- The Kuratowski embedding is an isometric embedding of a separable metric space in `ℓ^∞(ℕ, ℝ)`.
+-/
 def kuratowskiEmbedding (α : Type u) [MetricSpace α] [SeparableSpace α] : α → ℓ^∞(ℕ) :=
   Classical.choose (KuratowskiEmbedding.exists_isometric_embedding α)
 #align Kuratowski_embedding kuratowskiEmbedding

From 5ea801be4e1fb3169b5773cbbc59001dadca6d07 Mon Sep 17 00:00:00 2001
From: prendagast <chriscamano007@gmail.com>
Date: Thu, 15 Jun 2023 15:08:33 -0700
Subject: [PATCH 04/16] fixed doc string

---
 Mathlib/Topology/MetricSpace/Kuratowski.lean | 3 +++
 Mathlib/Topology/MetricSpace/Lipschitz.lean  | 4 ++--
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Topology/MetricSpace/Kuratowski.lean b/Mathlib/Topology/MetricSpace/Kuratowski.lean
index a9d0a3096e99d..40f2d25576dba 100644
--- a/Mathlib/Topology/MetricSpace/Kuratowski.lean
+++ b/Mathlib/Topology/MetricSpace/Kuratowski.lean
@@ -142,6 +142,9 @@ nonrec def NonemptyCompacts.kuratowskiEmbedding (α : Type u) [MetricSpace α] [
 
     Theorem 2.2 of Metric Embeddings and Lipschitz Extensions by Assaf Naor
     https://web.math.princeton.edu/~naor/homepage%20files/embeddings_extensions.pdf
+
+    The same result for the case of a finite type `ι` is implemented in
+    `LipschitzOnWith.extend_pi`.
 -/
 theorem LipschitzOnWith.extend_linf [PseudoMetricSpace α] {s : Set α} {f : α → ℓ^∞(ι)}
     {K : ℝ≥0} (hfl : LipschitzOnWith K f s): ∃ g : α → ℓ^∞(ι), LipschitzWith K g ∧ EqOn f g s := by
diff --git a/Mathlib/Topology/MetricSpace/Lipschitz.lean b/Mathlib/Topology/MetricSpace/Lipschitz.lean
index 7ab78f9e986f0..9b2533a5d0a6b 100644
--- a/Mathlib/Topology/MetricSpace/Lipschitz.lean
+++ b/Mathlib/Topology/MetricSpace/Lipschitz.lean
@@ -673,8 +673,8 @@ theorem LipschitzOnWith.extend_real [PseudoMetricSpace α] {f : α → ℝ} {s :
 
 /-- A function `f : α → (ι → ℝ)` which is `K`-Lipschitz on a subset `s` admits a `K`-Lipschitz
 extension to the whole space.
-TODO: state the same result (with the same proof) for the space `ℓ^∞ (ι, ℝ)` over a possibly
-infinite type `ι`. -/
+The same result (with the same proof) for the space `ℓ^∞ (ι, ℝ)` over a possibly
+infinite type `ι` is implemented in `LipschitzOnWith.extend_linf`. -/
 theorem LipschitzOnWith.extend_pi [PseudoMetricSpace α] [Fintype ι] {f : α → ι → ℝ} {s : Set α}
     {K : ℝ≥0} (hf : LipschitzOnWith K f s) : ∃ g : α → ι → ℝ, LipschitzWith K g ∧ EqOn f g s := by
   have : ∀ i, ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn (fun x => f x i) g s := fun i => by

From 5bae036421252130101e93aca33ab5586f76d439 Mon Sep 17 00:00:00 2001
From: prendagast <chriscamano007@gmail.com>
Date: Thu, 15 Jun 2023 17:20:16 -0700
Subject: [PATCH 05/16] correct indentation

---
 Mathlib/Topology/MetricSpace/Kuratowski.lean | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/Mathlib/Topology/MetricSpace/Kuratowski.lean b/Mathlib/Topology/MetricSpace/Kuratowski.lean
index 40f2d25576dba..33565b3f8a75b 100644
--- a/Mathlib/Topology/MetricSpace/Kuratowski.lean
+++ b/Mathlib/Topology/MetricSpace/Kuratowski.lean
@@ -119,9 +119,9 @@ def kuratowskiEmbedding (α : Type u) [MetricSpace α] [SeparableSpace α] : α
 #align Kuratowski_embedding kuratowskiEmbedding
 
 /--
-    The Kuratowski embedding is an isometry.
-    Theorem 2.1 of Metric Embeddings and Lipschitz Extensions by Assaf Naor
-    https://web.math.princeton.edu/~naor/homepage%20files/embeddings_extensions.pdf
+The Kuratowski embedding is an isometry.
+Theorem 2.1 of Metric Embeddings and Lipschitz Extensions by Assaf Naor
+https://web.math.princeton.edu/~naor/homepage%20files/embeddings_extensions.pdf
  -/
 protected theorem kuratowskiEmbedding.isometry (α : Type u) [MetricSpace α] [SeparableSpace α] :
     Isometry (kuratowskiEmbedding α) :=
@@ -137,14 +137,14 @@ nonrec def NonemptyCompacts.kuratowskiEmbedding (α : Type u) [MetricSpace α] [
 #align nonempty_compacts.Kuratowski_embedding NonemptyCompacts.kuratowskiEmbedding
 
 /--
-    A function `f : α → (ι → ℝ)` which is `K`-Lipschitz on a subset `s` admits a `K`-Lipschitz
-    extension to the whole space.
+A function `f : α → (ι → ℝ)` which is `K`-Lipschitz on a subset `s` admits a `K`-Lipschitz
+extension to the whole space.
 
-    Theorem 2.2 of Metric Embeddings and Lipschitz Extensions by Assaf Naor
-    https://web.math.princeton.edu/~naor/homepage%20files/embeddings_extensions.pdf
+Theorem 2.2 of Metric Embeddings and Lipschitz Extensions by Assaf Naor
+https://web.math.princeton.edu/~naor/homepage%20files/embeddings_extensions.pdf
 
-    The same result for the case of a finite type `ι` is implemented in
-    `LipschitzOnWith.extend_pi`.
+The same result for the case of a finite type `ι` is implemented in
+`LipschitzOnWith.extend_pi`.
 -/
 theorem LipschitzOnWith.extend_linf [PseudoMetricSpace α] {s : Set α} {f : α → ℓ^∞(ι)}
     {K : ℝ≥0} (hfl : LipschitzOnWith K f s): ∃ g : α → ℓ^∞(ι), LipschitzWith K g ∧ EqOn f g s := by

From 736ad9b493833f414405b2e28379c0761d772bf8 Mon Sep 17 00:00:00 2001
From: prendagast <chriscamano007@gmail.com>
Date: Thu, 15 Jun 2023 17:29:15 -0700
Subject: [PATCH 06/16] citation

---
 Mathlib/Topology/MetricSpace/Kuratowski.lean | 7 ++-----
 docs/references.bib                          | 7 +++++++
 2 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Topology/MetricSpace/Kuratowski.lean b/Mathlib/Topology/MetricSpace/Kuratowski.lean
index 33565b3f8a75b..44fdd37a2c7b8 100644
--- a/Mathlib/Topology/MetricSpace/Kuratowski.lean
+++ b/Mathlib/Topology/MetricSpace/Kuratowski.lean
@@ -120,9 +120,7 @@ def kuratowskiEmbedding (α : Type u) [MetricSpace α] [SeparableSpace α] : α
 
 /--
 The Kuratowski embedding is an isometry.
-Theorem 2.1 of Metric Embeddings and Lipschitz Extensions by Assaf Naor
-https://web.math.princeton.edu/~naor/homepage%20files/embeddings_extensions.pdf
- -/
+Theorem 2.1 of [Assaf Naor, *Metric Embeddings and Lipschitz Extensions*][Naor-2015]. -/
 protected theorem kuratowskiEmbedding.isometry (α : Type u) [MetricSpace α] [SeparableSpace α] :
     Isometry (kuratowskiEmbedding α) :=
   Classical.choose_spec (exists_isometric_embedding α)
@@ -140,8 +138,7 @@ nonrec def NonemptyCompacts.kuratowskiEmbedding (α : Type u) [MetricSpace α] [
 A function `f : α → (ι → ℝ)` which is `K`-Lipschitz on a subset `s` admits a `K`-Lipschitz
 extension to the whole space.
 
-Theorem 2.2 of Metric Embeddings and Lipschitz Extensions by Assaf Naor
-https://web.math.princeton.edu/~naor/homepage%20files/embeddings_extensions.pdf
+Theorem 2.2 of [Assaf Naor, *Metric Embeddings and Lipschitz Extensions*][Naor-2015]
 
 The same result for the case of a finite type `ι` is implemented in
 `LipschitzOnWith.extend_pi`.
diff --git a/docs/references.bib b/docs/references.bib
index a100599230101..bc901f539d133 100644
--- a/docs/references.bib
+++ b/docs/references.bib
@@ -1832,6 +1832,13 @@ @Article{         MR577178
   url           = {https://doi.org/10.1007/BF00417500}
 }
 
+@unpublished{Naor-2015,
+  author = {Assaf Naor},
+  title  = {Metric Embeddings and Lipschitz Extensions},
+  year   = {2015},
+  url    = {https://web.math.princeton.edu/~naor/homepage%20files/embeddings_extensions.pdf}
+}
+
 @Article{         Nash-Williams63,
   title         = {On well-quasi-ordering finite trees},
   volume        = {59},

From 9b23db4193a53b36ce169ca68b4a5831e17fd70b Mon Sep 17 00:00:00 2001
From: prendagast <chriscamano007@gmail.com>
Date: Thu, 15 Jun 2023 17:31:31 -0700
Subject: [PATCH 07/16] theorem rename

---
 Mathlib/Topology/MetricSpace/Kuratowski.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Topology/MetricSpace/Kuratowski.lean b/Mathlib/Topology/MetricSpace/Kuratowski.lean
index 44fdd37a2c7b8..f19f23e9a1563 100644
--- a/Mathlib/Topology/MetricSpace/Kuratowski.lean
+++ b/Mathlib/Topology/MetricSpace/Kuratowski.lean
@@ -143,7 +143,7 @@ Theorem 2.2 of [Assaf Naor, *Metric Embeddings and Lipschitz Extensions*][Naor-2
 The same result for the case of a finite type `ι` is implemented in
 `LipschitzOnWith.extend_pi`.
 -/
-theorem LipschitzOnWith.extend_linf [PseudoMetricSpace α] {s : Set α} {f : α → ℓ^∞(ι)}
+theorem LipschitzOnWith.extend_lp_infty [PseudoMetricSpace α] {s : Set α} {f : α → ℓ^∞(ι)}
     {K : ℝ≥0} (hfl : LipschitzOnWith K f s): ∃ g : α → ℓ^∞(ι), LipschitzWith K g ∧ EqOn f g s := by
   -- Construct the coordinate-wise extensions
   have : ∀ i : ι, ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn (fun x => f x i) g s

From 693799fb9d84c3cba633c2441fda2090a71626ef Mon Sep 17 00:00:00 2001
From: prendagast <chriscamano007@gmail.com>
Date: Thu, 15 Jun 2023 17:33:04 -0700
Subject: [PATCH 08/16] theorem statement correction

---
 Mathlib/Topology/MetricSpace/Kuratowski.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Topology/MetricSpace/Kuratowski.lean b/Mathlib/Topology/MetricSpace/Kuratowski.lean
index f19f23e9a1563..3a030c2039fa1 100644
--- a/Mathlib/Topology/MetricSpace/Kuratowski.lean
+++ b/Mathlib/Topology/MetricSpace/Kuratowski.lean
@@ -135,7 +135,7 @@ nonrec def NonemptyCompacts.kuratowskiEmbedding (α : Type u) [MetricSpace α] [
 #align nonempty_compacts.Kuratowski_embedding NonemptyCompacts.kuratowskiEmbedding
 
 /--
-A function `f : α → (ι → ℝ)` which is `K`-Lipschitz on a subset `s` admits a `K`-Lipschitz
+A function `f : α → ℓ^∞(ι, ℝ)` which is `K`-Lipschitz on a subset `s` admits a `K`-Lipschitz
 extension to the whole space.
 
 Theorem 2.2 of [Assaf Naor, *Metric Embeddings and Lipschitz Extensions*][Naor-2015]

From 3f74b0a56e91280f094ef5a1aa0831a062fec9e4 Mon Sep 17 00:00:00 2001
From: prendagast <chriscamano007@gmail.com>
Date: Thu, 15 Jun 2023 17:35:29 -0700
Subject: [PATCH 09/16] fixed theorem statement

---
 Mathlib/Topology/MetricSpace/Lipschitz.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Topology/MetricSpace/Lipschitz.lean b/Mathlib/Topology/MetricSpace/Lipschitz.lean
index 9b2533a5d0a6b..37e37c731002a 100644
--- a/Mathlib/Topology/MetricSpace/Lipschitz.lean
+++ b/Mathlib/Topology/MetricSpace/Lipschitz.lean
@@ -672,9 +672,8 @@ theorem LipschitzOnWith.extend_real [PseudoMetricSpace α] {f : α → ℝ} {s :
 #align lipschitz_on_with.extend_real LipschitzOnWith.extend_real
 
 /-- A function `f : α → (ι → ℝ)` which is `K`-Lipschitz on a subset `s` admits a `K`-Lipschitz
-extension to the whole space.
-The same result (with the same proof) for the space `ℓ^∞ (ι, ℝ)` over a possibly
-infinite type `ι` is implemented in `LipschitzOnWith.extend_linf`. -/
+extension to the whole space. The same result for the space `ℓ^∞ (ι, ℝ)` over a possibly infinite
+type `ι` is implemented in `LipschitzOnWith.extend_lp_infty`.-/
 theorem LipschitzOnWith.extend_pi [PseudoMetricSpace α] [Fintype ι] {f : α → ι → ℝ} {s : Set α}
     {K : ℝ≥0} (hf : LipschitzOnWith K f s) : ∃ g : α → ι → ℝ, LipschitzWith K g ∧ EqOn f g s := by
   have : ∀ i, ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn (fun x => f x i) g s := fun i => by

From 79778cc443f16c742137971eeed7162c20cc1c7f Mon Sep 17 00:00:00 2001
From: prendagast <chriscamano007@gmail.com>
Date: Thu, 15 Jun 2023 17:40:02 -0700
Subject: [PATCH 10/16] added lpinf notation to lp

---
 Mathlib/Analysis/NormedSpace/lpSpace.lean    | 3 +++
 Mathlib/Topology/MetricSpace/Kuratowski.lean | 4 +---
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Analysis/NormedSpace/lpSpace.lean b/Mathlib/Analysis/NormedSpace/lpSpace.lean
index 952d65640959f..30a4be17c007c 100644
--- a/Mathlib/Analysis/NormedSpace/lpSpace.lean
+++ b/Mathlib/Analysis/NormedSpace/lpSpace.lean
@@ -325,6 +325,9 @@ def lp (E : α → Type _) [∀ i, NormedAddCommGroup (E i)] (p : ℝ≥0∞) :
   neg_mem' := Memℓp.neg
 #align lp lp
 
+scoped[lp] notation "ℓ^∞(" ι ", " E ")" => lp (fun i : ι => E) ∞
+scoped[lp] notation "ℓ^∞(" ι ")" => lp (fun i : ι => ℝ) ∞
+
 namespace lp
 
 -- Porting note: was `Coe`
diff --git a/Mathlib/Topology/MetricSpace/Kuratowski.lean b/Mathlib/Topology/MetricSpace/Kuratowski.lean
index 3a030c2039fa1..5b4c87728c9b3 100644
--- a/Mathlib/Topology/MetricSpace/Kuratowski.lean
+++ b/Mathlib/Topology/MetricSpace/Kuratowski.lean
@@ -24,9 +24,7 @@ noncomputable section
 
 set_option linter.uppercaseLean3 false
 
-open Set Metric TopologicalSpace NNReal ENNReal
-
-local notation "ℓ^∞(" ι ") " => lp (fun i : ι => ℝ ) ∞
+open Set Metric TopologicalSpace NNReal ENNReal lp
 
 universe u v w
 

From 1ce9f2c8b01632669a816ecc115ffc9bbd636c38 Mon Sep 17 00:00:00 2001
From: prendagast <chriscamano007@gmail.com>
Date: Thu, 15 Jun 2023 17:43:30 -0700
Subject: [PATCH 11/16] fixed format bib

---
 docs/references.bib | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/docs/references.bib b/docs/references.bib
index bc901f539d133..bebb2203a92e8 100644
--- a/docs/references.bib
+++ b/docs/references.bib
@@ -1832,11 +1832,11 @@ @Article{         MR577178
   url           = {https://doi.org/10.1007/BF00417500}
 }
 
-@unpublished{Naor-2015,
-  author = {Assaf Naor},
-  title  = {Metric Embeddings and Lipschitz Extensions},
-  year   = {2015},
-  url    = {https://web.math.princeton.edu/~naor/homepage%20files/embeddings_extensions.pdf}
+@Unpublished{     Naor-2015,
+  author        = {Assaf Naor},
+  title         = {Metric Embeddings and Lipschitz Extensions},
+  year          = {2015},
+  url           = {https://web.math.princeton.edu/~naor/homepage%20files/embeddings_extensions.pdf}
 }
 
 @Article{         Nash-Williams63,

From f91fae3776a3b31cb97a86f2da52dfeae0421d5c Mon Sep 17 00:00:00 2001
From: prendagast <chriscamano007@gmail.com>
Date: Fri, 16 Jun 2023 15:19:24 -0700
Subject: [PATCH 12/16] Added Lip lemmas, reduced calc block

---
 Mathlib/Analysis/NormedSpace/lpSpace.lean    | 38 +++++++++++++++-
 Mathlib/Topology/MetricSpace/Kuratowski.lean | 46 +++++++-------------
 2 files changed, 52 insertions(+), 32 deletions(-)

diff --git a/Mathlib/Analysis/NormedSpace/lpSpace.lean b/Mathlib/Analysis/NormedSpace/lpSpace.lean
index 30a4be17c007c..79d8fca64a641 100644
--- a/Mathlib/Analysis/NormedSpace/lpSpace.lean
+++ b/Mathlib/Analysis/NormedSpace/lpSpace.lean
@@ -63,7 +63,7 @@ local macro_rules | `($x ^ $y)   => `(HPow.hPow $x $y) -- Porting note: See issu
 
 noncomputable section
 
-open scoped NNReal ENNReal BigOperators
+open scoped NNReal ENNReal BigOperators Function
 
 variable {α : Type _} {E : α → Type _} {p q : ℝ≥0∞} [∀ i, NormedAddCommGroup (E i)]
 
@@ -1220,3 +1220,39 @@ instance completeSpace : CompleteSpace (lp E p) :=
 end Topology
 
 end lp
+
+section Lipschitz
+
+lemma LipschitzWith.uniformly_bounded [PseudoMetricSpace α] (g : α → ι → ℝ) {K : ℝ≥0}
+    (hg : ∀ i, LipschitzWith K (g · i)) (a₀ : α) (hga₀b : Memℓp (g a₀) ∞) (a : α) :
+    Memℓp (g a) ∞ := by
+  rcases hga₀b with ⟨M, hM⟩
+  use ↑K * dist a a₀ + M
+  rintro - ⟨i, rfl⟩
+  calc
+    |g a i| = |g a i - g a₀ i + g a₀ i| := by simp
+    _ ≤ |g a i - g a₀ i| + |g a₀ i| := abs_add _ _
+    _ ≤ ↑K * dist a a₀ + M := by
+        gcongr
+        . exact lipschitzWith_iff_dist_le_mul.1 (hg i) a a₀
+        . exact hM ⟨i, rfl⟩
+
+theorem LipschitzOnWith.coordinate [PseudoMetricSpace α] (f : α → ℓ^∞(ι)) (s : Set α) (K : ℝ≥0) :
+    LipschitzOnWith K f s ↔ ∀ i : ι, LipschitzOnWith K (fun a : α ↦ f a i) s := by
+  simp_rw [lipschitzOnWith_iff_dist_le_mul]
+  constructor
+  · intro hfl i x hx y hy
+    calc
+      dist (f x i) (f y i) ≤ dist (f x) (f y) := lp.norm_apply_le_norm top_ne_zero (f x - f y) i
+      _ ≤ K * dist x y := hfl x hx y hy
+  · intro hgl x hx y hy
+    apply lp.norm_le_of_forall_le; positivity
+    intro i
+    apply hgl i x hx y hy
+
+theorem LipschitzWith.coordinate [PseudoMetricSpace α] {f : α → ℓ^∞(ι)} (K : ℝ≥0) :
+    LipschitzWith K f ↔ ∀ i : ι, LipschitzWith K (fun a : α ↦ f a i) := by
+  simp_rw [← lipschitz_on_univ]
+  apply LipschitzOnWith.coordinate
+
+end Lipschitz
diff --git a/Mathlib/Topology/MetricSpace/Kuratowski.lean b/Mathlib/Topology/MetricSpace/Kuratowski.lean
index 5b4c87728c9b3..f3bec85faeea9 100644
--- a/Mathlib/Topology/MetricSpace/Kuratowski.lean
+++ b/Mathlib/Topology/MetricSpace/Kuratowski.lean
@@ -24,7 +24,7 @@ noncomputable section
 
 set_option linter.uppercaseLean3 false
 
-open Set Metric TopologicalSpace NNReal ENNReal lp
+open Set Metric TopologicalSpace NNReal ENNReal lp Function
 
 universe u v w
 
@@ -147,40 +147,24 @@ theorem LipschitzOnWith.extend_lp_infty [PseudoMetricSpace α] {s : Set α} {f :
   have : ∀ i : ι, ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn (fun x => f x i) g s
   · intro i
     apply LipschitzOnWith.extend_real -- use the nonlinear Hahn-Banach theorem here!
-    rw [lipschitzOnWith_iff_dist_le_mul] at hfl ⊢
-    intro x hx y hy
-    calc
-      dist (f x i) (f y i) ≤ dist (f x) (f y) := lp.norm_apply_le_norm top_ne_zero (f x - f y) i
-      _ ≤ K * dist x y := hfl x hx y hy
-  choose g hg using this
+    revert i
+    rw [← LipschitzOnWith.coordinate]
+    exact hfl
+  choose g hgl hgeq using this
   rcases s.eq_empty_or_nonempty with rfl | ⟨a₀, ha₀_in_s⟩
   . exact ⟨fun _ ↦ 0, LipschitzWith.const' 0, by simp⟩
-  · let f_ext : α → ι → ℝ := fun x i ↦ g i x
-    -- Show that the extensions are uniformly bounded
-    have hf_extb : ∀ a : α, Memℓp (f_ext a) ∞
-    · intro a
-      let M : ℝ := ‖f a₀‖
-      use K * dist a a₀ + M
+  · -- Show that the extensions are uniformly bounded
+    have hf_extb : ∀ a : α, Memℓp (swap g a) ∞
+    . apply LipschitzWith.uniformly_bounded (swap g) hgl a₀
+      use ‖f a₀‖
       rintro - ⟨i, rfl⟩
-      rcases hg i with ⟨hgl, hgr⟩
-      calc
-        |g i a| = |g i a - f a₀ i + f a₀ i| := by simp
-        _ ≤ |g i a - f a₀ i| + |f a₀ i| := abs_add _ _
-        _ ≤ |g i a - g i a₀| + |g i a₀ - f a₀ i| + |f a₀ i| := by gcongr; apply abs_sub_le
-        _ = |g i a - g i a₀| + |f a₀ i| := by simp [hgr ha₀_in_s]
-        _ ≤ ↑K * dist a a₀ + |f a₀ i| := by
-            gcongr
-            exact lipschitzWith_iff_dist_le_mul.1 hgl a a₀
-        _ ≤ ↑K * dist a a₀ + M := by
-            gcongr
-            exact lp.norm_apply_le_norm top_ne_zero (f a₀) i
+      simp_rw [←hgeq i ha₀_in_s]
+      exact lp.norm_apply_le_norm top_ne_zero (f a₀) i
     -- Construct witness by bundling the function with its certificate of membership in ℓ^∞
-    let f_ext' : α → ℓ^∞(ι) := fun i ↦ ⟨f_ext i, hf_extb i⟩
+    let f_ext' : α → ℓ^∞(ι) := fun i ↦ ⟨swap g i, hf_extb i⟩
     refine ⟨f_ext', ?_, ?_⟩
-    · rw [lipschitzWith_iff_dist_le_mul]
-      intro x y
-      apply lp.norm_le_of_forall_le; positivity
-      exact fun i ↦ lipschitzWith_iff_dist_le_mul.mp (hg i).1 x y
+    · rw [LipschitzWith.coordinate]
+      exact hgl
     · intro a hyp
       ext i
-      exact (hg i).2 hyp
+      exact (hgeq i) hyp

From 2a521378c509a8fe2b7e3377ffb23a1b3755820b Mon Sep 17 00:00:00 2001
From: prendagast <chriscamano007@gmail.com>
Date: Fri, 16 Jun 2023 15:47:55 -0700
Subject: [PATCH 13/16] fixed notation port to lip section in lp

---
 Mathlib/Analysis/NormedSpace/lpSpace.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Mathlib/Analysis/NormedSpace/lpSpace.lean b/Mathlib/Analysis/NormedSpace/lpSpace.lean
index 79d8fca64a641..1fda5bfcb63b1 100644
--- a/Mathlib/Analysis/NormedSpace/lpSpace.lean
+++ b/Mathlib/Analysis/NormedSpace/lpSpace.lean
@@ -1223,6 +1223,10 @@ end lp
 
 section Lipschitz
 
+local notation "ℓ^∞(" ι ")" => lp (fun i : ι => ℝ) ∞
+
+open ENNReal
+
 lemma LipschitzWith.uniformly_bounded [PseudoMetricSpace α] (g : α → ι → ℝ) {K : ℝ≥0}
     (hg : ∀ i, LipschitzWith K (g · i)) (a₀ : α) (hga₀b : Memℓp (g a₀) ∞) (a : α) :
     Memℓp (g a) ∞ := by

From ba4c9cdbea2bd29702ac15ba638c3234639433d6 Mon Sep 17 00:00:00 2001
From: prendagast <chriscamano007@gmail.com>
Date: Fri, 16 Jun 2023 16:07:10 -0700
Subject: [PATCH 14/16] fixed notation port

---
 Mathlib/Analysis/NormedSpace/lpSpace.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/Mathlib/Analysis/NormedSpace/lpSpace.lean b/Mathlib/Analysis/NormedSpace/lpSpace.lean
index 1fda5bfcb63b1..937ddd461655e 100644
--- a/Mathlib/Analysis/NormedSpace/lpSpace.lean
+++ b/Mathlib/Analysis/NormedSpace/lpSpace.lean
@@ -1223,9 +1223,7 @@ end lp
 
 section Lipschitz
 
-local notation "ℓ^∞(" ι ")" => lp (fun i : ι => ℝ) ∞
-
-open ENNReal
+open ENNReal lp
 
 lemma LipschitzWith.uniformly_bounded [PseudoMetricSpace α] (g : α → ι → ℝ) {K : ℝ≥0}
     (hg : ∀ i, LipschitzWith K (g · i)) (a₀ : α) (hga₀b : Memℓp (g a₀) ∞) (a : α) :

From 521d2a9e6dbf903c59211dcb77060dfd78b3ed0f Mon Sep 17 00:00:00 2001
From: Chris Camano <53490775+chriscamano@users.noreply.github.com>
Date: Fri, 16 Jun 2023 17:24:07 -0700
Subject: [PATCH 15/16] Update Mathlib/Topology/MetricSpace/Kuratowski.lean

toms golf

Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
---
 Mathlib/Topology/MetricSpace/Kuratowski.lean | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/Mathlib/Topology/MetricSpace/Kuratowski.lean b/Mathlib/Topology/MetricSpace/Kuratowski.lean
index f3bec85faeea9..6d2fb2a516f90 100644
--- a/Mathlib/Topology/MetricSpace/Kuratowski.lean
+++ b/Mathlib/Topology/MetricSpace/Kuratowski.lean
@@ -144,12 +144,10 @@ The same result for the case of a finite type `ι` is implemented in
 theorem LipschitzOnWith.extend_lp_infty [PseudoMetricSpace α] {s : Set α} {f : α → ℓ^∞(ι)}
     {K : ℝ≥0} (hfl : LipschitzOnWith K f s): ∃ g : α → ℓ^∞(ι), LipschitzWith K g ∧ EqOn f g s := by
   -- Construct the coordinate-wise extensions
+  rw [LipschitzOnWith.coordinate] at hfl
   have : ∀ i : ι, ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn (fun x => f x i) g s
   · intro i
-    apply LipschitzOnWith.extend_real -- use the nonlinear Hahn-Banach theorem here!
-    revert i
-    rw [← LipschitzOnWith.coordinate]
-    exact hfl
+    exact LipschitzOnWith.extend_real (hfl i) -- use the nonlinear Hahn-Banach theorem here!
   choose g hgl hgeq using this
   rcases s.eq_empty_or_nonempty with rfl | ⟨a₀, ha₀_in_s⟩
   . exact ⟨fun _ ↦ 0, LipschitzWith.const' 0, by simp⟩

From 6ed96a019e43efaedd5d88ac7bad5362bbf5f14d Mon Sep 17 00:00:00 2001
From: Chris Camano <53490775+chriscamano@users.noreply.github.com>
Date: Fri, 16 Jun 2023 17:24:40 -0700
Subject: [PATCH 16/16] Update Mathlib/Topology/MetricSpace/Kuratowski.lean

Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
---
 Mathlib/Topology/MetricSpace/Kuratowski.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Topology/MetricSpace/Kuratowski.lean b/Mathlib/Topology/MetricSpace/Kuratowski.lean
index 6d2fb2a516f90..0eee480494ce1 100644
--- a/Mathlib/Topology/MetricSpace/Kuratowski.lean
+++ b/Mathlib/Topology/MetricSpace/Kuratowski.lean
@@ -150,7 +150,7 @@ theorem LipschitzOnWith.extend_lp_infty [PseudoMetricSpace α] {s : Set α} {f :
     exact LipschitzOnWith.extend_real (hfl i) -- use the nonlinear Hahn-Banach theorem here!
   choose g hgl hgeq using this
   rcases s.eq_empty_or_nonempty with rfl | ⟨a₀, ha₀_in_s⟩
-  . exact ⟨fun _ ↦ 0, LipschitzWith.const' 0, by simp⟩
+  . exact ⟨0, LipschitzWith.const' 0, by simp⟩
   · -- Show that the extensions are uniformly bounded
     have hf_extb : ∀ a : α, Memℓp (swap g a) ∞
     . apply LipschitzWith.uniformly_bounded (swap g) hgl a₀