feat(analysis/normed_space/operator_norm): bundle more arguments (#6207)

* Drop `lmul_left` in favor of a partially applied `lmul`.
* Use `lmul_left_right` in `has_fderiv_at_ring_inverse` and related lemmas.
* Add bundled `compL`, `lmulₗᵢ`, `lsmul`.
* Make `𝕜` argument in `of_homothety` implicit.
* Add `deriv₂` and `bilinear_comp`.



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

Author: urkud

src/analysis/analytic/linear.lean

@@ -15,6 +15,7 @@ the formal power series `f x = f a + f (x - a)`.
 variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
 {E : Type*} [normed_group E] [normed_space 𝕜 E]
 {F : Type*} [normed_group F] [normed_space 𝕜 F]
+{G : Type*} [normed_group G] [normed_space 𝕜 G]
 
 open_locale topological_space classical big_operators nnreal ennreal
 open set filter asymptotics
@@ -50,4 +51,48 @@ protected theorem has_fpower_series_at (f : E →L[𝕜] F) (x : E) :
 protected theorem analytic_at (f : E →L[𝕜] F) (x : E) : analytic_at 𝕜 f x :=
 (f.has_fpower_series_at x).analytic_at
 
+/-- Reinterpret a bilinear map `f : E →L[𝕜] F →L[𝕜] G` as a multilinear map
+`(E × F) [×2]→L[𝕜] G`. This multilinear map is the second term in the formal
+multilinear series expansion of `uncurry f`. It is given by
+`f.uncurry_bilinear ![(x, y), (x', y')] = f x y'`. -/
+def uncurry_bilinear (f : E →L[𝕜] F →L[𝕜] G) : (E × F) [×2]→L[𝕜] G :=
+@continuous_linear_map.uncurry_left 𝕜 1 (λ _, E × F) G _ _ _ _ _ $
+  (↑(continuous_multilinear_curry_fin1 𝕜 (E × F) G).symm : (E × F →L[𝕜] G) →L[𝕜] _).comp $
+    f.bilinear_comp (fst _ _ _) (snd _ _ _)
+
+@[simp] lemma uncurry_bilinear_apply (f : E →L[𝕜] F →L[𝕜] G) (m : fin 2 → E × F) :
+  f.uncurry_bilinear m = f (m 0).1 (m 1).2 :=
+rfl
+
+/-- Formal multilinear series expansion of a bilinear function `f : E →L[𝕜] F →L[𝕜] G`. -/
+@[simp] def fpower_series_bilinear (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
+  formal_multilinear_series 𝕜 (E × F) G
+| 0 := continuous_multilinear_map.curry0 𝕜 _ (f x.1 x.2)
+| 1 := (continuous_multilinear_curry_fin1 𝕜 (E × F) G).symm (f.deriv₂ x)
+| 2 := f.uncurry_bilinear
+| _ := 0
+
+@[simp] lemma fpower_series_bilinear_radius (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
+  (f.fpower_series_bilinear x).radius = ∞ :=
+(f.fpower_series_bilinear x).radius_eq_top_of_forall_image_add_eq_zero 3 $ λ n, rfl
+
+protected theorem has_fpower_series_on_ball_bilinear (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
+  has_fpower_series_on_ball (λ x : E × F, f x.1 x.2) (f.fpower_series_bilinear x) x ∞ :=
+{ r_le := by simp,
+  r_pos := ennreal.coe_lt_top,
+  has_sum := λ y _, (has_sum_nat_add_iff' 3).1 $
+    begin
+      simp only [finset.sum_range_succ, finset.sum_range_one, prod.fst_add, prod.snd_add,
+        f.map_add₂],
+      dsimp, simp only [add_comm, add_left_comm, sub_self, has_sum_zero]
+    end }
+
+protected theorem has_fpower_series_at_bilinear (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
+  has_fpower_series_at (λ x : E × F, f x.1 x.2) (f.fpower_series_bilinear x) x :=
+⟨∞, f.has_fpower_series_on_ball_bilinear x⟩
+
+protected theorem analytic_at_bilinear (f : E →L[𝕜] F →L[𝕜] G) (x : E × F) :
+  analytic_at 𝕜 (λ x : E × F, f x.1 x.2) x :=
+(f.has_fpower_series_at_bilinear x).analytic_at
+
 end continuous_linear_map

src/analysis/calculus/fderiv.lean

@@ -2379,7 +2379,7 @@ open normed_ring continuous_linear_map ring
 /-- At an invertible element `x` of a normed algebra `R`, the Fréchet derivative of the inversion
 operation is the linear map `λ t, - x⁻¹ * t * x⁻¹`. -/
 lemma has_fderiv_at_ring_inverse (x : units R) :
-  has_fderiv_at ring.inverse (- (lmul_right 𝕜 R ↑x⁻¹).comp (lmul_left 𝕜 R ↑x⁻¹)) x :=
+  has_fderiv_at ring.inverse (-lmul_left_right 𝕜 R ↑x⁻¹ ↑x⁻¹) x :=
 begin
   have h_is_o : is_o (λ (t : R), inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹)
     (λ (t : R), t) (𝓝 0),
@@ -2394,16 +2394,15 @@ begin
   simp only [has_fderiv_at, has_fderiv_at_filter],
   convert h_is_o.comp_tendsto h_lim,
   ext y,
-  simp only [coe_comp', function.comp_app, lmul_right_apply, lmul_left_apply, neg_apply,
-    inverse_unit x, units.inv_mul, add_sub_cancel'_right, mul_sub, sub_mul, one_mul],
-  abel
+  simp only [coe_comp', function.comp_app, lmul_left_right_apply, neg_apply, inverse_unit x,
+    units.inv_mul, add_sub_cancel'_right, mul_sub, sub_mul, one_mul, sub_neg_eq_add]
 end
 
 lemma differentiable_at_inverse (x : units R) : differentiable_at 𝕜 (@ring.inverse R _) x :=
 (has_fderiv_at_ring_inverse x).differentiable_at
 
 lemma fderiv_inverse (x : units R) :
-  fderiv 𝕜 (@ring.inverse R _) x = - (lmul_right 𝕜 R ↑x⁻¹).comp (lmul_left 𝕜 R ↑x⁻¹) :=
+  fderiv 𝕜 (@ring.inverse R _) x = - lmul_left_right 𝕜 R ↑x⁻¹ ↑x⁻¹ :=
 (has_fderiv_at_ring_inverse x).fderiv
 
 end algebra_inverse

src/analysis/calculus/times_cont_diff.lean

@@ -2386,18 +2386,16 @@ begin
     { use (ftaylor_series_within 𝕜 inverse univ),
       rw [le_antisymm hm bot_le, has_ftaylor_series_up_to_on_zero_iff],
       split,
-      { rintros _ ⟨x', hx'⟩,
-        rw ← hx',
+      { rintros _ ⟨x', rfl⟩,
         exact (inverse_continuous_at x').continuous_within_at },
       { simp [ftaylor_series_within] } } },
   { apply times_cont_diff_at_succ_iff_has_fderiv_at.mpr,
-    refine ⟨λ (x : R), - lmul_left_right 𝕜 R (inverse x, inverse x), _, _⟩,
+    refine ⟨λ (x : R), - lmul_left_right 𝕜 R (inverse x) (inverse x), _, _⟩,
     { refine ⟨{y : R | is_unit y}, x.nhds, _⟩,
-      intros y hy,
-      cases mem_set_of_eq.mp hy with y' hy',
-      rw [← hy', inverse_unit],
-      exact @has_fderiv_at_ring_inverse 𝕜 _ _ _ _ _ y' },
-    { exact (lmul_left_right_is_bounded_bilinear 𝕜 R).times_cont_diff.neg.comp_times_cont_diff_at
+      rintros _ ⟨y, rfl⟩,
+      rw [inverse_unit],
+      exact has_fderiv_at_ring_inverse y },
+    { convert (lmul_left_right_is_bounded_bilinear 𝕜 R).times_cont_diff.neg.comp_times_cont_diff_at
         (x : R) (IH.prod IH) } },
   { exact times_cont_diff_at_top.mpr Itop }
 end

src/analysis/normed_space/bounded_linear_maps.lean

@@ -201,6 +201,16 @@ structure is_bounded_bilinear_map (f : E × F → G) : Prop :=
 variable {𝕜}
 variable {f : E × F → G}
 
+lemma continuous_linear_map.is_bounded_bilinear_map (f : E →L[𝕜] F →L[𝕜] G) :
+  is_bounded_bilinear_map 𝕜 (λ x : E × F, f x.1 x.2) :=
+{ add_left := λ x₁ x₂ y, by rw [f.map_add, continuous_linear_map.add_apply],
+  smul_left := λ c x y, by rw [f.map_smul _, continuous_linear_map.smul_apply],
+  add_right := λ x, (f x).map_add,
+  smul_right := λ c x y, (f x).map_smul c y,
+  bound := ⟨max ∥f∥ 1, zero_lt_one.trans_le (le_max_right _ _),
+    λ x y, (f.le_op_norm₂ x y).trans $
+      by apply_rules [mul_le_mul_of_nonneg_right, norm_nonneg, le_max_left]⟩ }
+
 protected lemma is_bounded_bilinear_map.is_O (h : is_bounded_bilinear_map 𝕜 f) :
   asymptotics.is_O f (λ p : E × F, ∥p.1∥ * ∥p.2∥) ⊤ :=
 let ⟨C, Cpos, hC⟩ := h.bound in asymptotics.is_O.of_bound _ $
@@ -379,17 +389,8 @@ variables (𝕜)
 /-- The function `lmul_left_right : 𝕜' × 𝕜' → (𝕜' →L[𝕜] 𝕜')` is a bounded bilinear map. -/
 lemma continuous_linear_map.lmul_left_right_is_bounded_bilinear
   (𝕜' : Type*) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜'] :
-  is_bounded_bilinear_map 𝕜 (continuous_linear_map.lmul_left_right 𝕜 𝕜') :=
-{ add_left := λ v₁ v₂ w, by {ext t, simp [add_comm, add_mul]},
-  smul_left := λ c v w, by {ext, simp },
-  add_right := λ v w₁ w₂, by {ext t, simp [add_comm, mul_add]},
-  smul_right := λ c v w, by {ext, simp },
-  bound := begin
-    refine ⟨1, by linarith, _⟩,
-    intros v w,
-    rw one_mul,
-    apply continuous_linear_map.lmul_left_right_norm_le,
-  end }
+  is_bounded_bilinear_map 𝕜 (λ p : 𝕜' × 𝕜', continuous_linear_map.lmul_left_right 𝕜 𝕜' p.1 p.2) :=
+(continuous_linear_map.lmul_left_right 𝕜 𝕜').is_bounded_bilinear_map
 
 variables {𝕜}
 
@@ -420,6 +421,6 @@ by { simp_rw [←dist_zero_right, ←f.map_zero], exact isometry.dist_eq hf _ _
 /-- Construct a continuous linear equiv from a linear map that is also an isometry with full range. -/
 def continuous_linear_equiv.of_isometry (f : E →ₗ[𝕜] F) (hf : isometry f) (hfr : f.range = ⊤) :
   E ≃L[𝕜] F :=
-continuous_linear_equiv.of_homothety 𝕜
+continuous_linear_equiv.of_homothety
 (linear_equiv.of_bijective f (linear_map.ker_eq_bot.mpr (isometry.injective hf)) hfr)
 1 zero_lt_one (λ _, by simp [one_mul, f.norm_apply_of_isometry hf])

src/analysis/normed_space/operator_norm.lean

@@ -7,6 +7,7 @@ import linear_algebra.finite_dimensional
 import analysis.normed_space.linear_isometry
 import analysis.normed_space.riesz_lemma
 import analysis.asymptotics.asymptotics
+import algebra.algebra.tower
 
 /-!
 # Operator norm on the space of continuous linear maps
@@ -755,6 +756,8 @@ private lemma le_norm_flip (f : E →L[𝕜] F →L[𝕜] G) : ∥f∥ ≤ ∥fl
 f.op_norm_le_bound₂ (norm_nonneg _) $ λ x y,
   by { rw mul_right_comm, exact (flip f).le_op_norm₂ y x }
 
+@[simp] lemma flip_apply (f : E →L[𝕜] F →L[𝕜] G) (x : E) (y : F) : f.flip y x = f x y := rfl
+
 @[simp] lemma flip_flip (f : E →L[𝕜] F →L[𝕜] G) :
   f.flip.flip = f :=
 by { ext, refl }
@@ -802,31 +805,99 @@ variables {𝕜 F}
 
 @[simp] lemma apply_apply (v : E) (f : E →L[𝕜] F) : apply 𝕜 F v f = f v := rfl
 
+variables (𝕜 E F G)
+
+/-- Composition of continuous linear maps as a continuous bilinear map. -/
+def compL : (F →L[𝕜] G) →L[𝕜] (E →L[𝕜] F) →L[𝕜] (E →L[𝕜] G) :=
+linear_map.mk_continuous₂
+  (linear_map.mk₂ _ comp add_comp smul_comp comp_add (λ c f g, comp_smul _ _ _))
+  1 $ λ f g, by simpa only [one_mul] using op_norm_comp_le f g
+
+variables {𝕜 E F G}
+
+@[simp] lemma compL_apply (f : F →L[𝕜] G) (g : E →L[𝕜] F) : compL 𝕜 E F G f g = f.comp g := rfl
+
 section multiplication_linear
 variables (𝕜) (𝕜' : Type*) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜']
 
-/-- Left-multiplication in a normed algebra, considered as a continuous linear map. -/
-def lmul_left : 𝕜' → (𝕜' →L[𝕜] 𝕜') :=
-λ x, (algebra.lmul_left 𝕜 x).mk_continuous ∥x∥
-(λ y, by {rw algebra.lmul_left_apply, exact norm_mul_le x y})
+/-- Left multiplication in a normed algebra as a linear isometry to the space of
+continuous linear maps. -/
+def lmulₗᵢ : 𝕜' →ₗᵢ[𝕜] 𝕜' →L[𝕜] 𝕜' :=
+{ to_linear_map := (algebra.lmul 𝕜 𝕜').to_linear_map.mk_continuous₂ 1 $
+    λ x y, by simpa using norm_mul_le x y,
+  norm_map' := λ x, le_antisymm
+    (op_norm_le_bound _ (norm_nonneg x) (norm_mul_le x))
+    (by { convert ratio_le_op_norm _ (1 : 𝕜'), simp [normed_algebra.norm_one 𝕜 𝕜'] }) }
+
+/-- Left multiplication in a normed algebra as a continuous bilinear map. -/
+def lmul : 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' :=
+(lmulₗᵢ 𝕜 𝕜').to_continuous_linear_map
+
+@[simp] lemma lmul_apply (x y : 𝕜') : lmul 𝕜 𝕜' x y = x * y := rfl
+
+@[simp] lemma coe_lmulₗᵢ : ⇑(lmulₗᵢ 𝕜 𝕜') = lmul 𝕜 𝕜' := rfl
+
+@[simp] lemma op_norm_lmul_apply (x : 𝕜') : ∥lmul 𝕜 𝕜' x∥ = ∥x∥ :=
+(lmulₗᵢ 𝕜 𝕜').norm_map x
+
+@[simp] lemma op_norm_lmul : ∥lmul 𝕜 𝕜'∥ = 1 :=
+by haveI := normed_algebra.nontrivial 𝕜 𝕜'; exact (lmulₗᵢ 𝕜 𝕜').norm_to_continuous_linear_map
 
 /-- Right-multiplication in a normed algebra, considered as a continuous linear map. -/
-def lmul_right : 𝕜' → (𝕜' →L[𝕜] 𝕜') :=
-λ x, (algebra.lmul_right 𝕜 x).mk_continuous ∥x∥
-(λ y, by {rw [algebra.lmul_right_apply, mul_comm], exact norm_mul_le y x})
+def lmul_right : 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' := (lmul 𝕜 𝕜').flip
+
+@[simp] lemma lmul_right_apply (x y : 𝕜') : lmul_right 𝕜 𝕜' x y = y * x := rfl
+
+@[simp] lemma op_norm_lmul_right_apply (x : 𝕜') : ∥lmul_right 𝕜 𝕜' x∥ = ∥x∥ :=
+le_antisymm
+  (op_norm_le_bound _ (norm_nonneg x) (λ y, (norm_mul_le y x).trans_eq (mul_comm _ _)))
+  (by { convert ratio_le_op_norm _ (1 : 𝕜'), simp [normed_algebra.norm_one 𝕜 𝕜'] })
+
+@[simp] lemma op_norm_lmul_right : ∥lmul_right 𝕜 𝕜'∥ = 1 :=
+(op_norm_flip (lmul 𝕜 𝕜')).trans $ op_norm_lmul _ _
+
+/-- Right-multiplication in a normed algebra, considered as a linear isometry to the space of
+continuous linear maps. -/
+def lmul_rightₗᵢ : 𝕜' →ₗᵢ[𝕜] 𝕜' →L[𝕜] 𝕜' :=
+{ to_linear_map := lmul_right 𝕜 𝕜',
+  norm_map' := op_norm_lmul_right_apply 𝕜 𝕜' }
+
+@[simp] lemma coe_lmul_rightₗᵢ : ⇑(lmul_rightₗᵢ 𝕜 𝕜') = lmul_right 𝕜 𝕜' := rfl
 
 /-- Simultaneous left- and right-multiplication in a normed algebra, considered as a continuous
-linear map. -/
-def lmul_left_right (vw : 𝕜' × 𝕜') : 𝕜' →L[𝕜] 𝕜' :=
-(lmul_right 𝕜 𝕜' vw.2).comp (lmul_left 𝕜 𝕜' vw.1)
+trilinear map. -/
+def lmul_left_right : 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' →L[𝕜] 𝕜' :=
+((compL 𝕜 𝕜' 𝕜' 𝕜').comp (lmul_right 𝕜 𝕜')).flip.comp (lmul 𝕜 𝕜')
 
-@[simp] lemma lmul_left_apply (x y : 𝕜') : lmul_left 𝕜 𝕜' x y = x * y := rfl
-@[simp] lemma lmul_right_apply (x y : 𝕜') : lmul_right 𝕜 𝕜' x y = y * x := rfl
-@[simp] lemma lmul_left_right_apply (vw : 𝕜' × 𝕜') (x : 𝕜') :
-  lmul_left_right 𝕜 𝕜' vw x = vw.1 * x * vw.2 := rfl
+@[simp] lemma lmul_left_right_apply (x y z : 𝕜') :
+  lmul_left_right 𝕜 𝕜' x y z = x * z * y := rfl
+
+lemma op_norm_lmul_left_right_apply_apply_le (x y : 𝕜') :
+  ∥lmul_left_right 𝕜 𝕜' x y∥ ≤ ∥x∥ * ∥y∥ :=
+(op_norm_comp_le _ _).trans_eq $ by simp [mul_comm]
+
+lemma op_norm_lmul_left_right_apply_le (x : 𝕜') :
+  ∥lmul_left_right 𝕜 𝕜' x∥ ≤ ∥x∥ :=
+op_norm_le_bound _ (norm_nonneg x) (op_norm_lmul_left_right_apply_apply_le 𝕜 𝕜' x)
+
+lemma op_norm_lmul_left_right_le :
+  ∥lmul_left_right 𝕜 𝕜'∥ ≤ 1 :=
+op_norm_le_bound _ zero_le_one (λ x, (one_mul ∥x∥).symm ▸ op_norm_lmul_left_right_apply_le 𝕜 𝕜' x)
 
 end multiplication_linear
 
+section smul_linear
+
+variables (𝕜) (𝕜' : Type*) [normed_field 𝕜'] [normed_algebra 𝕜 𝕜']
+  [normed_space 𝕜' E] [is_scalar_tower 𝕜 𝕜' E]
+
+/-- Scalar multiplication as a continuous bilinear map. -/
+def lsmul : 𝕜' →L[𝕜] E →L[𝕜] E :=
+((algebra.lsmul 𝕜 E).to_linear_map : 𝕜' →ₗ[𝕜] E →ₗ[𝕜] E).mk_continuous₂ 1 $
+  λ c x, by simpa only [one_mul] using (norm_smul c x).le
+
+end smul_linear
+
 section restrict_scalars
 
 variables {𝕜' : Type*} [nondiscrete_normed_field 𝕜'] [normed_algebra 𝕜' 𝕜]
@@ -1004,23 +1075,23 @@ begin
   rw [← mul_assoc, inv_mul_cancel (ne_of_lt ha).symm, one_mul],
 end
 
-variable (𝕜)
-
 /-- A linear equivalence which is a homothety is a continuous linear equivalence. -/
 def of_homothety (f : E ≃ₗ[𝕜] F) (a : ℝ) (ha : 0 < a) (hf : ∀x, ∥f x∥ = a * ∥x∥) : E ≃L[𝕜] F :=
 { to_linear_equiv := f,
   continuous_to_fun := f.to_linear_map.continuous_of_bound a (λ x, le_of_eq (hf x)),
   continuous_inv_fun := f.symm.to_linear_map.continuous_of_bound a⁻¹
     (λ x, le_of_eq (homothety_inverse a ha f hf x)) }
 
+variable (𝕜)
+
 lemma to_span_nonzero_singleton_homothety (x : E) (h : x ≠ 0) (c : 𝕜) :
   ∥linear_equiv.to_span_nonzero_singleton 𝕜 E x h c∥ = ∥x∥ * ∥c∥ :=
 continuous_linear_map.to_span_singleton_homothety _ _ _
 
 /-- Given a nonzero element `x` of a normed space `E` over a field `𝕜`, the natural
     continuous linear equivalence from `E` to the span of `x`.-/
 def to_span_nonzero_singleton (x : E) (h : x ≠ 0) : 𝕜 ≃L[𝕜] (𝕜 ∙ x) :=
-of_homothety 𝕜
+of_homothety
   (linear_equiv.to_span_nonzero_singleton 𝕜 E x h)
   ∥x∥
   (norm_pos_iff.mpr h)
@@ -1073,22 +1144,29 @@ def linear_equiv.to_continuous_linear_equiv_of_bounds (e : E ≃ₗ[𝕜] F) (C_
 namespace continuous_linear_map
 variables (𝕜) (𝕜' : Type*) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜']
 
-@[simp] lemma lmul_left_norm (v : 𝕜') : ∥lmul_left 𝕜 𝕜' v∥ = ∥v∥ :=
-begin
-  refine le_antisymm _ _,
-  { exact linear_map.mk_continuous_norm_le _ (norm_nonneg v) _ },
-  { simpa [normed_algebra.norm_one 𝕜 𝕜'] using le_op_norm (lmul_left 𝕜 𝕜' v) (1:𝕜') }
-end
+variables {𝕜}
 
-@[simp] lemma lmul_right_norm (v : 𝕜') : ∥lmul_right 𝕜 𝕜' v∥ = ∥v∥ :=
-begin
-  refine le_antisymm _ _,
-  { exact linear_map.mk_continuous_norm_le _ (norm_nonneg v) _ },
-  { simpa [normed_algebra.norm_one 𝕜 𝕜'] using le_op_norm (lmul_right 𝕜 𝕜' v) (1:𝕜') }
-end
+variables {E' F' : Type*} [normed_group E'] [normed_group F'] [normed_space 𝕜 E'] [normed_space 𝕜 F']
+
+/-- Compose a bilinear map `E →L[𝕜] F →L[𝕜] G` with two linear maps `E' →L[𝕜] E` and `F' →L[𝕜] F`. -/
+def bilinear_comp (f : E →L[𝕜] F →L[𝕜] G) (gE : E' →L[𝕜] E) (gF : F' →L[𝕜] F) : E' →L[𝕜] F' →L[𝕜] G :=
+((f.comp gE).flip.comp gF).flip
+
+@[simp] lemma bilinear_comp_apply (f : E →L[𝕜] F →L[𝕜] G) (gE : E' →L[𝕜] E) (gF : F' →L[𝕜] F)
+  (x : E') (y : F') :
+  f.bilinear_comp gE gF x y = f (gE x) (gF y) :=
+rfl
+
+/-- Derivative of a continuous bilinear map `f : E →L[𝕜] F →L[𝕜] G` interpreted as a map `E × F → G`
+at point `p : E × F` evaluated at `q : E × F`, as a continuous bilinear map. -/
+def deriv₂ (f : E →L[𝕜] F →L[𝕜] G) : (E × F) →L[𝕜] (E × F) →L[𝕜] G :=
+f.bilinear_comp (fst _ _ _) (snd _ _ _) + f.flip.bilinear_comp (snd _ _ _) (fst _ _ _)
+
+@[simp] lemma coe_deriv₂ (f : E →L[𝕜] F →L[𝕜] G) (p : E × F) :
+  ⇑(f.deriv₂ p) = λ q : E × F, f p.1 q.2 + f q.1 p.2 := rfl
 
-lemma lmul_left_right_norm_le (vw : 𝕜' × 𝕜') :
-  ∥lmul_left_right 𝕜 𝕜' vw∥ ≤ ∥vw.1∥ * ∥vw.2∥ :=
-by simpa [mul_comm] using op_norm_comp_le (lmul_right 𝕜 𝕜' vw.2) (lmul_left 𝕜 𝕜' vw.1)
+lemma map_add₂ (f : E →L[𝕜] F →L[𝕜] G) (x x' : E) (y y' : F) :
+  f (x + x') (y + y') = f x y + f.deriv₂ (x, y) (x', y') + f x' y' :=
+by simp only [map_add, add_apply, coe_deriv₂, add_assoc]
 
 end continuous_linear_map