chore(linear_algebra/basic, analysis/normed_space/operator_norm): bundle another argument into the homs (#5899)

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

Author: eric-wieser

src/analysis/normed_space/operator_norm.lean

@@ -683,23 +683,19 @@ continuous_linear_map.homothety_norm _ c.norm_smul_right_apply
 
 variables (𝕜 F)
 
-/-- The linear map obtained by applying a continuous linear map at a given vector. -/
-def applyₗ (v : E) : (E →L[𝕜] F) →ₗ[𝕜] F :=
-{ to_fun := λ f, f v,
-  map_add' := λ f g, f.add_apply g v,
-  map_smul' := λ x f, f.smul_apply x v }
-
-lemma continuous_applyₗ (v : E) : continuous (continuous_linear_map.applyₗ 𝕜 F v) :=
-begin
-  apply (continuous_linear_map.applyₗ 𝕜 F v).continuous_of_bound,
-  intro f,
-  rw mul_comm,
-  exact f.le_op_norm v,
-end
-
-/-- The continuous linear map obtained by applying a continuous linear map at a given vector. -/
-def apply (v : E) : (E →L[𝕜] F) →L[𝕜] F :=
-⟨continuous_linear_map.applyₗ 𝕜 F v, continuous_linear_map.continuous_applyₗ _ _ _⟩
+/-- The continuous linear map obtained by applying a continuous linear map at a given vector.
+
+This is the continuous version of `linear_map.applyₗ`. -/
+def apply : E →L[𝕜] (E →L[𝕜] F) →L[𝕜] F :=
+linear_map.mk_continuous
+{ to_fun := λ v, linear_map.mk_continuous
+    { to_fun := λ f, f v,
+      map_add' := λ f g, f.add_apply g v,
+      map_smul' := λ x f, f.smul_apply x v }
+    ∥v∥ (λ f, by simpa [mul_comm] using f.le_op_norm v),
+  map_add' := λ _ _, ext $ λ f, f.map_add _ _,
+  map_smul' := λ _ _, ext $ λ f, f.map_smul _ _, }
+1 $ λ x, op_norm_le_bound _ (by simp) (λ f, by simpa [mul_comm] using f.le_op_norm x)
 
 variables {𝕜 F}
 

src/linear_algebra/basic.lean

@@ -330,11 +330,15 @@ variable (S)
 
 /-- Applying a linear map at `v : M`, seen as `S`-linear map from `M →ₗ[R] M₂` to `M₂`.
 
- See `applyₗ` for a version where `S = R` -/
-def applyₗ' (v : M) : (M →ₗ[R] M₂) →ₗ[S] M₂ :=
-{ to_fun := λ f, f v,
-  map_add' := λ f g, f.add_apply g v,
-  map_smul' := λ x f, f.smul_apply x v }
+ See `linear_map.applyₗ` for a version where `S = R`. -/
+@[simps]
+def applyₗ' : M →+ (M →ₗ[R] M₂) →ₗ[S] M₂ :=
+{ to_fun := λ v,
+  { to_fun := λ f, f v,
+    map_add' := λ f g, f.add_apply g v,
+    map_smul' := λ x f, f.smul_apply x v },
+  map_zero' := linear_map.ext $ λ f, f.map_zero,
+  map_add' := λ x y, linear_map.ext $ λ f, f.map_add _ _ }
 
 end semimodule
 
@@ -479,9 +483,14 @@ def comp_right (f : M₂ →ₗ[R] M₃) : (M →ₗ[R] M₂) →ₗ[R] (M →
 λ _ _, linear_map.ext $ λ _, f.3 _ _⟩
 
 /-- Applying a linear map at `v : M`, seen as a linear map from `M →ₗ[R] M₂` to `M₂`.
-See also `linear_map.applyₗ'` for a version that works with two different semirings. -/
-def applyₗ (v : M) : (M →ₗ[R] M₂) →ₗ[R] M₂ :=
-applyₗ' R v
+See also `linear_map.applyₗ'` for a version that works with two different semirings.
+
+This is the `linear_map` version of `add_monoid_hom.eval`. -/
+@[simps]
+def applyₗ : M →ₗ[R] (M →ₗ[R] M₂) →ₗ[R] M₂ :=
+{ to_fun := λ v, { to_fun := λ f, f v, ..applyₗ' R v },
+  map_smul' := λ x y, linear_map.ext $ λ f, f.map_smul _ _,
+  ..applyₗ' R }
 
 end comm_semiring