Every material commutator contains a positive-order velocity jet.
theorem
AVenhance.Infra.Section4.iterateWordMaterialError_lower_velocity
{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)
(w : List (Fin 2))
(x : Homogenization.Vec 2)
:
iterateWordMaterialError (fun (z : AmnrSpace) => b z.1 z.2) w (fun (z : AmnrSpace) => u z.1 z.2) (t, x) = ∑ j : Fin 2,
(List.map
(fun (p : List (Fin 2) × List (Fin 2)) =>
iterateSpatialWord p.1 (fun (y : Homogenization.Vec 2) => b t y j) x * spaceGrad (iterateSpatialWord p.2 (u t)) x j)
(List.filter (fun (p : List (Fin 2) × List (Fin 2)) => !p.1.isEmpty) (iterateSpatialSplits w))).sum
The velocity commutator has exactly the nonprincipal ordered splits.