Second-order Taylor expansions

A map f between real normed spaces which is C³ at x has the second-order Taylor expansion

f x' = f x + Df(x) (x' - x) + ½ D²f(x) (x' - x) (x' - x) + O(‖x' - x‖ ^ 3).

More generally, the expansion holds whenever f is twice differentiable near x and its second derivative is Lipschitz at x, i.e. D²f(x') - D²f(x) = O(‖x' - x‖). The remainder vanishes at x, and since the second derivative is symmetric its derivative is Df(x') - Df(x) - D²f(x) (x' - x) = O(‖x' - x‖ ^ 2), so the estimate is two applications of the mean value inequality.

Let u be a real function on a real inner product space E. A second-order Taylor expansion of u at x is an expansion

u x' = u x + ⟪y, x' - x⟫ + ⟪A (x' - x), x' - x⟫ / 2 + o(‖x' - x‖ ^ 2)

with y : E and an operator A : E →L[ℝ] E. Only the quadratic form of A is determined by u, so A is unique once it is required to be symmetric: two symmetric second-order terms differ by a symmetric operator whose quadratic form is o(‖x' - x‖ ^ 2), hence zero along every line through x, and a symmetric operator with vanishing quadratic form is zero. No differentiability of u beyond the expansion itself is assumed, so the statement applies to the Alexandrov Hessian of a convex function.

Main statements

• TauCeti.isBigO_sub_taylor_two_of_hasFDerivAt — the second-order Taylor expansion, with cubic remainder, of a twice differentiable map whose second derivative is Lipschitz at the point.
• ContDiffAt.isBigO_sub_taylor_two — the second-order Taylor expansion of a C³ map, with cubic remainder.
• TauCeti.eq_of_isSymmetric_of_isLittleO — the symmetric second-order term of a Taylor expansion is unique.

theorem TauCeti.isBigO_sub_taylor_two_of_hasFDerivAt {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {f' : E → E →L[ℝ] F} {f'' : E → E →L[ℝ] E →L[ℝ] F} {x : E} (hf : ∀ᶠ (y : E) in nhds x, HasFDerivAt f (f' y) y) (hf' : ∀ᶠ (y : E) in nhds x, HasFDerivAt f' (f'' y) y) (hf'' : (fun (y : E) => f'' y - f'' x) =O[nhds x] fun (y : E) => y - x) : (fun (x' : E) => f x' - f x - (f' x) (x' - x) - 2⁻¹ • ((f'' x) (x' - x)) (x' - x)) =O[nhds x] fun (x' : E) => ‖x' - x‖ ^ 3

The second-order Taylor expansion with cubic remainder. If f has derivative f' and f' has derivative f'' near x, and f'' is Lipschitz at x in the sense that f'' y - f'' x = O(‖y - x‖), then f x' = f x + f' x (x' - x) + ½ f'' x (x' - x) (x' - x) + O(‖x' - x‖ ^ 3).

theorem ContDiffAt.isBigO_sub_taylor_two {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {x : E} (hf : ContDiffAt ℝ 3 f x) : (fun (x' : E) => f x' - f x - (fderiv ℝ f x) (x' - x) - 2⁻¹ • ((fderiv ℝ (fderiv ℝ f) x) (x' - x)) (x' - x)) =O[nhds x] fun (x' : E) => ‖x' - x‖ ^ 3

The second-order Taylor expansion of a C³ map. If f is C³ at x, then f x' = f x + Df(x) (x' - x) + ½ D²f(x) (x' - x) (x' - x) + O(‖x' - x‖ ^ 3).

theorem TauCeti.eq_of_isSymmetric_of_isLittleO {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {u : E → ℝ} {x y : E} {A B : E →L[ℝ] E} (hA : (↑A).IsSymmetric) (hB : (↑B).IsSymmetric) (hTA : (fun (x' : E) => u x' - u x - inner ℝ y (x' - x) - inner ℝ (A (x' - x)) (x' - x) / 2) =o[nhds x] fun (x' : E) => ‖x' - x‖ ^ 2) (hTB : (fun (x' : E) => u x' - u x - inner ℝ y (x' - x) - inner ℝ (B (x' - x)) (x' - x) / 2) =o[nhds x] fun (x' : E) => ‖x' - x‖ ^ 2) : A = B

The symmetric second-order term of a Taylor expansion is unique. If the real function u has the second-order expansions u x' = u x + ⟪y, x' - x⟫ + ⟪A (x' - x), x' - x⟫ / 2 + o(‖x' - x‖ ^ 2) and the same with B, and A and B are symmetric, then A = B.