chore: move code around in NormedSpace.Multilinear.Basic (#30087)

Preparation for #22089. The current PR only moves 77 lines earlier in the file, to make it available at a point where I will need it. Pure cut and paste, no other change.

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: sgouezel

Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

@@ -825,6 +825,82 @@ protected def piFieldEquiv : G ≃ₗᵢ[𝕜] ContinuousMultilinearMap 𝕜 (fu
 
 end ContinuousMultilinearMap
 
+open ContinuousMultilinearMap
+
+namespace MultilinearMap
+
+/-- Given a map `f : G →ₗ[𝕜] MultilinearMap 𝕜 E G'` and an estimate
+`H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖`, construct a continuous linear
+map from `G` to `ContinuousMultilinearMap 𝕜 E G'`.
+
+In order to lift, e.g., a map `f : (MultilinearMap 𝕜 E G) →ₗ[𝕜] MultilinearMap 𝕜 E' G'`
+to a map `(ContinuousMultilinearMap 𝕜 E G) →L[𝕜] ContinuousMultilinearMap 𝕜 E' G'`,
+one can apply this construction to `f.comp ContinuousMultilinearMap.toMultilinearMapLinear`
+which is a linear map from `ContinuousMultilinearMap 𝕜 E G` to `MultilinearMap 𝕜 E' G'`. -/
+def mkContinuousLinear (f : G →ₗ[𝕜] MultilinearMap 𝕜 E G') (C : ℝ)
+    (H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖) : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G' :=
+  LinearMap.mkContinuous
+    { toFun := fun x => (f x).mkContinuous (C * ‖x‖) <| H x
+      map_add' := fun x y => by
+        ext1
+        simp
+      map_smul' := fun c x => by
+        ext1
+        simp }
+    (max C 0) fun x => by
+      simpa using ((f x).mkContinuous_norm_le' _).trans_eq <| by
+        rw [max_mul_of_nonneg _ _ (norm_nonneg x), zero_mul]
+
+theorem mkContinuousLinear_norm_le' (f : G →ₗ[𝕜] MultilinearMap 𝕜 E G') (C : ℝ)
+    (H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖) : ‖mkContinuousLinear f C H‖ ≤ max C 0 := by
+  dsimp only [mkContinuousLinear]
+  exact LinearMap.mkContinuous_norm_le _ (le_max_right _ _) _
+
+theorem mkContinuousLinear_norm_le (f : G →ₗ[𝕜] MultilinearMap 𝕜 E G') {C : ℝ} (hC : 0 ≤ C)
+    (H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖) : ‖mkContinuousLinear f C H‖ ≤ C :=
+  (mkContinuousLinear_norm_le' f C H).trans_eq (max_eq_left hC)
+
+variable [∀ i, SeminormedAddCommGroup (E' i)] [∀ i, NormedSpace 𝕜 (E' i)]
+
+/-- Given a map `f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)` and an estimate
+`H : ∀ m m', ‖f m m'‖ ≤ C * ∏ i, ‖m i‖ * ∏ i, ‖m' i‖`, upgrade all `MultilinearMap`s in the type to
+`ContinuousMultilinearMap`s. -/
+def mkContinuousMultilinear (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) (C : ℝ)
+    (H : ∀ m₁ m₂, ‖f m₁ m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖) :
+    ContinuousMultilinearMap 𝕜 E (ContinuousMultilinearMap 𝕜 E' G) :=
+  mkContinuous
+    { toFun := fun m => mkContinuous (f m) (C * ∏ i, ‖m i‖) <| H m
+      map_update_add' := fun m i x y => by
+        ext1
+        simp
+      map_update_smul' := fun m i c x => by
+        ext1
+        simp }
+    (max C 0) fun m => by
+      simp only [coe_mk]
+      refine ((f m).mkContinuous_norm_le' _).trans_eq ?_
+      rw [max_mul_of_nonneg, zero_mul]
+      positivity
+
+@[simp]
+theorem mkContinuousMultilinear_apply (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) {C : ℝ}
+    (H : ∀ m₁ m₂, ‖f m₁ m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖) (m : ∀ i, E i) :
+    ⇑(mkContinuousMultilinear f C H m) = f m :=
+  rfl
+
+theorem mkContinuousMultilinear_norm_le' (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) (C : ℝ)
+    (H : ∀ m₁ m₂, ‖f m₁ m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖) :
+    ‖mkContinuousMultilinear f C H‖ ≤ max C 0 := by
+  dsimp only [mkContinuousMultilinear]
+  exact mkContinuous_norm_le _ (le_max_right _ _) _
+
+theorem mkContinuousMultilinear_norm_le (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) {C : ℝ}
+    (hC : 0 ≤ C) (H : ∀ m₁ m₂, ‖f m₁ m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖) :
+    ‖mkContinuousMultilinear f C H‖ ≤ C :=
+  (mkContinuousMultilinear_norm_le' f C H).trans_eq (max_eq_left hC)
+
+end MultilinearMap
+
 namespace ContinuousLinearMap
 
 theorem norm_compContinuousMultilinearMap_le (g : G →L[𝕜] G') (f : ContinuousMultilinearMap 𝕜 E G) :
@@ -926,85 +1002,8 @@ theorem LinearIsometry.norm_compContinuousMultilinearMap (g : G →ₗᵢ[𝕜]
     LinearIsometry.coe_toContinuousLinearMap, LinearIsometry.norm_map,
     ContinuousMultilinearMap.norm_def, Function.comp_apply]
 
-open ContinuousMultilinearMap
-
-namespace MultilinearMap
-
-/-- Given a map `f : G →ₗ[𝕜] MultilinearMap 𝕜 E G'` and an estimate
-`H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖`, construct a continuous linear
-map from `G` to `ContinuousMultilinearMap 𝕜 E G'`.
-
-In order to lift, e.g., a map `f : (MultilinearMap 𝕜 E G) →ₗ[𝕜] MultilinearMap 𝕜 E' G'`
-to a map `(ContinuousMultilinearMap 𝕜 E G) →L[𝕜] ContinuousMultilinearMap 𝕜 E' G'`,
-one can apply this construction to `f.comp ContinuousMultilinearMap.toMultilinearMapLinear`
-which is a linear map from `ContinuousMultilinearMap 𝕜 E G` to `MultilinearMap 𝕜 E' G'`. -/
-def mkContinuousLinear (f : G →ₗ[𝕜] MultilinearMap 𝕜 E G') (C : ℝ)
-    (H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖) : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G' :=
-  LinearMap.mkContinuous
-    { toFun := fun x => (f x).mkContinuous (C * ‖x‖) <| H x
-      map_add' := fun x y => by
-        ext1
-        simp
-      map_smul' := fun c x => by
-        ext1
-        simp }
-    (max C 0) fun x => by
-      simpa using ((f x).mkContinuous_norm_le' _).trans_eq <| by
-        rw [max_mul_of_nonneg _ _ (norm_nonneg x), zero_mul]
-
-theorem mkContinuousLinear_norm_le' (f : G →ₗ[𝕜] MultilinearMap 𝕜 E G') (C : ℝ)
-    (H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖) : ‖mkContinuousLinear f C H‖ ≤ max C 0 := by
-  dsimp only [mkContinuousLinear]
-  exact LinearMap.mkContinuous_norm_le _ (le_max_right _ _) _
-
-theorem mkContinuousLinear_norm_le (f : G →ₗ[𝕜] MultilinearMap 𝕜 E G') {C : ℝ} (hC : 0 ≤ C)
-    (H : ∀ x m, ‖f x m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖) : ‖mkContinuousLinear f C H‖ ≤ C :=
-  (mkContinuousLinear_norm_le' f C H).trans_eq (max_eq_left hC)
-
-variable [∀ i, SeminormedAddCommGroup (E' i)] [∀ i, NormedSpace 𝕜 (E' i)]
-
-/-- Given a map `f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)` and an estimate
-`H : ∀ m m', ‖f m m'‖ ≤ C * ∏ i, ‖m i‖ * ∏ i, ‖m' i‖`, upgrade all `MultilinearMap`s in the type to
-`ContinuousMultilinearMap`s. -/
-def mkContinuousMultilinear (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) (C : ℝ)
-    (H : ∀ m₁ m₂, ‖f m₁ m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖) :
-    ContinuousMultilinearMap 𝕜 E (ContinuousMultilinearMap 𝕜 E' G) :=
-  mkContinuous
-    { toFun := fun m => mkContinuous (f m) (C * ∏ i, ‖m i‖) <| H m
-      map_update_add' := fun m i x y => by
-        ext1
-        simp
-      map_update_smul' := fun m i c x => by
-        ext1
-        simp }
-    (max C 0) fun m => by
-      simp only [coe_mk]
-      refine ((f m).mkContinuous_norm_le' _).trans_eq ?_
-      rw [max_mul_of_nonneg, zero_mul]
-      positivity
-
-@[simp]
-theorem mkContinuousMultilinear_apply (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) {C : ℝ}
-    (H : ∀ m₁ m₂, ‖f m₁ m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖) (m : ∀ i, E i) :
-    ⇑(mkContinuousMultilinear f C H m) = f m :=
-  rfl
-
-theorem mkContinuousMultilinear_norm_le' (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) (C : ℝ)
-    (H : ∀ m₁ m₂, ‖f m₁ m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖) :
-    ‖mkContinuousMultilinear f C H‖ ≤ max C 0 := by
-  dsimp only [mkContinuousMultilinear]
-  exact mkContinuous_norm_le _ (le_max_right _ _) _
-
-theorem mkContinuousMultilinear_norm_le (f : MultilinearMap 𝕜 E (MultilinearMap 𝕜 E' G)) {C : ℝ}
-    (hC : 0 ≤ C) (H : ∀ m₁ m₂, ‖f m₁ m₂‖ ≤ (C * ∏ i, ‖m₁ i‖) * ∏ i, ‖m₂ i‖) :
-    ‖mkContinuousMultilinear f C H‖ ≤ C :=
-  (mkContinuousMultilinear_norm_le' f C H).trans_eq (max_eq_left hC)
-
-end MultilinearMap
-
 namespace ContinuousMultilinearMap
 
-
 theorem norm_compContinuousLinearMap_le (g : ContinuousMultilinearMap 𝕜 E₁ G)
     (f : ∀ i, E i →L[𝕜] E₁ i) : ‖g.compContinuousLinearMap f‖ ≤ ‖g‖ * ∏ i, ‖f i‖ :=
   opNorm_le_bound (by positivity) fun m =>