Iterates Forcing Flux Parts #
Support for the Armstrong–Vicol anomalous-diffusion formalization.
theorem
AVenhance.Infra.Section4.iterate_TForcing_word_flux_three_parts
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(κm κprev t : ℝ)
(hs : ContDiff ℝ (↑⊤) (I.sMat hΦ m κm t))
(v : Homogenization.Vec 2 → ℝ)
(w : List (Fin 2))
(x : Homogenization.Vec 2)
:
iterateWordFlux (fun (y : Homogenization.Vec 2) => I.Kmat κm m t - κprev • 1 + I.sMat hΦ m κm t y) v w x = (I.Kmat κm m t - timeAvgMat (I.Kmat κm m)).mulVec (spaceGrad (iterateSpatialWord w v) x) + (timeAvgMat (I.Kmat κm m) - κprev • 1).mulVec (spaceGrad (iterateSpatialWord w v) x) + iterateWordFlux (I.sMat hΦ m κm t) v w x
The actual forcing separates its centered time oscillation, mean diffusivity mismatch, and spatial flow correction at every word order.