Uniform trajectory bounds for recursive spatial jets. The base point component is controlled inductively, and each newly appended column satisfies a linear equation with coefficients bounded on the resulting compact tube.

theorem AVenhance.Infra.Flow.FiniteSpatialJetBounds.norm_prod_pi_le_of_components {E : Type u_1} [NormedAddCommGroup E] (x : E) (f : Fin 2 → E) {C : ℝ} (hC : 0 ≤ C) (hx : ‖x‖ ≤ C) (hf : ∀ (i : Fin 2), ‖f i‖ ≤ C) : ‖(x, f)‖ ≤ C

theorem AVenhance.Infra.Flow.FiniteSpatialJetBounds.exists_spatialJetField_derivative_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 ℝ (Function.uncurry (spatialJetField b n)) (t, z)‖ ≤ M

theorem AVenhance.Infra.Flow.spatialJetFlow_bounded_on_window {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlowOn b X) (n : ℕ) (a d s R : ℝ) : 0 ≤ R → ∃ (C : ℝ), 0 ≤ C ∧ ∀ t ∈ Set.Icc a d, ∀ (z : SpatialJetState n), ‖z‖ ≤ R → ‖spatialJetFlow hb X hX n t z s‖ ≤ C

On any compact time window, all order-n jet trajectories from a bounded set of initial states remain in one bounded state ball.