Compact-window Taylor control for the recursive augmented fields.

theorem AVenhance.Infra.Flow.spatialJetField_fderiv_eq_joint {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) (n : ℕ) (t : ℝ) (z : SpatialJetState n) : fderiv ℝ (spatialJetField b n t) z = fderiv ℝ (Function.uncurry (spatialJetField b n)) (t, z) ∘SL ContinuousLinearMap.inr ℝ ℝ (SpatialJetState n)

theorem AVenhance.Infra.Flow.spatialJetField_fderiv_bound_on_window {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) (n : ℕ) (a d R : ℝ) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ t ∈ Set.Icc a d, ∀ (z : SpatialJetState n), ‖z‖ ≤ R → ‖fderiv ℝ (spatialJetField b n t) z‖ ≤ M

The state derivative of an augmented field is uniformly bounded on a compact time window and a bounded state ball.

theorem AVenhance.Infra.Flow.spatialJetField_taylor_remainder_on_window {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) (n : ℕ) (a d R : ℝ) (hR : 0 ≤ R) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ t ∈ Set.Icc a d, ∀ (x y : SpatialJetState n), ‖x‖ ≤ R → ‖y‖ ≤ R → ‖spatialJetField b n t y - spatialJetField b n t x - (fderiv ℝ (spatialJetField b n t) x) (y - x)‖ ≤ C * ‖y - x‖ * ‖y - x‖

On a compact time window and a bounded state ball, the nonlinear part of the first-order Taylor expansion of any recursive jet field is quadratically bounded.