Normalized coefficient motion from genuine one-sided time derivatives.

theorem EulerPacketMovingFrame.normalized_motion_errors_within {a ε Θ G d β : ℝ} {B E : ℝ → Fin 3 → Fin 3 → ℝ} {h h₁ b₁ k₁ : ℝ → ℝ} (ha : 1 / 2 ≤ a) (hε : 0 < ε) (hΘ : 1 ≤ Θ) (hG : 1 ≤ G) (hd : 0 ≤ d) (hsmall : 16 * (ε * Θ * G ^ 2 + d) ≤ 1) (hB : ∀ t ∈ Set.Icc 0 Θ, ∀ (i j : Fin 3), |B t i j| ≤ G) (hE : ∀ t ∈ Set.Icc 0 Θ, ∀ (i j : Fin 3), |E t i j| ≤ d) (hb : ∀ t ∈ Set.Icc 0 Θ, HasDerivWithinAt (fun (s : ℝ) => B s 0 1) (b₁ t) (Set.Icc 0 Θ) t) (hk : ∀ t ∈ Set.Icc 0 Θ, HasDerivWithinAt (fun (s : ℝ) => B s 2 1) (k₁ t) (Set.Icc 0 Θ) t) (hbBound : ∀ t ∈ Set.Icc 0 Θ, |b₁ t| ≤ 2 * ε * G ^ 2) (hkBound : ∀ t ∈ Set.Icc 0 Θ, |k₁ t| ≤ 2 * ε * G ^ 2) (hShear : ∀ t ∈ Set.Icc 0 Θ, HasDerivWithinAt h (h₁ t) (Set.Icc 0 Θ) t) (hShearBound : ∀ t ∈ Set.Icc 0 Θ, |h₁ t| ≤ 4 * ε * G * |h t|) (hb0 : B 0 0 1 = a) (hk0 : B 0 2 1 = a * β) (hh0 : h 0 = a / ε ^ 2) : have e := 16 * (ε * Θ * G ^ 2 + d); ε ≤ e ∧ ∀ t ∈ Set.Icc 0 Θ, (∀ (i j : Fin 3), |ε * B t i j / a| ≤ e) ∧ (∀ (i j : Fin 3), |E t i j / a| ≤ e) ∧ |ε ^ 2 * h t / a - 1| ≤ e ∧ |B t 0 1 / a - 1| ≤ e ∧ |B t 2 1 / a - β| ≤ e

The existing quantitative motion estimate applies on closed intervals without assuming an extension of the original coefficient paths.