Iterates Centered Remainder Gradient #
Support for the Armstrong–Vicol anomalous-diffusion formalization.
theorem
AVenhance.Infra.Section4.iterate_TForcing_word_gradient_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)
:
spaceGrad (iterateSpatialWord w (I.TForcing hΦ m κm κprev v t)) x = spaceGrad
(fun (y : Homogenization.Vec 2) =>
∑ 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) y)
x + spaceGrad
(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 forcing gradient retains the centered term separately from the small mean/spatial remainder at every spatial order.