Uniform residual bounds for the actual coefficient field.

theorem PlanarMidpoint.approx_actual_residual_bound (C : E → Coeff) (p : E) (c : Coeff) (J : E →L[ℝ] Coeff) (H : Hessian) (h : E) (η B T ε t : ℝ) (hη : 0 ≤ η) (hB : 0 ≤ B) (hε : 0 ≤ ε) (hd : ‖approxDisplacement c J H h ε t‖ ≤ B * ε) (hv : ‖approxVelocity c J H h ε t‖ ≤ B * ε) (htail : ‖approxResidualTail c J H h ε t‖ ≤ T) (hcoeff : have d := approxDisplacement c J H h ε t; ‖C (p + d) - c - J d - (1 / 2) • (H d) d‖ ≤ η * ‖d‖ ^ 2) : ‖approxAcceleration c J H h ε t + K (C (p + approxDisplacement c J H h ε t)) (approxVelocity c J H h ε t) (approxVelocity c J H h ε t)‖ ≤ (8 * η * B ^ 4 + T * ε) * ε ^ 4

theorem PlanarMidpoint.short_geodesic_approximation (C : E → Coeff) (p : E) (c : Coeff) (J : E →L[ℝ] Coeff) (H : Hessian) (h : E) (r M L η B T ε ρ : ℝ) (hM : 0 ≤ M) (hL : 0 ≤ L) (hr : 0 < r) (hη : 0 ≤ η) (hB : 0 ≤ B) (hT : 0 ≤ T) (hε : 0 ≤ ε) (hbound : ∀ x ∈ Metric.ball p r, ‖C x‖ ≤ M) (hLip : ∀ x ∈ Metric.ball p r, ∀ y ∈ Metric.ball p r, ‖C x - C y‖ ≤ L * ‖x - y‖) (hsmall : 8 * L * r ^ 2 + 16 * M * r < 1 / 2) (hcoeff : ∀ (d : E), ‖d‖ < ρ → ‖C (p + d) - c - J d - (1 / 2) • (H d) d‖ ≤ η * ‖d‖ ^ 2) (hsize : ∀ t ∈ Set.Icc 0 1, ‖approxDisplacement c J H h ε t‖ ≤ B * ε ∧ ‖approxVelocity c J H h ε t‖ ≤ B * ε ∧ ‖approxResidualTail c J H h ε t‖ ≤ T) (hεr : B * ε < r) (hερ : B * ε < ρ) (γ v : ℝ → E) (hγ : IsShortGeodesic C 1 p r (p - (ε / 2) • h) (p + (ε / 2) • h) γ v) : ‖γ (1 / 2) - (p + approxDisplacement c J H h ε (1 / 2))‖ ≤ 2 * (8 * η * B ^ 4 + T * ε) * ε ^ 4

A short actual geodesic has the quartic midpoint polynomial as a uniform approximation. All hypotheses on the approximate trajectory are explicit polynomial bounds, while the actual curve is constrained only by the ODE.

theorem PlanarMidpoint.exists_short_geodesic_approximation (C : E → Coeff) (p : E) (c : Coeff) (J : E →L[ℝ] Coeff) (H : Hessian) (h : E) (r M L : ℝ) (hr : 0 < r) (hM : 0 ≤ M) (hL : 0 ≤ L) (hbound : ∀ x ∈ Metric.ball p r, ‖C x‖ ≤ M) (hLip : ∀ x ∈ Metric.ball p r, ∀ y ∈ Metric.ball p r, ‖C x - C y‖ ≤ L * ‖x - y‖) (hsmall : 8 * L * r ^ 2 + 16 * M * r < 1 / 2) (hTaylor : ∀ η > 0, ∃ ρ > 0, ∀ (d : E), ‖d‖ < ρ → ‖C (p + d) - c - J d - (1 / 2) • (H d) d‖ ≤ η * ‖d‖ ^ 2) (κ : ℝ) (hκ : 0 < κ) : ∃ δ > 0, ∀ (ε : ℝ), 0 ≤ ε → ε < δ → ∀ (γ v : ℝ → E), IsShortGeodesic C 1 p r (p - (ε / 2) • h) (p + (ε / 2) • h) γ v → ‖γ (1 / 2) - (p + approxDisplacement c J H h ε (1 / 2))‖ ≤ κ * ε ^ 4

Uniform fourth-order approximation, expressed without any differentiability of the endpoint-to-geodesic choice.