All spatial orders of the actual flows on source cutoff windows.

theorem AVenhance.Infra.Section4.amnr_previous_flow_spatial_contDiff_infty_of_A3 {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (s t : ℝ) (ht : |t - s| ≤ tauPP β I.Λ m / 2 + tauP β I.Λ m) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => flow (streamVel (Φ (m - 1))) ⋯ ⋯ t x s

The actual previous flow is spatially smooth on every interval of the source cutoff length. Invertibility is proved from the actual Jacobian rate given by the stream-regularity estimates.

theorem AVenhance.Infra.Section4.amnr_xFlow_spatial_contDiff_infty_of_A3 {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) (t : ℝ) (ht : |t - ↑l * tauPP β I.Λ m| ≤ tauPP β I.Λ m / 2 + tauP β I.Λ m) : ContDiff ℝ (↑⊤) (I.xFlow hΦ m l t)

Every spatial order of the forward flow is now proved on the whole actual cutoff window, instead of supplied as a smoothness hypothesis.

theorem AVenhance.Infra.Section4.amnr_xFlowInv_spatial_contDiff_infty_of_A3 {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (l : ℤ) (t : ℝ) (ht : |t - ↑l * tauPP β I.Λ m| ≤ tauPP β I.Λ m / 2 + tauP β I.Λ m) : ContDiff ℝ (↑⊤) (I.xFlowInv hΦ m l t)

Every spatial order of the inverse flow follows by exchanging its actual initial and target times in the same short-interval argument.