Iterates Material Gradient Commutator

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_material_gradient_commutator {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {u : ℝ → Homogenization.Vec 2 → ℝ} (hb : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => b z.1 z.2) (Set.Ioi 0 ×ˢ Set.univ)) (hu : ContDiffOn ℝ (↑⊤) (fun (z : AmnrSpace) => u z.1 z.2) (Set.Ioi 0 ×ˢ Set.univ)) {t : ℝ} (ht : 0 < t) (x : Homogenization.Vec 2) (j : Fin 2) : amnrMaterial b (fun (s : ℝ) (y : Homogenization.Vec 2) => spaceGrad (u s) y j) t x = spaceGrad (amnrMaterial b u t) x j - (gradMatrix (b t) x).mulVec (spaceGrad (u t) x) j

Material differentiation of an actual gradient keeps the one-jet drift commutator with its exact sign and the gradMatrix convention.