chore(Analysis/Normed/Operator): move extension to a new file (#29888)

The moved parts are not modified except for adapting the sections and imports.

Original definition of `ContinuousLinearMap.extend` was by Zhouhang Zhou in 2019 (mathlib3 PR #1649)

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: mcdoll

Mathlib.lean

@@ -1883,6 +1883,7 @@ import Mathlib.Analysis.Normed.Operator.Compact
 import Mathlib.Analysis.Normed.Operator.Completeness
 import Mathlib.Analysis.Normed.Operator.Conformal
 import Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
+import Mathlib.Analysis.Normed.Operator.Extend
 import Mathlib.Analysis.Normed.Operator.LinearIsometry
 import Mathlib.Analysis.Normed.Operator.Mul
 import Mathlib.Analysis.Normed.Operator.NNNorm

Mathlib/Analysis/InnerProductSpace/LinearPMap.lean

@@ -5,7 +5,7 @@ Authors: Moritz Doll
 -/
 import Mathlib.Analysis.InnerProductSpace.Adjoint
 import Mathlib.Analysis.InnerProductSpace.ProdL2
-import Mathlib.Analysis.Normed.Operator.Completeness
+import Mathlib.Analysis.Normed.Operator.Extend
 import Mathlib.Topology.Algebra.Module.Equiv
 import Mathlib.Topology.Algebra.Module.LinearPMap
 

Mathlib/Analysis/Normed/Operator/Completeness.lean

@@ -155,88 +155,4 @@ theorem isCompact_image_coe_closedBall [ProperSpace F] (f₀ : E →SL[σ₁₂]
 
 end Completeness
 
-section UniformlyExtend
-
-section NonField
-
-variable {R R₂ E F Fₗ : Type*} [AddCommGroup E] [UniformSpace E] [IsUniformAddGroup E]
-  [AddCommGroup F] [UniformSpace F] [IsUniformAddGroup F] [T0Space F]
-  [AddCommMonoid Fₗ] [UniformSpace Fₗ] [ContinuousAdd Fₗ]
-  [Semiring R] [Semiring R₂] [Module R E] [Module R₂ F] [Module R Fₗ]
-  [ContinuousConstSMul R Fₗ] [ContinuousConstSMul R₂ F]
-  {σ₁₂ : R →+* R₂} (f g : E →SL[σ₁₂] F) [CompleteSpace F] (e : E →L[R] Fₗ) (h_dense : DenseRange e)
-
-variable (h_e : IsUniformInducing e)
-
-/-- Extension of a continuous linear map `f : E →SL[σ₁₂] F`, with `E` a normed space and `F` a
-complete normed space, along a uniform and dense embedding `e : E →L[𝕜] Fₗ`. -/
-def extend : Fₗ →SL[σ₁₂] F :=
-  -- extension of `f` is continuous
-  have cont := (uniformContinuous_uniformly_extend h_e h_dense f.uniformContinuous).continuous
-  -- extension of `f` agrees with `f` on the domain of the embedding `e`
-  have eq := uniformly_extend_of_ind h_e h_dense f.uniformContinuous
-  { toFun := (h_e.isDenseInducing h_dense).extend f
-    map_add' := by
-      refine h_dense.induction_on₂ ?_ ?_
-      · exact isClosed_eq (cont.comp continuous_add)
-          ((cont.comp continuous_fst).add (cont.comp continuous_snd))
-      · intro x y
-        simp only [eq, ← e.map_add]
-        exact f.map_add _ _
-    map_smul' := fun k => by
-      refine fun b => h_dense.induction_on b ?_ ?_
-      · exact isClosed_eq (cont.comp (continuous_const_smul _))
-          ((continuous_const_smul _).comp cont)
-      · intro x
-        rw [← map_smul]
-        simp only [eq]
-        exact ContinuousLinearMap.map_smulₛₗ _ _ _
-    cont }
-
-@[simp]
-theorem extend_eq (x : E) : extend f e h_dense h_e (e x) = f x :=
-  IsDenseInducing.extend_eq (h_e.isDenseInducing h_dense) f.cont _
-
-theorem extend_unique (g : Fₗ →SL[σ₁₂] F) (H : g.comp e = f) : extend f e h_dense h_e = g :=
-  ContinuousLinearMap.coeFn_injective <|
-    uniformly_extend_unique h_e h_dense (ContinuousLinearMap.ext_iff.1 H) g.continuous
-
-@[simp]
-theorem extend_zero : extend (0 : E →SL[σ₁₂] F) e h_dense h_e = 0 :=
-  extend_unique _ _ _ _ _ (zero_comp _)
-
-end NonField
-
-section
-
-variable [CompleteSpace F] (e : E →L[𝕜] Fₗ) (h_dense : DenseRange e)
-
-variable {N : ℝ≥0} (h_e : ∀ x, ‖x‖ ≤ N * ‖e x‖) [RingHomIsometric σ₁₂]
-
-/-- If a dense embedding `e : E →L[𝕜] G` expands the norm by a constant factor `N⁻¹`, then the
-norm of the extension of `f` along `e` is bounded by `N * ‖f‖`. -/
-theorem opNorm_extend_le :
-    ‖f.extend e h_dense (isUniformEmbedding_of_bound _ h_e).isUniformInducing‖ ≤ N * ‖f‖ := by
-  -- Add `opNorm_le_of_dense`?
-  refine opNorm_le_bound _ ?_ (isClosed_property h_dense (isClosed_le ?_ ?_) fun x ↦ ?_)
-  · cases le_total 0 N with
-    | inl hN => exact mul_nonneg hN (norm_nonneg _)
-    | inr hN =>
-      have : Unique E := ⟨⟨0⟩, fun x ↦ norm_le_zero_iff.mp <|
-        (h_e x).trans (mul_nonpos_of_nonpos_of_nonneg hN (norm_nonneg _))⟩
-      obtain rfl : f = 0 := Subsingleton.elim ..
-      simp
-  · exact (cont _).norm
-  · exact continuous_const.mul continuous_norm
-  · rw [extend_eq]
-    calc
-      ‖f x‖ ≤ ‖f‖ * ‖x‖ := le_opNorm _ _
-      _ ≤ ‖f‖ * (N * ‖e x‖) := mul_le_mul_of_nonneg_left (h_e x) (norm_nonneg _)
-      _ ≤ N * ‖f‖ * ‖e x‖ := by rw [mul_comm ↑N ‖f‖, mul_assoc]
-
-
-end
-
-end UniformlyExtend
-
 end ContinuousLinearMap

Mathlib/Analysis/Normed/Operator/Extend.lean

@@ -0,0 +1,118 @@
+/-
+Copyright (c) 2025 Moritz Doll. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Moritz Doll, Zhouhang Zhou
+-/
+import Mathlib.Analysis.Normed.Operator.Basic
+
+/-!
+
+# Extension of continuous linear maps on Banach spaces
+
+In this file we provide two different ways to extend a continuous linear map defined on a dense
+subspace to the entire Banach space.
+
+* `ContinuousLinearMap.extend`: Extend from a dense subspace using `IsUniformInducing`
+* `ContinuousLinearMap.extendOfNorm`: Extend from a continuous linear map that is a dense
+injection into the domain and using a norm estimate.
+
+-/
+
+suppress_compilation
+
+open scoped NNReal
+
+variable {𝕜 𝕜₂ E Eₗ F Fₗ : Type*}
+
+namespace ContinuousLinearMap
+
+section Extend
+
+section Ring
+
+variable [AddCommGroup E] [UniformSpace E] [IsUniformAddGroup E]
+  [AddCommGroup F] [UniformSpace F] [IsUniformAddGroup F] [T0Space F]
+  [AddCommMonoid Eₗ] [UniformSpace Eₗ] [ContinuousAdd Eₗ]
+  [Semiring 𝕜] [Semiring 𝕜₂] [Module 𝕜 E] [Module 𝕜₂ F] [Module 𝕜 Eₗ]
+  [ContinuousConstSMul 𝕜 Eₗ] [ContinuousConstSMul 𝕜₂ F]
+  {σ₁₂ : 𝕜 →+* 𝕜₂} (f g : E →SL[σ₁₂] F) [CompleteSpace F] (e : E →L[𝕜] Eₗ)
+
+variable (h_dense : DenseRange e) (h_e : IsUniformInducing e)
+
+/-- Extension of a continuous linear map `f : E →SL[σ₁₂] F`, with `E` a normed space and `F` a
+complete normed space, along a uniform and dense embedding `e : E →L[𝕜] Eₗ`. -/
+def extend : Eₗ →SL[σ₁₂] F :=
+  -- extension of `f` is continuous
+  have cont := (uniformContinuous_uniformly_extend h_e h_dense f.uniformContinuous).continuous
+  -- extension of `f` agrees with `f` on the domain of the embedding `e`
+  have eq := uniformly_extend_of_ind h_e h_dense f.uniformContinuous
+  { toFun := (h_e.isDenseInducing h_dense).extend f
+    map_add' := by
+      refine h_dense.induction_on₂ ?_ ?_
+      · exact isClosed_eq (cont.comp continuous_add)
+          ((cont.comp continuous_fst).add (cont.comp continuous_snd))
+      · intro x y
+        simp only [eq, ← e.map_add]
+        exact f.map_add _ _
+    map_smul' := fun k => by
+      refine fun b => h_dense.induction_on b ?_ ?_
+      · exact isClosed_eq (cont.comp (continuous_const_smul _))
+          ((continuous_const_smul _).comp cont)
+      · intro x
+        rw [← map_smul]
+        simp only [eq]
+        exact ContinuousLinearMap.map_smulₛₗ _ _ _
+    cont }
+
+@[simp]
+theorem extend_eq (x : E) : extend f e h_dense h_e (e x) = f x :=
+  IsDenseInducing.extend_eq (h_e.isDenseInducing h_dense) f.cont _
+
+theorem extend_unique (g : Eₗ →SL[σ₁₂] F) (H : g.comp e = f) : extend f e h_dense h_e = g :=
+  ContinuousLinearMap.coeFn_injective <|
+    uniformly_extend_unique h_e h_dense (ContinuousLinearMap.ext_iff.1 H) g.continuous
+
+@[simp]
+theorem extend_zero : extend (0 : E →SL[σ₁₂] F) e h_dense h_e = 0 :=
+  extend_unique _ _ _ _ _ (zero_comp _)
+
+end Ring
+
+section NormedField
+
+variable [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂}
+  [NormedAddCommGroup E] [NormedAddCommGroup Eₗ] [NormedAddCommGroup F] [NormedAddCommGroup Fₗ]
+  [NormedSpace 𝕜 E] [NormedSpace 𝕜 Eₗ] [NormedSpace 𝕜₂ F] [NormedSpace 𝕜₂ Fₗ] [CompleteSpace F]
+  (f g : E →SL[σ₁₂] F) (e : E →L[𝕜] Eₗ)
+
+variable (h_dense : DenseRange e) (h_e : IsUniformInducing e)
+
+variable {N : ℝ≥0} (h_e : ∀ x, ‖x‖ ≤ N * ‖e x‖) [RingHomIsometric σ₁₂]
+
+/-- If a dense embedding `e : E →L[𝕜] G` expands the norm by a constant factor `N⁻¹`, then the
+norm of the extension of `f` along `e` is bounded by `N * ‖f‖`. -/
+theorem opNorm_extend_le :
+    ‖f.extend e h_dense (isUniformEmbedding_of_bound _ h_e).isUniformInducing‖ ≤ N * ‖f‖ := by
+  -- Add `opNorm_le_of_dense`?
+  refine opNorm_le_bound _ ?_ (isClosed_property h_dense (isClosed_le ?_ ?_) fun x ↦ ?_)
+  · cases le_total 0 N with
+    | inl hN => exact mul_nonneg hN (norm_nonneg _)
+    | inr hN =>
+      have : Unique E := ⟨⟨0⟩, fun x ↦ norm_le_zero_iff.mp <|
+        (h_e x).trans (mul_nonpos_of_nonpos_of_nonneg hN (norm_nonneg _))⟩
+      obtain rfl : f = 0 := Subsingleton.elim ..
+      simp
+  · exact (cont _).norm
+  · exact continuous_const.mul continuous_norm
+  · rw [extend_eq]
+    calc
+      ‖f x‖ ≤ ‖f‖ * ‖x‖ := le_opNorm _ _
+      _ ≤ ‖f‖ * (N * ‖e x‖) := mul_le_mul_of_nonneg_left (h_e x) (norm_nonneg _)
+      _ ≤ N * ‖f‖ * ‖e x‖ := by rw [mul_comm ↑N ‖f‖, mul_assoc]
+
+
+end NormedField
+
+end Extend
+
+end ContinuousLinearMap

Mathlib/MeasureTheory/Integral/SetToL1.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Zhouhang Zhou, Yury Kudryashov, Sébastien Gouëzel, Rémy Degenne
 -/
 import Mathlib.MeasureTheory.Integral.FinMeasAdditive
-import Mathlib.Analysis.Normed.Operator.Completeness
+import Mathlib.Analysis.Normed.Operator.Extend
 
 /-!
 # Extension of a linear function from indicators to L1