Joint continuity of finite recursive jet flows on compact windows.

theorem AVenhance.Infra.Flow.spatialJetFlow_dist_le_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 : ℝ) (hs : s ∈ Set.Icc a d) (R : ℝ) (hR : 0 ≤ R) : ∃ (K : NNReal), ∀ t ∈ Set.Icc a d, ∀ (z w : SpatialJetState n), ‖z‖ ≤ R → ‖w‖ ≤ R → dist (spatialJetFlow hb X hX n t z s) (spatialJetFlow hb X hX n t w s) ≤ dist z w * Real.exp (↑K * |t - s|)

On a compact time window and a bounded set of initial jet states, the finite jet flow is Lipschitz in its initial state, with a constant depending on the window and the bounded trajectory tube.

theorem AVenhance.Infra.Flow.spatialJetFlow_continuous_fixed_start {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlowOn b X) (n : ℕ) (s : ℝ) : Continuous fun (p : ℝ × SpatialJetState n) => spatialJetFlow hb X hX n p.1 p.2 s

The target-time and initial-state map of each finite recursive jet flow is continuous when the initial time is fixed.