Iterates Terminal Centered Forcing Split

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_terminal_centered_forcing_pairing_split {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (hN : 1 ≤ Nstar β) {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 : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u 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 (I.TForcing hΦ m κm κprev u z.1)) z.2) ((iterateKmatPrimitive I κm m z.1).mulVec (spaceGrad (iterateSpatialWord w (u z.1)) z.2)) = (∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (fun (y : Homogenization.Vec 2) => ∑ j : Fin 2, ∑ k : Fin 2, (I.Kmat κm m z.1 j k - timeAvgMat (I.Kmat κm m) j k) * iterateSpatialWord (j :: k :: w) (u z.1) y) z.2) ((iterateKmatPrimitive I κm m z.1).mulVec (spaceGrad (iterateSpatialWord w (u z.1)) z.2))) + ∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (iterateSpatialWord w (vecDiv fun (y : Homogenization.Vec 2) => (timeAvgMat (I.Kmat κm m) - κprev • 1 + I.sMat hΦ m κm z.1 y).mulVec (spaceGrad (u z.1) y))) z.2) ((iterateKmatPrimitive I κm m z.1).mulVec (spaceGrad (iterateSpatialWord w (u z.1)) z.2))

The actual first-increment forcing pairing splits into the exact centered cancellation and small remainder, with all integrability proved.