feat: add a TietzeExtension class (#9788)

This adds a class `TietzeExtension` to encode the Tietze extension theorem as a type class that can be satisfied by various types. For now, we provide instances for `ℝ`, `ℝ≥0`, `ℂ`, `IsROrC 𝕜`, pi types, product types, as well as constructors via homeomorphisms or retracts of a `TietzeExtension` space, and also a constructor for finite dimensional topological vector spaces.

Mathlib.lean

@@ -699,6 +699,7 @@ import Mathlib.Analysis.Complex.RealDeriv
 import Mathlib.Analysis.Complex.RemovableSingularity
 import Mathlib.Analysis.Complex.Schwarz
 import Mathlib.Analysis.Complex.TaylorSeries
+import Mathlib.Analysis.Complex.Tietze
 import Mathlib.Analysis.Complex.UnitDisc.Basic
 import Mathlib.Analysis.Complex.UpperHalfPlane.Basic
 import Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty

Mathlib/Analysis/Complex/Tietze.lean

@@ -0,0 +1,120 @@
+/-
+Copyright (c) 2024 Jireh Loreaux. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jireh Loreaux
+-/
+import Mathlib.Analysis.Complex.Basic
+import Mathlib.Data.IsROrC.Lemmas
+import Mathlib.Topology.TietzeExtension
+import Mathlib.Analysis.NormedSpace.HomeomorphBall
+import Mathlib.Analysis.NormedSpace.IsROrC
+/-!
+# Finite dimensional topological vector spaces over `ℝ` satisfy the Tietze extension property
+
+There are two main results here:
+
+- `IsROrC.instTietzeExtensionTVS`: finite dimensional topological vector spaces over `ℝ` (or `ℂ`)
+  have the Tietze extension property.
+- `BoundedContinuousFunction.exists_norm_eq_restrict_eq`: when mapping into a finite dimensional
+  normed vector space over `ℝ` (or `ℂ`), the extension can be chosen to preserve the norm of the
+  bounded continuous function it extends.
+
+-/
+
+universe u u₁ v w
+
+-- this is not an instance because Lean cannot determine `𝕜`.
+theorem TietzeExtension.of_tvs (𝕜 : Type v) [NontriviallyNormedField 𝕜] {E : Type w}
+    [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E]
+    [T2Space E] [FiniteDimensional 𝕜 E] [CompleteSpace 𝕜] [TietzeExtension.{u, v} 𝕜] :
+    TietzeExtension.{u, w} E :=
+  Basis.ofVectorSpace 𝕜 E |>.equivFun.toContinuousLinearEquiv.toHomeomorph |> .of_homeo
+
+instance Complex.instTietzeExtension : TietzeExtension ℂ :=
+  TietzeExtension.of_tvs ℝ
+
+instance (priority := 900) IsROrC.instTietzeExtension {𝕜 : Type*} [IsROrC 𝕜] : TietzeExtension 𝕜 :=
+  TietzeExtension.of_tvs ℝ
+
+instance IsROrC.instTietzeExtensionTVS {𝕜 : Type v} [IsROrC 𝕜] {E : Type w}
+    [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E]
+    [ContinuousSMul 𝕜 E] [T2Space E] [FiniteDimensional 𝕜 E] :
+    TietzeExtension.{u, w} E :=
+  TietzeExtension.of_tvs 𝕜
+
+instance Set.instTietzeExtensionUnitBall {𝕜 : Type v} [IsROrC 𝕜] {E : Type w}
+    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] :
+    TietzeExtension.{u, w} (Metric.ball (0 : E) 1) :=
+  have : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
+  .of_homeo Homeomorph.unitBall.symm
+
+instance Set.instTietzeExtensionUnitClosedBall {𝕜 : Type v} [IsROrC 𝕜] {E : Type w}
+    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] :
+    TietzeExtension.{u, w} (Metric.closedBall (0 : E) 1) := by
+  have : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
+  have : IsScalarTower ℝ 𝕜 E := Real.isScalarTower
+  -- I didn't find this retract in Mathlib.
+  let g : E → E := fun x ↦ ‖x‖⁻¹ • x
+  classical
+  suffices this : Continuous (piecewise (Metric.closedBall 0 1) id g) by
+    refine .of_retract ⟨Subtype.val, by continuity⟩ ⟨_, this.codRestrict fun x ↦ ?_⟩ ?_
+    · by_cases hx : x ∈ Metric.closedBall 0 1
+      · simpa [piecewise_eq_of_mem (hi := hx)] using hx
+      · simp only [piecewise_eq_of_not_mem (hi := hx), IsROrC.real_smul_eq_coe_smul (K := 𝕜)]
+        by_cases hx' : x = 0 <;> simp [hx']
+    · ext x
+      simp [piecewise_eq_of_mem (hi := x.property)]
+  refine continuous_piecewise (fun x hx ↦ ?_) continuousOn_id ?_
+  · replace hx : ‖x‖ = 1 := by simpa [frontier_closedBall (0 : E) one_ne_zero] using hx
+    simp [hx]
+  · refine continuousOn_id.norm.inv₀ ?_ |>.smul continuousOn_id
+    simp only [closure_compl, interior_closedBall (0 : E) one_ne_zero, mem_compl_iff,
+      Metric.mem_ball, dist_zero_right, not_lt, id_eq, ne_eq, norm_eq_zero]
+    exact fun x hx ↦ norm_pos_iff.mp <| one_pos.trans_le hx
+
+theorem Metric.instTietzeExtensionBall {𝕜 : Type v} [IsROrC 𝕜] {E : Type w}
+    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] {r : ℝ} (hr : 0 < r) :
+    TietzeExtension.{u, w} (Metric.ball (0 : E) r) :=
+  have : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
+  .of_homeo <| show (Metric.ball (0 : E) r) ≃ₜ (Metric.ball (0 : E) 1) from
+    PartialHomeomorph.unitBallBall (0 : E) r hr |>.toHomeomorphSourceTarget.symm
+
+theorem Metric.instTietzeExtensionClosedBall (𝕜 : Type v) [IsROrC 𝕜] {E : Type w}
+    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] (y : E) {r : ℝ} (hr : 0 < r) :
+    TietzeExtension.{u, w} (Metric.closedBall y r) :=
+  .of_homeo <| by
+    show (Metric.closedBall y r) ≃ₜ (Metric.closedBall (0 : E) 1)
+    symm
+    apply (DilationEquiv.smulTorsor y (k := (r : 𝕜)) <| by exact_mod_cast hr.ne').toHomeomorph.sets
+    ext x
+    simp only [mem_closedBall, dist_zero_right, DilationEquiv.coe_toHomeomorph, Set.mem_preimage,
+      DilationEquiv.smulTorsor_apply, vadd_eq_add, dist_add_self_left, norm_smul,
+      IsROrC.norm_ofReal, abs_of_nonneg hr.le]
+    exact (mul_le_iff_le_one_right hr).symm
+
+variable {X : Type u} [TopologicalSpace X] [NormalSpace X] {s : Set X} (hs : IsClosed s)
+variable (𝕜 : Type v) [IsROrC 𝕜] [TietzeExtension.{u, v} 𝕜]
+variable {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E]
+
+namespace BoundedContinuousFunction
+
+/-- **Tietze extension theorem** for real-valued bounded continuous maps, a version with a closed
+embedding and bundled composition. If `e : C(X, Y)` is a closed embedding of a topological space
+into a normal topological space and `f : X →ᵇ ℝ` is a bounded continuous function, then there exists
+a bounded continuous function `g : Y →ᵇ ℝ` of the same norm such that `g ∘ e = f`. -/
+theorem exists_norm_eq_restrict_eq (f : s →ᵇ E) :
+    ∃ g : X →ᵇ E, ‖g‖ = ‖f‖ ∧ g.restrict s = f := by
+  by_cases hf : ‖f‖ = 0; · exact ⟨0, by aesop⟩
+  have := Metric.instTietzeExtensionClosedBall.{u, v} 𝕜 (0 : E) (by aesop : 0 < ‖f‖)
+  have hf' x : f x ∈ Metric.closedBall 0 ‖f‖ := by simpa using f.norm_coe_le_norm x
+  obtain ⟨g, hg_mem, hg⟩ := (f : C(s, E)).exists_forall_mem_restrict_eq hs hf'
+  simp only [Metric.mem_closedBall, dist_zero_right] at hg_mem
+  let g' : X →ᵇ E := .ofNormedAddCommGroup g (map_continuous g) ‖f‖ hg_mem
+  refine ⟨g', ?_, by ext x; congrm($(hg) x)⟩
+  apply le_antisymm ((g'.norm_le <| by positivity).mpr hg_mem)
+  refine (f.norm_le <| by positivity).mpr fun x ↦ ?_
+  have hx : f x = g' x := by simpa using congr($(hg) x).symm
+  rw [hx]
+  exact g'.norm_le (norm_nonneg g') |>.mp le_rfl x
+
+end BoundedContinuousFunction

Mathlib/Topology/Separation/NotNormal.lean

@@ -41,7 +41,7 @@ theorem IsClosed.mk_lt_continuum [NormalSpace X] {s : Set X} (hs : IsClosed s)
     -- By the Tietze Extension Theorem, any function `f : C(s, ℝ)` can be extended to `C(X, ℝ)`,
     -- hence `#C(s, ℝ) ≤ #C(X, ℝ)`
     _ ≤ #C(X, ℝ) := by
-      choose f hf using (ContinuousMap.exists_restrict_eq_of_closed · hs)
+      choose f hf using ContinuousMap.exists_restrict_eq (Y := ℝ) hs
       have hfi : Injective f := LeftInverse.injective hf
       exact mk_le_of_injective hfi
     -- Since `t` is dense, restriction `C(X, ℝ) → C(t, ℝ)` is injective, hence `#C(X, ℝ) ≤ #C(t, ℝ)`

Mathlib/Topology/TietzeExtension.lean

@@ -24,6 +24,12 @@ The proof mostly follows <https://ncatlab.org/nlab/show/Tietze+extension+theorem
 gap in the proof for unbounded functions, see
 `exists_extension_forall_exists_le_ge_of_closedEmbedding`.
 
+In addition we provide a class `TietzeExtension` encoding the idea that a topological space
+satisfies the Tietze extension theorem. This allows us to get a version of the Tietze extension
+theorem that simultaneously applies to `ℝ`, `ℝ × ℝ`, `ℂ`, `ι → ℝ`, `ℝ≥0` et cetera. At some point
+in the future, it may be desirable to provide instead a more general approach via
+*absolute retracts*, but the current implementation covers the most common use cases easily.
+
 ## Implementation notes
 
 We first prove the theorems for a closed embedding `e : X → Y` of a topological space into a normal
@@ -34,6 +40,117 @@ topological space, then specialize them to the case `X = s : Set Y`, `e = (↑)`
 Tietze extension theorem, Urysohn's lemma, normal topological space
 -/
 
+/-!  ### The `TietzeExtension` class -/
+
+section TietzeExtensionClass
+
+universe u u₁ u₂ v w
+
+-- TODO: define *absolute retracts* and then prove they satisfy Tietze extension.
+-- Then make instances of that instead and remove this class.
+/-- A class encoding the concept that a space satisfies the Tietze extension property. -/
+class TietzeExtension (Y : Type v) [TopologicalSpace Y] : Prop where
+  exists_restrict_eq' {X : Type u} [TopologicalSpace X] [NormalSpace X] (s : Set X)
+    (hs : IsClosed s) (f : C(s, Y)) : ∃ (g : C(X, Y)), g.restrict s = f
+
+variable {X₁ : Type u₁} [TopologicalSpace X₁]
+variable {X : Type u} [TopologicalSpace X] [NormalSpace X] {s : Set X} (hs : IsClosed s)
+variable {e : X₁ → X} (he : ClosedEmbedding e)
+variable {Y : Type v} [TopologicalSpace Y] [TietzeExtension.{u, v} Y]
+
+/-- **Tietze extension theorem** for `TietzeExtension` spaces, a version for a closed set. Let
+`s` be a closed set in a normal topological space `X₂`. Let `f` be a continuous function
+on `s` with values in a `TietzeExtension` space `Y`. Then there exists a continuous function
+`g : C(X₂, Y)` such that `g.restrict s = f`. -/
+theorem ContinuousMap.exists_restrict_eq (f : C(s, Y)) : ∃ (g : C(X, Y)), g.restrict s = f :=
+  TietzeExtension.exists_restrict_eq' s hs f
+#align continuous_map.exists_restrict_eq_of_closed ContinuousMap.exists_restrict_eq
+
+/-- **Tietze extension theorem** for `TietzeExtension` spaces. Let `e` be a closed embedding of a
+nonempty topological space `X₁` into a normal topological space `X₂`. Let `f` be a continuous
+function on `X₁` with values in a `TietzeExtension` space `Y`. Then there exists a
+continuous function `g : C(X₂, Y)` such that `g ∘ e = f`. -/
+theorem ContinuousMap.exists_extension (f : C(X₁, Y)) :
+    ∃ (g : C(X, Y)), g.comp ⟨e, he.continuous⟩ = f := by
+  let e' : X₁ ≃ₜ Set.range e := Homeomorph.ofEmbedding _ he.toEmbedding
+  obtain ⟨g, hg⟩ := (f.comp e'.symm).exists_restrict_eq he.closed_range
+  exact ⟨g, by ext x; simpa using congr($(hg) ⟨e' x, x, rfl⟩)⟩
+
+/-- **Tietze extension theorem** for `TietzeExtension` spaces. Let `e` be a closed embedding of a
+nonempty topological space `X₁` into a normal topological space `X₂`. Let `f` be a continuous
+function on `X₁` with values in a `TietzeExtension` space `Y`. Then there exists a
+continuous function `g : C(X₂, Y)` such that `g ∘ e = f`.
+
+This version is provided for convenience and backwards compatibility. Here the composition is
+phrased in terms of bare functions. -/
+theorem ContinuousMap.exists_extension' (f : C(X₁, Y)) : ∃ (g : C(X, Y)), g ∘ e = f :=
+  f.exists_extension he |>.imp fun g hg ↦ by ext x; congrm($(hg) x)
+#align continuous_map.exists_extension_of_closed_embedding ContinuousMap.exists_extension'
+
+/-- This theorem is not intended to be used directly because it is rare for a set alone to
+satisfy `[TietzeExtension t]`. For example, `Metric.ball` in `ℝ` only satisfies it when
+the radius is strictly positive, so finding this as an instance will fail.
+
+Instead, it is intended to be used as a constructor for theorems about sets which *do* satisfy
+`[TietzeExtension t]` under some hypotheses. -/
+theorem ContinuousMap.exists_forall_mem_restrict_eq {Y : Type v} [TopologicalSpace Y] (f : C(s, Y))
+    {t : Set Y} (hf : ∀ x, f x ∈ t) [ht : TietzeExtension.{u, v} t] :
+    ∃ (g : C(X, Y)), (∀ x, g x ∈ t) ∧ g.restrict s = f := by
+  obtain ⟨g, hg⟩ := mk _ (map_continuous f |>.codRestrict hf) |>.exists_restrict_eq hs
+  exact ⟨comp ⟨Subtype.val, by continuity⟩ g, by simp, by ext x; congrm(($(hg) x : Y))⟩
+
+/-- This theorem is not intended to be used directly because it is rare for a set alone to
+satisfy `[TietzeExtension t]`. For example, `Metric.ball` in `ℝ` only satisfies it when
+the radius is strictly positive, so finding this as an instance will fail.
+
+Instead, it is intended to be used as a constructor for theorems about sets which *do* satisfy
+`[TietzeExtension t]` under some hypotheses. -/
+theorem ContinuousMap.exists_extension_forall_mem {Y : Type v} [TopologicalSpace Y] (f : C(X₁, Y))
+    {t : Set Y} (hf : ∀ x, f x ∈ t) [ht : TietzeExtension.{u, v} t] :
+    ∃ (g : C(X, Y)), (∀ x, g x ∈ t) ∧ g.comp ⟨e, he.continuous⟩ = f := by
+  obtain ⟨g, hg⟩ := mk _ (map_continuous f |>.codRestrict hf) |>.exists_extension he
+  exact ⟨comp ⟨Subtype.val, by continuity⟩ g, by simp, by ext x; congrm(($(hg) x : Y))⟩
+
+instance Pi.instTietzeExtension {ι : Type*} {Y : ι → Type v} [∀ i, TopologicalSpace (Y i)]
+    [∀ i, TietzeExtension (Y i)] : TietzeExtension (∀ i, Y i) where
+  exists_restrict_eq' s hs f := by
+    obtain ⟨g', hg'⟩ := Classical.skolem.mp <| fun i ↦
+      ContinuousMap.exists_restrict_eq hs (ContinuousMap.piEquiv _ _ |>.symm f i)
+    exact ⟨ContinuousMap.piEquiv _ _ g', by ext x i; congrm($(hg' i) x)⟩
+
+instance Prod.instTietzeExtension {Y : Type v} {Z : Type w} [TopologicalSpace Y]
+    [TietzeExtension.{u, v} Y] [TopologicalSpace Z] [TietzeExtension.{u, w} Z] :
+    TietzeExtension (Y × Z) where
+  exists_restrict_eq' s hs f := by
+    obtain ⟨g₁, hg₁⟩ := (ContinuousMap.fst.comp f).exists_restrict_eq hs
+    obtain ⟨g₂, hg₂⟩ := (ContinuousMap.snd.comp f).exists_restrict_eq hs
+    exact ⟨g₁.prodMk g₂, by ext1 x; congrm(($(hg₁) x), $(hg₂) x)⟩
+
+instance Unique.instTietzeExtension {Y : Type v} [TopologicalSpace Y] [Unique Y] :
+    TietzeExtension.{u, v} Y where
+  exists_restrict_eq' _ _ f := ⟨.const _ default, by ext x; exact Subsingleton.elim _ _⟩
+
+/-- Any retract of a `TietzeExtension` space is one itself.-/
+theorem TietzeExtension.of_retract {Y : Type v} {Z : Type w} [TopologicalSpace Y]
+    [TopologicalSpace Z] [TietzeExtension.{u, w} Z] (ι : C(Y, Z)) (r : C(Z, Y))
+    (h : r.comp ι = .id Y) : TietzeExtension.{u, v} Y where
+  exists_restrict_eq' s hs f := by
+    obtain ⟨g, hg⟩ := (ι.comp f).exists_restrict_eq hs
+    use r.comp g
+    ext1 x
+    have := congr(r.comp $(hg))
+    rw [← r.comp_assoc ι, h, f.id_comp] at this
+    congrm($this x)
+
+/-- Any homeomorphism from a `TietzeExtension` space is one itself.-/
+theorem TietzeExtension.of_homeo {Y : Type v} {Z : Type w} [TopologicalSpace Y]
+    [TopologicalSpace Z] [TietzeExtension.{u, w} Z] (e : Y ≃ₜ Z) :
+    TietzeExtension.{u, v} Y :=
+  .of_retract (e : C(Y, Z)) (e.symm : C(Z, Y)) <| by simp
+
+end TietzeExtensionClass
+
+/-! The Tietze extension theorem for `ℝ`. -/
 
 variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [NormalSpace Y]
 
@@ -380,15 +497,8 @@ theorem exists_extension_forall_mem_of_closedEmbedding (f : C(X, ℝ)) {t : Set
     exact hgG.2 (congr_fun hGF _)
 #align continuous_map.exists_extension_forall_mem_of_closed_embedding ContinuousMap.exists_extension_forall_mem_of_closedEmbedding
 
-/-- **Tietze extension theorem** for real-valued continuous maps, a version for a closed
-embedding. Let `e` be a closed embedding of a nonempty topological space `X` into a normal
-topological space `Y`. Let `f` be a continuous real-valued function on `X`. Then there exists a
-continuous real-valued function `g : C(Y, ℝ)` such that `g ∘ e = f`. -/
-theorem exists_extension_of_closedEmbedding (f : C(X, ℝ)) (e : X → Y) (he : ClosedEmbedding e) :
-    ∃ g : C(Y, ℝ), g ∘ e = f :=
-  (exists_extension_forall_mem_of_closedEmbedding f (fun _ => mem_univ _) univ_nonempty he).imp
-    fun _ => And.right
-#align continuous_map.exists_extension_of_closed_embedding ContinuousMap.exists_extension_of_closedEmbedding
+alias exists_extension_of_closedEmbedding := exists_extension'
+attribute [deprecated] exists_extension_of_closedEmbedding -- deprecated since 2024-01-16
 
 /-- **Tietze extension theorem** for real-valued continuous maps, a version for a closed set. Let
 `s` be a closed set in a normal topological space `Y`. Let `f` be a continuous real-valued function
@@ -404,15 +514,21 @@ theorem exists_restrict_eq_forall_mem_of_closed {s : Set Y} (f : C(s, ℝ)) {t :
   ⟨g, hgt, coe_injective hgf⟩
 #align continuous_map.exists_restrict_eq_forall_mem_of_closed ContinuousMap.exists_restrict_eq_forall_mem_of_closed
 
-/-- **Tietze extension theorem** for real-valued continuous maps, a version for a closed set. Let
-`s` be a closed set in a normal topological space `Y`. Let `f` be a continuous real-valued function
-on `s`. Then there exists a continuous real-valued function `g : C(Y, ℝ)` such that
-`g.restrict s = f`. -/
-theorem exists_restrict_eq_of_closed {s : Set Y} (f : C(s, ℝ)) (hs : IsClosed s) :
-    ∃ g : C(Y, ℝ), g.restrict s = f :=
-  let ⟨g, _, hgf⟩ :=
-    exists_restrict_eq_forall_mem_of_closed f (fun _ => mem_univ _) univ_nonempty hs
-  ⟨g, hgf⟩
-#align continuous_map.exists_restrict_eq_of_closed ContinuousMap.exists_restrict_eq_of_closed
+alias exists_restrict_eq_of_closed := exists_restrict_eq
+attribute [deprecated] exists_restrict_eq_of_closed -- deprecated since 2024-01-16
 
 end ContinuousMap
+
+/-- **Tietze extension theorem** for real-valued continuous maps.
+`ℝ` is a `TietzeExtension` space. -/
+instance Real.instTietzeExtension : TietzeExtension ℝ where
+  exists_restrict_eq' _s hs f :=
+    f.exists_restrict_eq_forall_mem_of_closed (fun _ => mem_univ _) univ_nonempty hs |>.imp
+      fun _ ↦ (And.right ·)
+
+open NNReal in
+/-- **Tietze extension theorem** for nonnegative real-valued continuous maps.
+`ℝ≥0` is a `TietzeExtension` space. -/
+instance NNReal.instTietzeExtension : TietzeExtension ℝ≥0 :=
+  .of_retract ⟨((↑) : ℝ≥0 → ℝ), by continuity⟩ ⟨Real.toNNReal, continuous_real_toNNReal⟩ <| by
+    ext; simp