Dirichlet stability with a quantitatively absorbable differential residual.

theorem PlanarMidpoint.dirichlet_stability {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] (x v a : ℝ → V) (R Lx Lv : ℝ) (hx : ∀ t ∈ Set.Icc 0 1, HasDerivAt x (v t) t) (hv : ∀ t ∈ Set.Icc 0 1, HasDerivAt v (a t) t) (hx0 : x 0 = 0) (hx1 : x 1 = 0) (hLx : 0 ≤ Lx) (hLv : 0 ≤ Lv) (hsmall : Lx + Lv < 1) (hres : ∀ t ∈ Set.Icc 0 1, ‖a t‖ ≤ R + Lx * ‖x t‖ + Lv * ‖v t‖) (t : ℝ) (ht : t ∈ Set.Icc 0 1) : ‖x t‖ ≤ R / (1 - Lx - Lv) ∧ ‖v t‖ ≤ R / (1 - Lx - Lv)

A residual bound controls a zero-endpoint curve and its velocity whenever the sum of the two Lipschitz constants is less than one. Compactness supplies the maximum, so no a priori bound on the unknown error is assumed.

theorem PlanarMidpoint.bvp_stability {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] (x v a y w b : ℝ → V) (R Lx Lv : ℝ) (hx : ∀ t ∈ Set.Icc 0 1, HasDerivAt x (v t) t) (hv : ∀ t ∈ Set.Icc 0 1, HasDerivAt v (a 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) (hLx : 0 ≤ Lx) (hLv : 0 ≤ Lv) (hsmall : Lx + Lv < 1) (hres : ∀ t ∈ Set.Icc 0 1, ‖a t - b t‖ ≤ R + Lx * ‖x t - y t‖ + Lv * ‖v t - w t‖) (t : ℝ) (ht : t ∈ Set.Icc 0 1) : ‖x t - y t‖ ≤ R / (1 - Lx - Lv) ∧ ‖v t - w t‖ ≤ R / (1 - Lx - Lv)

Stability for a true and an approximate curve having the same endpoints.