Joint continuity of the actual sMat spatial jets from conditional flow jets. The time cutoff sum is represented locally by a fixed finite sum.

theorem AVenhance.Infra.Section4.IteratesCoefficientContinuity.iterate_hatXi_active_distance {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) (t : ℝ) (hne : I.hatXiML m l t ≠ 0) : |t - ↑l * tauPP β I.Λ m| ≤ 1 / 2 * tauPP β I.Λ m + tauP β I.Λ m

theorem AVenhance.Infra.Section4.iterate_sMat_word_joint_continuousOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm : ℝ} (hκm : 0 < κm) (hflow : ∀ (l : ℤ), ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) (i j : Fin 2) : ContinuousOn (fun (z : AmnrSpace) => iterateSpatialWord w (fun (y : Homogenization.Vec 2) => I.sMat hΦ m κm z.1 y i j) z.2) (Set.Ici 0 ×ˢ Set.univ)

Continuity of all actual sMat word jets. The conditional premise is joint smoothness of the actual flow Jacobians; K and cutoff continuity are proved.

theorem AVenhance.Infra.Section4.iterate_sMat_matrixWord_joint_continuousOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {κm : ℝ} (hκm : 0 < κm) (hflow : ∀ (l : ℤ), ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) : ContinuousOn (fun (z : AmnrSpace) => iterateMatrixWord (I.sMat hΦ m κm z.1) w z.2) (Set.Ici 0 ×ˢ Set.univ)

Matrix-valued joint continuity of the actual coefficient jet.