All-order explicit gradient of the forcing, with exact binomial grouping.

theorem AVenhance.Infra.Section4.IteratesWordForcingGradient.iterate_abs_list_sum {α : Type u_1} (P : List α) (f : α → ℝ) : |(List.map f P).sum| ≤ (List.map (fun (p : α) => |f p|) P).sum

theorem AVenhance.Infra.Section4.iterate_word_forcing_gradient_formula {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {v : Homogenization.Vec 2 → ℝ} (hA : ContDiff ℝ (↑⊤) A) (hv : ContDiff ℝ (↑⊤) v) (w : List (Fin 2)) (x : Homogenization.Vec 2) (k : Fin 2) : spaceGrad (iterateSpatialWord w (vecDiv fun (y : Homogenization.Vec 2) => (A y).mulVec (spaceGrad v y))) x k = ∑ i : Fin 2, ∑ j : Fin 2, (List.map (fun (p : List (Fin 2) × List (Fin 2)) => iterateSpatialWord p.1 (fun (y : Homogenization.Vec 2) => A y i j) x * spaceGrad (iterateSpatialWord p.2 v) x j) (iterateSpatialSplits (i :: k :: w))).sum

Differentiating the actual forcing once more is the full Leibniz expansion with two extra derivative letters: one for divergence and one for the gradient.