Iterates Flow Close

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_flowGrad_zero_bound {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 2 ≤ m) {l : ℤ} {t : ℝ} (hne : I.hatXiML m l t ≠ 0) (x : Homogenization.Vec 2) (i j : Fin 2) : |(I.flowGrad hΦ m l t x - 1) i j| ≤ 40 * epsilon β I.Λ (m - 1) ^ (2 * delta β)

The refresh-time estimate supplies the small factor, rather than the uniform all-order seminorm bound.