Coarse Dirichlet estimates for vector-valued curves on the unit interval.

theorem PlanarMidpoint.velocity_secant_bound {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] (x v a : ℝ → V) (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‖ ≤ M) (t : ℝ) (ht : t ∈ Set.Icc 0 1) : ‖v t - (x 1 - x 0)‖ ≤ M

Bounded acceleration controls velocity relative to its endpoint secant.

theorem PlanarMidpoint.position_chord_bound {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] (x v a : ℝ → V) (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‖ ≤ M) (t : ℝ) (ht : t ∈ Set.Icc 0 1) : ‖x t - ((1 - t) • x 0 + t • x 1)‖ ≤ M

The corresponding position differs from its affine chord by at most M.

theorem PlanarMidpoint.dirichlet_velocity_bound {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] (x v a : ℝ → V) (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‖ ≤ M) (hx0 : x 0 = 0) (hx1 : x 1 = 0) (t : ℝ) (ht : t ∈ Set.Icc 0 1) : ‖v t‖ ≤ M

Zero endpoint data convert the secant estimate to a velocity estimate.

theorem PlanarMidpoint.dirichlet_position_bound {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] (x v a : ℝ → V) (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‖ ≤ M) (hx0 : x 0 = 0) (hx1 : x 1 = 0) (t : ℝ) (ht : t ∈ Set.Icc 0 1) : ‖x t‖ ≤ M

Zero endpoint data convert the chord estimate to a position estimate.

theorem PlanarMidpoint.dirichlet_unique {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] [CompleteSpace V] (x v : ℝ → V) (hx : ∀ t ∈ Set.Icc 0 1, HasDerivAt x (v t) t) (hv : ∀ t ∈ Set.Icc 0 1, HasDerivAt v 0 t) (hx0 : x 0 = 0) (hx1 : x 1 = 0) (t : ℝ) (ht : t ∈ Set.Icc 0 1) : x t = 0

A curve with zero acceleration and zero endpoints vanishes identically.