[Merged by Bors] - feat: Lipschitz extensions of maps into l^infty

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)]
 
@@ -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`
@@ -1217,3 +1220,41 @@ instance completeSpace : CompleteSpace (lp E p) :=
 end Topology
 
 end lp
+
+section Lipschitz
+
+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 : α) :
+    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

Mathlib/Topology/MetricSpace/Kuratowski.lean

@@ -14,35 +14,33 @@ 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.
+
 -/
 
 
 noncomputable section
 
 set_option linter.uppercaseLean3 false
 
-open Set Metric TopologicalSpace
-
-open scoped ENNReal
-
-local notation "ℓ_infty_ℝ" => lp (fun n : ℕ => ℝ) ∞
+open Set Metric TopologicalSpace NNReal ENNReal lp Function
 
 universe u v w
 
 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 +91,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,21 +110,59 @@ 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 [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 α)
 #align Kuratowski_embedding.isometry kuratowskiEmbedding.isometry
 
 /-- 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
+
+/--
+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]
+
+The same result for the case of a finite type `ι` is implemented in
+`LipschitzOnWith.extend_pi`.
+-/
+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
+    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 ⟨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₀
+      use ‖f a₀‖
+      rintro - ⟨i, rfl⟩
+      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 ↦ ⟨swap g i, hf_extb i⟩
+    refine ⟨f_ext', ?_, ?_⟩
+    · rw [LipschitzWith.coordinate]
+      exact hgl
+    · intro a hyp
+      ext i
+      exact (hgeq i) hyp

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
@@ -669,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.
-TODO: state the same result (with the same proof) for the space `ℓ^∞ (ι, ℝ)` over a possibly
-infinite type `ι`. -/
+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

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},