The second derivative as a derivative

The second derivative fderiv 𝕜 (fderiv 𝕜 g) x of a map between normed spaces is, by definition, the derivative at x of the map fderiv 𝕜 g. Mathlib supplies the differentiability of fderiv 𝕜 g at a twice continuously differentiable point through ContDiffAt.fderiv_right; this file packages that into the single HasFDerivAt statement that second-order arguments use, so that the identification is made once rather than at each use.

An invertible second derivative therefore lets the differential avoid any prescribed value c on some punctured neighbourhood of the point, the neighbourhood being allowed to depend on c. That fixed-value avoidance is the local rigidity behind the isolation of nondegenerate critical points, and it asks nothing of the value taken.

The file also records that on an open set the second directional derivative x ↦ D(Dg(·) v)(x) v of a C² map is continuous, and the second-order chain rule D²(f ∘ φ)(v, w) = D²f(Dφ v, Dφ w) + Df(D²φ(v, w)). At a point where the differential of the outer function vanishes the first-order term drops out, so the second derivative of a composition is the second derivative of the outer function evaluated on the images of the differential of the inner one, i.e. the second derivative transforms as a bilinear form. The second derivative of a separated sum φ ∘ Prod.fst + ψ ∘ Prod.snd on a product is the block-diagonal map built from the second derivatives of the summands. Finally, the second derivative of a directional derivative y ↦ Dg(y) v is the third derivative of g evaluated at v, and differentiating the symmetry of the second derivative shows that the third derivative is symmetric in its last two directions. No statement here mentions critical points as such, so all of them belong here rather than with the Morse theory that uses them.

Main results

• ContDiffAt.hasFDerivAt_fderiv: at a twice continuously differentiable point, fderiv 𝕜 g is differentiable, with derivative the second derivative of g.
• ContDiffOn.continuousOn_fderiv_fderiv_apply: on an open set, the second directional derivative of a C² map in a fixed direction is continuous.
• TauCeti.eventually_fderiv_ne: where the second derivative is invertible, the differential avoids any prescribed value on a punctured neighbourhood of the point.
• TauCeti.fderiv_fderiv_comp_apply: the second-order chain rule for C² maps.
• TauCeti.fderiv_fderiv_comp_apply_of_fderiv_eq_zero: for C² maps, where the differential of the outer function vanishes, the second derivative of a composition is the pullback of the second derivative along the differential of the inner function.
• TauCeti.fderiv_fderiv_comp_fst_add_comp_snd: the second derivative of a separated sum on a product is block diagonal.
• TauCeti.fderiv_fderiv_fderiv_apply: the second derivative of a directional derivative of a C³ map is its third derivative.
• TauCeti.fderiv_fderiv_fderiv_apply_comm: the third derivative of a sufficiently smooth map is symmetric in its last two directions.

theorem ContDiffAt.hasFDerivAt_fderiv {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {g : E → F} {x : E} (h : ContDiffAt 𝕜 n g x) (hn : 2 ≤ n) : HasFDerivAt (fderiv 𝕜 g) (fderiv 𝕜 (fderiv 𝕜 g) x) x

At a twice continuously differentiable point, fderiv 𝕜 g is differentiable, with derivative the second derivative of g.

theorem ContDiffOn.continuousOn_fderiv_fderiv_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {g : E → F} {s : Set E} (hg : ContDiffOn 𝕜 2 g s) (hs : IsOpen s) (v : E) : ContinuousOn (fun (x : E) => (fderiv 𝕜 (fun (y : E) => (fderiv 𝕜 g y) v) x) v) s

On an open set s, the second directional derivative x ↦ D(Dg(·) v)(x) v of a C² map g in a fixed direction v is continuous.

theorem TauCeti.eventually_fderiv_ne {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {g : E → F} {x : E} {c : E →L[𝕜] F} (hg : ContDiffAt 𝕜 2 g x) (hinv : (fderiv 𝕜 (fderiv 𝕜 g) x).IsInvertible) : ∀ᶠ (y : E) in nhdsWithin x {x}ᶜ, fderiv 𝕜 g y ≠ c

Where the second derivative is invertible, the differential avoids any prescribed value near the point. Nothing is assumed about the value c, and in particular the differential need not vanish at x. The punctured neighbourhood on which c is avoided may depend on c, so this is avoidance of one fixed value rather than local injectivity of fderiv 𝕜 g.

theorem TauCeti.fderiv_fderiv_comp_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] {f : E → G} {φ : F → E} {b : F} (hf : ContDiffAt 𝕜 2 f (φ b)) (hφ : ContDiffAt 𝕜 2 φ b) (v w : F) : ((fderiv 𝕜 (fderiv 𝕜 (f ∘ φ)) b) v) w = ((fderiv 𝕜 (fderiv 𝕜 f) (φ b)) ((fderiv 𝕜 φ b) v)) ((fderiv 𝕜 φ b) w) + (fderiv 𝕜 f (φ b)) (((fderiv 𝕜 (fderiv 𝕜 φ) b) v) w)

The second-order chain rule. If f is C² at φ b and φ is C² at b, then the second derivative of f ∘ φ at b is D²f(φ b)(Dφ v, Dφ w) + Df(φ b)(D²φ(v, w)).

theorem TauCeti.fderiv_fderiv_comp_apply_of_fderiv_eq_zero {𝕜 : 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] {f : E → G} {φ : F → E} {b : F} (hf : ContDiffAt 𝕜 2 f (φ b)) (hφ : ContDiffAt 𝕜 2 φ b) (hc : fderiv 𝕜 f (φ b) = 0) (v w : F) : ((fderiv 𝕜 (fderiv 𝕜 (f ∘ φ)) b) v) w = ((fderiv 𝕜 (fderiv 𝕜 f) (φ b)) ((fderiv 𝕜 φ b) v)) ((fderiv 𝕜 φ b) w)

The second derivative at a critical point is a bilinear form pullback. If f is C² at φ b, φ is C² at b, and the differential of f vanishes at φ b, then the second derivative of f ∘ φ at b is the second derivative of f at φ b evaluated on the images of the differential of φ.

theorem TauCeti.fderiv_fderiv_comp_fst_add_comp_snd {𝕜 : 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] {φ : E → G} {ψ : F → G} {a : E} {b : F} (hφ : ContDiffAt 𝕜 2 φ a) (hψ : ContDiffAt 𝕜 2 ψ b) : fderiv 𝕜 (fderiv 𝕜 (φ ∘ Prod.fst + ψ ∘ Prod.snd)) (a, b) = ↑(ContinuousLinearMap.coprodEquivL 𝕜) ∘SL (fderiv 𝕜 (fderiv 𝕜 φ) a).prodMap (fderiv 𝕜 (fderiv 𝕜 ψ) b)

The second derivative of a separated sum φ ∘ Prod.fst + ψ ∘ Prod.snd at (a, b) is block diagonal: it sends (v, w) to the coproduct of D²φ a v and D²ψ b w, i.e. to the functional (v', w') ↦ D²φ a v v' + D²ψ b w w'.

theorem TauCeti.fderiv_fderiv_fderiv_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {g : E → F} {x : E} (hg : ContDiffAt 𝕜 3 g x) (v a b : E) : ((fderiv 𝕜 (fderiv 𝕜 fun (y : E) => (fderiv 𝕜 g y) v) x) a) b = (((fderiv 𝕜 (fderiv 𝕜 (fderiv 𝕜 g)) x) a) b) v

The second derivative of the directional derivative y ↦ Dg(y) v of a C³ map g is the third derivative of g, evaluated at v.

theorem TauCeti.fderiv_fderiv_fderiv_apply_comm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : WithTop ℕ∞} {g : E → F} {x : E} (hg : ContDiffAt 𝕜 n g x) (hn : minSmoothness 𝕜 3 ≤ n) (a b c : E) : (((fderiv 𝕜 (fderiv 𝕜 (fderiv 𝕜 g)) x) a) b) c = (((fderiv 𝕜 (fderiv 𝕜 (fderiv 𝕜 g)) x) a) c) b

The third derivative is symmetric in its last two directions. For a map that is C^{minSmoothness 𝕜 3} at x (so C³ over ℝ or ℂ), differentiating the symmetry of the second derivative near x gives D³g(x)(a, b, c) = D³g(x)(a, c, b).