Primitive zero-order bounds for the actual pulled-back flow gradient.

theorem AVenhance.Infra.Section4.amnr_flowGrad_abs_le_of_lipschitz {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) {L : ℝ} (hL : ∀ (t : ℝ) (x y : Homogenization.Vec 2), ‖streamVel (Φ (m - 1)) t x - streamVel (Φ (m - 1)) t y‖ ≤ L * ‖x - y‖) (l : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (k p : Fin 2) : |I.flowGrad hΦ m l t x k p| ≤ Real.exp (L * |t - ↑l * tauPP β I.Λ m|)

Grönwall controls every coordinate of the actual flow gradient. The pullback evaluation needs no additional estimate on the inverse flow.

theorem AVenhance.Infra.Section4.amnr_flowGrad_abs_le_on_cutoff_window {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {C : ℝ} (hC : 0 ≤ C) (hL : ∀ (t : ℝ) (x y : Homogenization.Vec 2), ‖streamVel (Φ (m - 1)) t x - streamVel (Φ (m - 1)) t y‖ ≤ C * a β I.Λ (m - 1) * ‖x - y‖) (l : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (ht : |t - ↑l * tauPP β I.Λ m| ≤ tauPP β I.Λ m / 2 + tauP β I.Λ m) (k p : Fin 2) : |I.flowGrad hΦ m l t x k p| ≤ Real.exp (C * 2 ^ (-25))

On every closed cutoff window, the source-scale Lipschitz estimate gives a uniform primitive flow-gradient bound, independent of m and l.