From 2372d46eea6272883305712f1168f54da3eb3f36 Mon Sep 17 00:00:00 2001 From: Chris Camano Date: Sun, 18 Jun 2023 00:43:51 +0000 Subject: [PATCH] feat: Lipschitz extensions of maps into l^infty (#5107) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A function `f : α → ℓ^∞(ι, ℝ)` which is `K`-Lipschitz on a subset `s` admits a `K`-Lipschitz extension to the whole space. Co-authored-by: Ian Bunner <31334766+ian-bunner@users.noreply.github.com> Co-authored-by: Chris Camano <53490775+chriscamano@users.noreply.github.com> --- Mathlib/Analysis/NormedSpace/lpSpace.lean | 43 ++++++++++++- Mathlib/Topology/MetricSpace/Kuratowski.lean | 66 +++++++++++++++----- Mathlib/Topology/MetricSpace/Lipschitz.lean | 8 ++- docs/references.bib | 7 +++ 4 files changed, 105 insertions(+), 19 deletions(-) diff --git a/Mathlib/Analysis/NormedSpace/lpSpace.lean b/Mathlib/Analysis/NormedSpace/lpSpace.lean index 676271c41c133..ac8ca40f5e96d 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)] @@ -324,6 +324,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` @@ -1216,3 +1219,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 diff --git a/Mathlib/Topology/MetricSpace/Kuratowski.lean b/Mathlib/Topology/MetricSpace/Kuratowski.lean index c964112f36378..0eee480494ce1 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,7 @@ 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 @@ -34,15 +32,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 +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,12 +110,15 @@ 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 α) @@ -125,8 +126,43 @@ 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 + +/-- +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 diff --git a/Mathlib/Topology/MetricSpace/Lipschitz.lean b/Mathlib/Topology/MetricSpace/Lipschitz.lean index 22528e3b68008..37e37c731002a 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 @@ -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 diff --git a/docs/references.bib b/docs/references.bib index a100599230101..bebb2203a92e8 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},