Quantitative comparison of geodesics and polynomial trajectories #
These estimates preserve the quadratic dependence of acceleration on velocity. The contraction constants tend to zero with the allowed velocity radius.
theorem
PlanarMidpoint.force_difference_bound
(C : E → Coeff)
(S : Set E)
(M L r : ℝ)
(hM : 0 ≤ M)
(hL : 0 ≤ L)
(_hr : 0 ≤ r)
(hbound : ∀ x ∈ S, ‖C x‖ ≤ M)
(hLip : ∀ x ∈ S, ∀ y ∈ S, ‖C x - C y‖ ≤ L * ‖x - y‖)
{x y v w : E}
(hx : x ∈ S)
(hy : y ∈ S)
(hv : ‖v‖ ≤ r)
(hw : ‖w‖ ≤ r)
:
Spatial and velocity Lipschitz constants for the Christoffel force on a small phase neighborhood.
theorem
PlanarMidpoint.geodesic_polynomial_comparison
(C : E → Coeff)
(S : Set E)
(M L r R : ℝ)
(hM : 0 ≤ M)
(hL : 0 ≤ L)
(hr : 0 ≤ r)
(hbound : ∀ x ∈ S, ‖C x‖ ≤ M)
(hLip : ∀ x ∈ S, ∀ y ∈ S, ‖C x - C y‖ ≤ L * ‖x - y‖)
(hsmall : 8 * L * r ^ 2 + 16 * M * r < 1)
(x v y w b : ℝ → E)
(hx : ∀ t ∈ Set.Icc 0 1, HasDerivAt x (v t) t)
(hv : ∀ t ∈ Set.Icc 0 1, HasDerivAt v (-K (C (x t)) (v t) (v t)) t)
(hy : ∀ t ∈ Set.Icc 0 1, HasDerivAt y (w t) t)
(hw : ∀ t ∈ Set.Icc 0 1, HasDerivAt w (b t) t)
(h0 : x 0 = y 0)
(h1 : x 1 = y 1)
(hxS : ∀ t ∈ Set.Icc 0 1, x t ∈ S)
(hyS : ∀ t ∈ Set.Icc 0 1, y t ∈ S)
(hvsmall : ∀ t ∈ Set.Icc 0 1, ‖v t‖ ≤ r)
(hwsmall : ∀ t ∈ Set.Icc 0 1, ‖w t‖ ≤ r)
(hres : ∀ t ∈ Set.Icc 0 1, ‖b t + K (C (y t)) (w t) (w t)‖ ≤ R)
(t : ℝ)
(ht : t ∈ Set.Icc 0 1)
:
A true geodesic and a polynomial trajectory with the same endpoints are close whenever the latter has a small acceleration residual.
theorem
PlanarMidpoint.force_taylor_error_bound
(c d : Coeff)
(x v : E)
(η B ε : ℝ)
(hη : 0 ≤ η)
(hB : 0 ≤ B)
(hε : 0 ≤ ε)
(hcoeff : ‖c - d‖ ≤ η * ‖x‖ ^ 2)
(hx : ‖x‖ ≤ B * ε)
(hv : ‖v‖ ≤ B * ε)
:
A coefficient Taylor error, quadratic in displacement, becomes a fourth-order force error when displacement and velocity are both first order.