Quadratic initial-point remainder for the flow's second variation.

theorem AVenhance.Infra.Flow.ThirdSpatialRemainder.gronwallBound_zero_scale_thirdSpatialRemainder (L a c d : ℝ) : gronwallBound 0 L (c * a) d = c * gronwallBound 0 L a d

theorem AVenhance.Infra.Flow.ThirdSpatialRemainder.thirdRemainder_linearFlow_bound_on_Ico (A : ℝ → Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) (M : ℝ) (hM₀ : 0 ≤ M) (hA : ∀ (q : ℝ), ‖A q‖ ≤ M) {V : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hV : IsFlow (fun (q : ℝ) (v : Homogenization.Vec 2) => (A q) v) V) (s t : ℝ) (_hst : s ≤ t) (v : Homogenization.Vec 2) (q : ℝ) : q ∈ Set.Ico s t → ‖V q v s‖ ≤ Real.exp (M * (t - s)) * ‖v‖

theorem AVenhance.Infra.Flow.exists_flow_secondVariation_quadratic_remainder_all_times_of_le {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (x : Homogenization.Vec 2) (s t : ℝ) (hst : s ≤ t) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (u h k : Homogenization.Vec 2), ∀ q ∈ Set.Icc s t, ‖flowSecondVariation hb hX (x + u) s ⋯ h k q 0 s - flowSecondVariation hb hX x s ⋯ h k q 0 s - flowThirdVariation hb hX x s ⋯ u h k q 0 s‖ ≤ C * ‖u‖ * ‖u‖ * ‖h‖ * ‖k‖

On a forward interval, the selected third variation is the linear term in the initial-point Taylor expansion of the second variation, with a uniform quadratic remainder.