Second derivatives along a line

Mathlib's DifferentiableAt.deriv_comp_add_smul computes the derivative of the restriction s ↦ f (x + s • y) of a function to a line. This file records the second derivative: it is the diagonal entry fderiv 𝕜 (fderiv 𝕜 f) (x + t • y) y y of the Hessian.

Main results

• ContDiffAt.deriv_deriv_comp_add_smul: the second derivative of s ↦ f (x + s • y) at t is fderiv 𝕜 (fderiv 𝕜 f) (x + t • y) y y, for f of class C² at x + t • y.

theorem ContDiffAt.deriv_deriv_comp_add_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x y : E} {t : 𝕜} (hf : ContDiffAt 𝕜 2 f (x + t • y)) : deriv (deriv fun (s : 𝕜) => f (x + s • y)) t = ((fderiv 𝕜 (fderiv 𝕜 f) (x + t • y)) y) y

The second derivative of the restriction s ↦ f (x + s • y) of a C² function to a line is the diagonal Hessian entry fderiv 𝕜 (fderiv 𝕜 f) (x + t • y) y y.