Iterates Centered Hessian Transfer

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_centered_hessian_forcing_transfer {β : ℝ} (I : Ingredients β) (hN : 1 ≤ Nstar β) {m : ℕ} {κm : ℝ} (hm : 1 ≤ m) (hκm : 0 < κm) {u : ℝ → Homogenization.Vec 2 → ℝ} (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (hup : ∀ (t : ℝ), 0 < t → IsZ2Periodic (u t)) (w : List (Fin 2)) {s : ℝ} (hs : 0 ≤ s) : ∫ (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)) = -∫ (t : ℝ) in 0..s, ∫ (x : Homogenization.Vec 2) in unitCube, (∑ j : Fin 2, ∑ k : Fin 2, (I.Kmat κm m t j k - timeAvgMat (I.Kmat κm m) j k) * iterateSpatialWord (j :: k :: w) (u t) x) * ∑ j : Fin 2, ∑ k : Fin 2, iterateKmatPrimitive I κm m t j k * iterateSpatialWord (j :: k :: w) (u t) x

The centered forcing gradient transfers to the exact Hessian half-square pairing. This is the first-increment forcing term, with its original sign.