feat: bundled versions of two operations on continuous multilinear ma…

…ps (#11775)

We provide versions of `smulRight` and `compContinuousLinearMap` as a continuous bilinear (resp multilinear) map.

Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

@@ -930,6 +930,21 @@ theorem norm_mkPiRing (z : G) : ‖ContinuousMultilinearMap.mkPiRing 𝕜 ι z
   rw [ContinuousMultilinearMap.mkPiRing, norm_smulRight, norm_mkPiAlgebra, one_mul]
 #align continuous_multilinear_map.norm_mk_pi_field ContinuousMultilinearMap.norm_mkPiRing
 
+variable (𝕜 E G) in
+/-- Continuous bilinear map realizing `(f, z) ↦ f.smulRight z`. -/
+def smulRightL : ContinuousMultilinearMap 𝕜 E 𝕜 →L[𝕜] G →L[𝕜] ContinuousMultilinearMap 𝕜 E G :=
+  LinearMap.mkContinuous₂
+    { toFun := fun f ↦
+        { toFun := fun z ↦ f.smulRight z
+          map_add' := fun x y ↦ by ext; simp
+          map_smul' := fun c x ↦ by ext; simp [smul_smul, mul_comm] }
+      map_add' := fun f g ↦ by ext; simp [add_smul]
+      map_smul' := fun c f ↦ by ext; simp [smul_smul] }
+    1 (fun f z ↦ by simp [norm_smulRight])
+
+@[simp] lemma smulRightL_apply (f : ContinuousMultilinearMap 𝕜 E 𝕜) (z : G) :
+  smulRightL 𝕜 E G f z = f.smulRight z := rfl
+
 variable (𝕜 ι G)
 
 /-- Continuous multilinear maps on `𝕜^n` with values in `G` are in bijection with `G`, as such a
@@ -1182,7 +1197,9 @@ theorem norm_compContinuous_linearIsometryEquiv (g : ContinuousMultilinearMap 
 This implementation fixes `f : Π i, E i →L[𝕜] E₁ i`.
 
 Actually, the map is multilinear in `f`,
-see `ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear`. -/
+see `ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear`.
+
+For a version fixing `g` and varying `f`, see `compContinuousLinearMapLRight`. -/
 def compContinuousLinearMapL (f : ∀ i, E i →L[𝕜] E₁ i) :
     ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G :=
   LinearMap.mkContinuous
@@ -1199,14 +1216,48 @@ theorem compContinuousLinearMapL_apply (g : ContinuousMultilinearMap 𝕜 E₁ G
   rfl
 #align continuous_multilinear_map.comp_continuous_linear_mapL_apply ContinuousMultilinearMap.compContinuousLinearMapL_apply
 
-variable (G)
-
+variable (G) in
 theorem norm_compContinuousLinearMapL_le (f : ∀ i, E i →L[𝕜] E₁ i) :
     ‖compContinuousLinearMapL (G := G) f‖ ≤ ∏ i, ‖f i‖ :=
   LinearMap.mkContinuous_norm_le _ (prod_nonneg fun _ _ => norm_nonneg _) _
 #align continuous_multilinear_map.norm_comp_continuous_linear_mapL_le ContinuousMultilinearMap.norm_compContinuousLinearMapL_le
 
-variable (𝕜 E E₁)
+/-- `ContinuousMultilinearMap.compContinuousLinearMap` as a bundled continuous linear map.
+This implementation fixes `g : ContinuousMultilinearMap 𝕜 E₁ G`.
+
+Actually, the map is linear in `g`,
+see `ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear`.
+
+For a version fixing `f` and varying `g`, see `compContinuousLinearMapL`. -/
+def compContinuousLinearMapLRight (g : ContinuousMultilinearMap 𝕜 E₁ G) :
+    ContinuousMultilinearMap 𝕜 (fun i ↦ E i →L[𝕜] E₁ i) (ContinuousMultilinearMap 𝕜 E G) :=
+  MultilinearMap.mkContinuous
+    { toFun := fun f => g.compContinuousLinearMap f
+      map_add' := by
+        intro h f i f₁ f₂
+        ext x
+        simp only [compContinuousLinearMap_apply, add_apply]
+        convert g.map_add (fun j ↦ f j (x j)) i (f₁ (x i)) (f₂ (x i)) <;>
+          exact apply_update (fun (i : ι) (f : E i →L[𝕜] E₁ i) ↦ f (x i)) f i _ _
+      map_smul' := by
+        intro h f i a f₀
+        ext x
+        simp only [compContinuousLinearMap_apply, smul_apply]
+        convert g.map_smul (fun j ↦ f j (x j)) i a (f₀ (x i)) <;>
+          exact apply_update (fun (i : ι) (f : E i →L[𝕜] E₁ i) ↦ f (x i)) f i _ _ }
+    (‖g‖) (fun f ↦ by simp [norm_compContinuousLinearMap_le])
+
+@[simp]
+theorem compContinuousLinearMapLRight_apply (g : ContinuousMultilinearMap 𝕜 E₁ G)
+    (f : ∀ i, E i →L[𝕜] E₁ i) : compContinuousLinearMapLRight g f = g.compContinuousLinearMap f :=
+  rfl
+
+variable (E) in
+theorem norm_compContinuousLinearMapLRight_le (g : ContinuousMultilinearMap 𝕜 E₁ G) :
+    ‖compContinuousLinearMapLRight (E := E) g‖ ≤ ‖g‖ :=
+  MultilinearMap.mkContinuous_norm_le _ (norm_nonneg _) _
+
+variable (𝕜 E E₁ G)
 
 open Function in
 /-- If `f` is a collection of continuous linear maps, then the construction
@@ -1356,7 +1407,7 @@ open Topology Filter
 
 /-- If the target space is complete, the space of continuous multilinear maps with its norm is also
 complete. The proof is essentially the same as for the space of continuous linear maps (modulo the
-addition of `Finset.prod` where needed. The duplication could be avoided by deducing the linear
+addition of `Finset.prod` where needed). The duplication could be avoided by deducing the linear
 case from the multilinear case via a currying isomorphism. However, this would mess up imports,
 and it is more satisfactory to have the simplest case as a standalone proof. -/
 instance completeSpace [CompleteSpace G] : CompleteSpace (ContinuousMultilinearMap 𝕜 E G) := by

Mathlib/Topology/Algebra/Module/StrongTopology.lean

@@ -307,6 +307,9 @@ variable {𝕜 : Type*} [NormedField 𝕜] {E F G : Type*}
 /-- Send a continuous bilinear map to an abstract bilinear map (forgetting continuity). -/
 def toLinearMap₂ (L : E →L[𝕜] F →L[𝕜] G) : E →ₗ[𝕜] F →ₗ[𝕜] G := (coeLM 𝕜).comp L.toLinearMap
 
+@[simp] lemma toLinearMap₂_apply (L : E →L[𝕜] F →L[𝕜] G) (v : E) (w : F) :
+    L.toLinearMap₂ v w = L v w := rfl
+
 end BilinearMaps
 
 end ContinuousLinearMap

scripts/style-exceptions.txt

@@ -10,6 +10,7 @@ Mathlib/Analysis/Calculus/ContDiff/Defs.lean : line 1 : ERR_NUM_LIN : 1900 file
 Mathlib/Analysis/Convolution.lean : line 1 : ERR_NUM_LIN : 1700 file contains 1545 lines, try to split it up
 Mathlib/Analysis/InnerProductSpace/Basic.lean : line 1 : ERR_NUM_LIN : 2500 file contains 2358 lines, try to split it up
 Mathlib/Analysis/Normed/Group/Basic.lean : line 1 : ERR_NUM_LIN : 3000 file contains 2815 lines, try to split it up
+Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean : line 1 : ERR_NUM_LIN : 1700 file contains 1511 lines, try to split it up
 Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean : line 1 : ERR_NUM_LIN : 2300 file contains 2118 lines, try to split it up
 Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean : line 1 : ERR_NUM_LIN : 2900 file contains 2728 lines, try to split it up
 Mathlib/Combinatorics/SimpleGraph/Connectivity.lean : line 1 : ERR_NUM_LIN : 2800 file contains 2653 lines, try to split it up