Derivatives of maps built from a continuous bilinear map

The quadratic map z ↦ B z z attached to a continuous bilinear map B : E →L[𝕜] E →L[𝕜] F is smooth, with derivative at y the polarization B.flip y + B y of B evaluated at y; since that derivative is linear in y, the second derivative is the constant continuous linear map B.flip + B. This is the derivative computation behind the local model of a nondegenerate critical point, but it depends on nothing beyond the bilinear chain rule ContinuousLinearMap.hasStrictFDerivAt_of_bilinear and the smoothness of bounded bilinear maps.

The same chain rule differentiates the pairing y ↦ B (u y) (∂_w u y) of a C² map u with one of its directional derivatives, the one-form x ↦ B x pulled back along u and evaluated in the direction w; its derivative involves the second derivative of u.

Main results

• ContinuousLinearMap.contDiff_apply_self: z ↦ B z z is C^n for every n, and its corollary ContinuousLinearMap.differentiable_apply_self.
• ContinuousLinearMap.hasStrictFDerivAt_apply_self: z ↦ B z z is strictly differentiable at y, with derivative the polarization of B evaluated at y.
• ContinuousLinearMap.hasFDerivAt_apply_self, and its fderiv form ContinuousLinearMap.fderiv_apply_self.
• ContinuousLinearMap.fderiv_fderiv_apply_self: the second derivative of z ↦ B z z is the constant B.flip + B.
• ContinuousLinearMap.hasFDerivAt_bilinear_fderiv_apply: the derivative of y ↦ B (u y) (∂_w u y) at a point where u is C².
• ContinuousLinearMap.contDiff_precomp_comp: the pullback (v, w) ↦ B (L v) (L w) of a continuous bilinear map B along a continuous linear map L depends smoothly on (B, L).

theorem ContinuousLinearMap.contDiff_apply_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} (B : E →L[𝕜] E →L[𝕜] F) : ContDiff 𝕜 n fun (z : E) => (B z) z

The map z ↦ B z z attached to a continuous bilinear map B is C^n for every n.

theorem ContinuousLinearMap.differentiable_apply_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (B : E →L[𝕜] E →L[𝕜] F) : Differentiable 𝕜 fun (z : E) => (B z) z

The map z ↦ B z z attached to a continuous bilinear map B is differentiable.

theorem ContinuousLinearMap.hasStrictFDerivAt_apply_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (B : E →L[𝕜] E →L[𝕜] F) (y : E) : HasStrictFDerivAt (fun (z : E) => (B z) z) (B.flip y + B y) y

The map z ↦ B z z attached to a continuous bilinear map B is strictly differentiable at y, with derivative the polarization of B evaluated at y.

theorem ContinuousLinearMap.hasFDerivAt_apply_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (B : E →L[𝕜] E →L[𝕜] F) (y : E) : HasFDerivAt (fun (z : E) => (B z) z) (B.flip y + B y) y

The map z ↦ B z z attached to a continuous bilinear map B is differentiable at y, with derivative the polarization of B evaluated at y.

@[simp]

theorem ContinuousLinearMap.fderiv_apply_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (B : E →L[𝕜] E →L[𝕜] F) (y : E) : fderiv 𝕜 (fun (z : E) => (B z) z) y = B.flip y + B y

At y, the differential of z ↦ B z z is B.flip y + B y.

@[simp]

theorem ContinuousLinearMap.fderiv_fderiv_apply_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (B : E →L[𝕜] E →L[𝕜] F) (y : E) : fderiv 𝕜 (fderiv 𝕜 fun (z : E) => (B z) z) y = B.flip + B

The second derivative of z ↦ B z z is the constant B.flip + B.

theorem ContinuousLinearMap.hasFDerivAt_bilinear_fderiv_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (B : F →L[𝕜] F →L[𝕜] G) {u : E → F} {z : E} (hu : ContDiffAt 𝕜 2 u z) (w : E) : HasFDerivAt (fun (y : E) => (B (u y)) ((fderiv 𝕜 u y) w)) (((precompR E B) (u z)) ((fderiv 𝕜 (fderiv 𝕜 u) z).flip w) + ((precompL E B) (fderiv 𝕜 u z)) ((fderiv 𝕜 u z) w)) z

The derivative of y ↦ B (u y) (∂_w u y) in the direction v, at a point where u is C², is B (u) (∂_v ∂_w u) + B (∂_v u) (∂_w u).

theorem ContinuousLinearMap.contDiff_precomp_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : WithTop ℕ∞} : ContDiff 𝕜 n fun (p : (F →L[𝕜] F →L[𝕜] G) × (E →L[𝕜] F)) => precomp G p.2 ∘SL p.1 ∘SL p.2

The pullback (v, w) ↦ B (L v) (L w) of a continuous bilinear map B along a continuous linear map L is C^n as a function of the pair (B, L).