Iterates Flow Bounds

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_flowGrad_word_bound {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {l : ℤ} {t : ℝ} (hne : I.hatXiML m l t ≠ 0) (w : List (Fin 2)) (x : Homogenization.Vec 2) (i j : Fin 2) : |iterateSpatialWord w (fun (y : Homogenization.Vec 2) => (I.flowGrad hΦ m l t y - 1) i j) x| ≤ 40 * ↑w.length.factorial * (2 ^ 10 / epsilon β I.Λ (m - 1)) ^ w.length

All coordinate words, with explicit constants fixed before ingredients.