Second-order Taylor estimates along line segments

The coarse remainder constant is sufficient for uniform geodesic residual estimates. It follows by two applications of the vector-valued mean-value inequality and does not invoke parameter smoothness of ODE solutions.

theorem PlanarMidpoint.second_order_line_remainder {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {x v a : ℝ → V} {M : ℝ} (hM : 0 ≤ M) (hx : ∀ t ∈ Set.Icc 0 1, HasDerivAt x (v t) t) (hv : ∀ t ∈ Set.Icc 0 1, HasDerivAt v (a t) t) (ha : ∀ t ∈ Set.Icc 0 1, ‖a t - a 0‖ ≤ M) : ‖x 1 - x 0 - v 0 - (1 / 2) • a 0‖ ≤ M

A uniform bound on the change in the second derivative controls the second-order Taylor remainder at time one.

theorem PlanarMidpoint.second_order_spatial_remainder {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : U → V} {J : U → U →L[ℝ] V} {H : U → U →L[ℝ] U →L[ℝ] V} {S : Set U} {p d : U} {η : ℝ} (hη : 0 ≤ η) (hseg : ∀ t ∈ Set.Icc 0 1, p + t • d ∈ S) (hf : ∀ y ∈ S, HasFDerivAt f (J y) y) (hJ : ∀ y ∈ S, HasFDerivAt J (H y) y) (hH : ∀ y ∈ S, ‖H y - H p‖ ≤ η) : ‖f (p + d) - f p - (J p) d - (1 / 2) • ((H p) d) d‖ ≤ η * ‖d‖ ^ 2

A second-order spatial remainder estimate from bounds on the variation of an actual second Fréchet derivative along the segment.

theorem PlanarMidpoint.exists_second_order_spatial_remainder {U : Type u_1} {V : Type u_2} [NormedAddCommGroup U] [NormedSpace ℝ U] [NormedAddCommGroup V] [NormedSpace ℝ V] {f : U → V} {Ω : Set U} {p : U} (hΩ : IsOpen Ω) (hp : p ∈ Ω) (hf : ContDiffOn ℝ 2 f Ω) {η : ℝ} (hη : 0 < η) : ∃ r > 0, Metric.ball p r ⊆ Ω ∧ ∀ (d : U), ‖d‖ < r → ‖f (p + d) - f p - (fderiv ℝ f p) d - (1 / 2) • ((fderiv ℝ (fderiv ℝ f) p) d) d‖ ≤ η * ‖d‖ ^ 2

A C² map has a second-order spatial expansion with a uniformly small quadratic remainder on a sufficiently small ball.