Iterates Terminal Current Gradient Split

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_terminal_current_gradient_material_pairing_split {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {u v : ℝ → Homogenization.Vec 2 → ℝ} {Q : ℝ → Matrix (Fin 2) (Fin 2) ℝ} (hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ici 0 ×ˢ Set.univ)) (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)) (hQc : ContinuousOn (fun (z : AmnrSpace) => Q z.1) (Set.Ici 0 ×ˢ Set.univ)) {s : ℝ} (hs1 : s ≤ 1) : ∫ (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)) = (∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot (spaceGrad (amnrMaterial b u z.1) z.2) ((Q z.1).mulVec (spaceGrad (v z.1) z.2))) - ∫ (z : AmnrSpace) in iterateTruncatedCell s, Homogenization.vecDot ((gradMatrix (b z.1) z.2).mulVec (spaceGrad (u z.1) z.2)) ((Q z.1).mulVec (spaceGrad (v z.1) z.2))

The current coordinatewise material-gradient term has the same exact flow commutator after transpose reversal of its scalar pairing.