The first spatial primitive flow rate, from actual stream-regularity derivative bounds.

theorem AVenhance.Infra.Section4.amnr_previous_velocity_lipschitz_of_A3 {β C : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hreg : StreamRegularityBounds C I Φ) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) (x y : Homogenization.Vec 2) : ‖streamVel (Φ (m - 1)) t x - streamVel (Φ (m - 1)) t y‖ ≤ 2 ^ 20 * a β I.Λ (m - 1) * ‖x - y‖

The actual previous velocity has the source Lipschitz rate also at the zero-stream base scale.

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

The inverse flow has a uniform spatial derivative norm on each actual cutoff window, from Grönwall and the preceding source velocity rate.