Iterates Coefficient Words

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_sMat_word_entry_bound {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm t : ℝ) (hflow : ∀ (l : ℤ), ContDiff ℝ (↑⊤) (I.flowGrad hΦ m l t)) (w : List (Fin 2)) (x : Homogenization.Vec 2) {K : ℝ} {F : ℕ → ℝ} (hK : ∀ (i j : Fin 2), |I.Kmat κm m t i j| ≤ K) (hF : ∀ (l : ℤ), I.hatXiML m l t ≠ 0 → ∀ (v : List (Fin 2)) (y : Homogenization.Vec 2) (i j : Fin 2), |iterateSpatialWord v (fun (z : Homogenization.Vec 2) => (I.flowGrad hΦ m l t z - 1) i j) y| ≤ F v.length) (i j : Fin 2) : |iterateSpatialWord w (fun (y : Homogenization.Vec 2) => I.sMat hΦ m κm t y i j) x| ≤ coarseCoeffWordBudget K κm F w

The LeftJacobian jet uses all flow suborders in the quadratic Leibniz budget.