A local quadratic remainder estimate for a flow and its variational equation. All bounds are confined to one compact forward time window and one bounded state tube.

theorem AVenhance.Infra.Flow.VariationalRemainderOnWindow.gronwallBound_zero_scale (K c a d : ℝ) : gronwallBound 0 K (c * a) d = c * gronwallBound 0 K a d

theorem AVenhance.Infra.Flow.flowOn_variational_quadratic_remainder_on_window {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (F : ℝ → E → E) {Y : ℝ → E → ℝ → E} (hY : IsFlowOn F Y) (x : E) {V : ℝ → E → ℝ → E} (A : ℝ → E →L[ℝ] E) (hV : IsFlowOn (fun (r : ℝ) (v : E) => (A r) v) V) {s t M T L C₀ R : ℝ} (hst : s ≤ t) (hM₀ : 0 ≤ M) (hT₀ : 0 ≤ T) (hL₀ : 0 ≤ L) (hA : ∀ r ∈ Set.Icc s t, ‖A r‖ ≤ M) (hAeq : ∀ (r : ℝ), A r = fderiv ℝ (F r) (Y r x s)) (htraj : ∀ r ∈ Set.Icc s t, ∀ (w : E), ‖w - x‖ ≤ 1 → ‖Y r w s‖ ≤ C₀) (hTube : C₀ + Real.exp (M * (t - s)) ≤ R) (hLip : ∀ r ∈ Set.Ico s t, LipschitzOnWith ⟨L, hL₀⟩ (F r) (Metric.closedBall 0 R)) (hTaylor : ∀ r ∈ Set.Ico s t, ∀ (v : E), ‖Y r x s‖ ≤ R → ‖v‖ ≤ R → ‖F r v - F r (Y r x s) - (A r) (v - Y r x s)‖ ≤ T * ‖v - Y r x s‖ * ‖v - Y r x s‖) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (h : E), ‖h‖ ≤ 1 → ‖Y t (x + h) s - Y t x s - V t h s‖ ≤ C * ‖h‖ * ‖h‖

A quadratic Taylor error in the vector field produces a quadratic error between a nonlinear trajectory and its variational approximation. The trajectory, derivative, Taylor, and Lipschitz hypotheses are only required on the indicated compact window and bounded state tube.