Iterates Centered Remainder Formula

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_word_constant_plus_matrix_forcing (B : Matrix (Fin 2) (Fin 2) ℝ) {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {v : Homogenization.Vec 2 → ℝ} (hA : ContDiff ℝ (↑⊤) A) (hv : ContDiff ℝ (↑⊤) v) (w : List (Fin 2)) (x : Homogenization.Vec 2) : iterateSpatialWord w (vecDiv fun (y : Homogenization.Vec 2) => (B + A y).mulVec (spaceGrad v y)) x = ∑ j : Fin 2, ∑ k : Fin 2, B j k * iterateSpatialWord (j :: k :: w) v x + iterateSpatialWord w (vecDiv fun (y : Homogenization.Vec 2) => (A y).mulVec (spaceGrad v y)) x

A time-only coefficient separates as its literal Hessian contraction before applying any forcing-energy estimate.

theorem AVenhance.Infra.Section4.iterate_TForcing_word_centered_remainder {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm κprev t : ℝ) (v : ℝ → Homogenization.Vec 2 → ℝ) (hs : ContDiff ℝ (↑⊤) (I.sMat hΦ m κm t)) (hv : ContDiff ℝ (↑⊤) (v t)) (w : List (Fin 2)) (x : Homogenization.Vec 2) : iterateSpatialWord w (I.TForcing hΦ m κm κprev v t) x = ∑ j : Fin 2, ∑ k : Fin 2, (I.Kmat κm m t j k - timeAvgMat (I.Kmat κm m) j k) * iterateSpatialWord (j :: k :: w) (v t) x + iterateSpatialWord w (vecDiv fun (y : Homogenization.Vec 2) => (timeAvgMat (I.Kmat κm m) - κprev • 1 + I.sMat hΦ m κm t y).mulVec (spaceGrad (v t) y)) x

The actual differentiated forcing is its centered Hessian contraction plus the actual mean/spatial remainder forcing.