feat: deriv versions of composition lemmas with bilinear maps (#11868)

We already have the `fderiv` versions.

Mathlib/Analysis/Calculus/Deriv/Mul.lean

@@ -36,12 +36,46 @@ open ContinuousLinearMap (smulRight smulRight_one_eq_iff)
 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
 variable {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
 variable {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+variable {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
 variable {f f₀ f₁ g : 𝕜 → F}
 variable {f' f₀' f₁' g' : F}
 variable {x : 𝕜}
 variable {s t : Set 𝕜}
 variable {L L₁ L₂ : Filter 𝕜}
 
+/-! ### Derivative of bilinear maps -/
+
+namespace ContinuousLinearMap
+
+variable {B : E →L[𝕜] F →L[𝕜] G} {u : 𝕜 → E} {v : 𝕜 → F} {u' : E} {v' : F}
+
+theorem hasDerivWithinAt_of_bilinear
+    (hu : HasDerivWithinAt u u' s x) (hv : HasDerivWithinAt v v' s x) :
+    HasDerivWithinAt (fun x ↦ B (u x) (v x)) (B (u x) v' + B u' (v x)) s x := by
+  simpa using (B.hasFDerivWithinAt_of_bilinear
+    hu.hasFDerivWithinAt hv.hasFDerivWithinAt).hasDerivWithinAt
+
+theorem hasDerivAt_of_bilinear (hu : HasDerivAt u u' x) (hv : HasDerivAt v v' x) :
+    HasDerivAt (fun x ↦ B (u x) (v x)) (B (u x) v' + B u' (v x)) x := by
+  simpa using (B.hasFDerivAt_of_bilinear hu.hasFDerivAt hv.hasFDerivAt).hasDerivAt
+
+theorem hasStrictDerivAt_of_bilinear (hu : HasStrictDerivAt u u' x) (hv : HasStrictDerivAt v v' x) :
+    HasStrictDerivAt (fun x ↦ B (u x) (v x)) (B (u x) v' + B u' (v x)) x := by
+  simpa using
+    (B.hasStrictFDerivAt_of_bilinear hu.hasStrictFDerivAt hv.hasStrictFDerivAt).hasStrictDerivAt
+
+theorem derivWithin_of_bilinear (hxs : UniqueDiffWithinAt 𝕜 s x)
+    (hu : DifferentiableWithinAt 𝕜 u s x) (hv : DifferentiableWithinAt 𝕜 v s x) :
+    derivWithin (fun y => B (u y) (v y)) s x =
+      B (u x) (derivWithin v s x) + B (derivWithin u s x) (v x) :=
+  (B.hasDerivWithinAt_of_bilinear hu.hasDerivWithinAt hv.hasDerivWithinAt).derivWithin hxs
+
+theorem deriv_of_bilinear (hu : DifferentiableAt 𝕜 u x) (hv : DifferentiableAt 𝕜 v x) :
+    deriv (fun y => B (u y) (v y)) x = B (u x) (deriv v x) + B (deriv u x) (v x) :=
+  (B.hasDerivAt_of_bilinear hu.hasDerivAt hv.hasDerivAt).deriv
+
+end ContinuousLinearMap
+
 section SMul
 
 /-! ### Derivative of the multiplication of a scalar function and a vector function -/

Mathlib/Analysis/Calculus/FDeriv/Bilinear.lean

@@ -138,6 +138,14 @@ theorem ContinuousLinearMap.hasFDerivAt_of_bilinear {f : G' → E} {g : G' → F
   (B.isBoundedBilinearMap.hasFDerivAt (f x, g x)).comp x (hf.prod hg)
 #align continuous_linear_map.has_fderiv_at_of_bilinear ContinuousLinearMap.hasFDerivAt_of_bilinear
 
+@[fun_prop]
+theorem ContinuousLinearMap.hasStrictFDerivAt_of_bilinear
+    {f : G' → E} {g : G' → F} {f' : G' →L[𝕜] E}
+    {g' : G' →L[𝕜] F} {x : G'} (hf : HasStrictFDerivAt f f' x) (hg : HasStrictFDerivAt g g' x) :
+    HasStrictFDerivAt (fun y => B (f y) (g y))
+      (B.precompR G' (f x) g' + B.precompL G' f' (g x)) x :=
+  (B.isBoundedBilinearMap.hasStrictFDerivAt (f x, g x)).comp x (hf.prod hg)
+
 theorem ContinuousLinearMap.fderivWithin_of_bilinear {f : G' → E} {g : G' → F} {x : G'} {s : Set G'}
     (hf : DifferentiableWithinAt 𝕜 f s x) (hg : DifferentiableWithinAt 𝕜 g s x)
     (hs : UniqueDiffWithinAt 𝕜 s x) :

Mathlib/Analysis/InnerProductSpace/Basic.lean

@@ -1821,6 +1821,11 @@ theorem innerSLFlip_apply (x y : E) : innerSLFlip 𝕜 x y = ⟪y, x⟫ :=
 set_option linter.uppercaseLean3 false in
 #align innerSL_flip_apply innerSLFlip_apply
 
+variable (F) in
+@[simp] lemma innerSL_real_flip : (innerSL ℝ (E := F)).flip = innerSL ℝ := by
+  ext v w
+  exact real_inner_comm _ _
+
 variable {𝕜}
 
 namespace ContinuousLinearMap

Mathlib/Analysis/NormedSpace/OperatorNorm/Bilinear.lean

@@ -364,6 +364,9 @@ def precompL (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) : (Eₗ →L[𝕜] E) →L[
   (precompR Eₗ (flip L)).flip
 #align continuous_linear_map.precompL ContinuousLinearMap.precompL
 
+@[simp] lemma precompL_apply (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) (u : Eₗ →L[𝕜] E) (f : Fₗ) (g : Eₗ) :
+    precompL Eₗ L u f g = L (u g) f := rfl
+
 theorem norm_precompR_le (L : E →L[𝕜] Fₗ →L[𝕜] Gₗ) :
     -- Porting note: added
     letI : SeminormedAddCommGroup ((Eₗ →L[𝕜] Fₗ) →L[𝕜] Eₗ →L[𝕜] Gₗ) := inferInstance