Iterates Terminal Two Forcing Parts

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_terminal_TForcing_pairing_two_parts {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} {κm κprev : ℝ} (hm : 1 ≤ m) (hκm : 0 < κm) (hflow : ∀ (l : ℤ), ContDiff ℝ ↑⊤ fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2) {u v : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hv : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => v z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (w : List (Fin 2)) {s : ℝ} (hs : 0 ≤ s) : ∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (u z.1)) z.2) (iterateWordFlux (fun (y : Homogenization.Vec 2) => I.Kmat κm m z.1 - κprev • 1 + I.sMat hΦ m κm z.1 y) (v z.1) w z.2) = (∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (u z.1)) z.2) ((I.Kmat κm m z.1 - timeAvgMat (I.Kmat κm m)).mulVec (spaceGrad (iterateSpatialWord w (v z.1)) z.2))) + ∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (u z.1)) z.2) (iterateWordFlux (fun (y : Homogenization.Vec 2) => timeAvgMat (I.Kmat κm m) - κprev • 1 + I.sMat hΦ m κm z.1 y) (v z.1) w z.2)

Exact terminal forcing decomposition into the centered oscillation and mean-plus-spatial remainder. This permits a common small remainder budget.