Iterates Actual Matrix Primitive

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_increment_matrix_primitive_pairing {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} {κm κprev : ℝ} {θ₀ : Homogenization.Vec 2 → ℝ} {θprev : ℝ → Homogenization.Vec 2 → ℝ} {T : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hT : I.IsTIterates hΦ m κm κprev θ₀ θprev T) (hθ : IsClassicalSol (streamVel (Φ (m - 1))) κprev (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) θ₀ θprev) (hm : 1 ≤ m) (hκm : 0 < κm) (i : ℕ) (hi : i + 1 ≤ Nstar β) (w : List (Fin 2)) {s : ℝ} (hs : 0 ≤ s) (hs1 : s ≤ 1) : have u := fun (t : ℝ) => iterateSpatialWord w (iterateIncrement T (i + 1) t); have v := fun (t : ℝ) => iterateSpatialWord w (iterateIncrement T i t); have b := streamVel (Φ (m - 1)); have Q := iterateKmatPrimitive I κm m; ∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (u z.1) z.2) ((I.Kmat κm m z.1 - timeAvgMat (I.Kmat κm m)).mulVec (spaceGrad (v z.1) z.2)) = ((∫ (x : Homogenization.Vec 2) in unitCube, Homogenization.vecDot (spaceGrad (u s) x) ((Q s).mulVec (spaceGrad (v s) x))) - ∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (u z.1) z.2) ((Q z.1).mulVec fun (k : Fin 2) => amnrMaterial b (fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (v t) x k) z.1 z.2)) - ∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (fun (j : Fin 2) => amnrMaterial b (fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (u t) x j) z.1 z.2) ((Q z.1).mulVec (spaceGrad (v z.1) z.2))

Full matrix oscillatory flux identity for actual increments. The terminal term and both differentiated material terms are assembled without norm loss.