Explicit spatial Leibniz expansions for the actual increment forcing. The differentiated forcing is computed rather than supplied as an equation.

theorem AVenhance.Infra.Section4.iterate_matrix_forcing_formula {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {v : Homogenization.Vec 2 → ℝ} (hA : ContDiff ℝ (↑⊤) A) (hv : ContDiff ℝ (↑⊤) v) (x : Homogenization.Vec 2) : vecDiv (fun (y : Homogenization.Vec 2) => (A y).mulVec (spaceGrad v y)) x = ∑ i : Fin 2, ∑ j : Fin 2, (spaceGrad (fun (y : Homogenization.Vec 2) => A y i j) x i * spaceGrad v x j + A x i j * spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad v y j) x i)

Divergence of the coefficient/gradient flux, with both Leibniz terms.

theorem AVenhance.Infra.Section4.IteratesForcingGradient.forcing_product_abs_le {a b D G : ℝ} (ha : |a| ≤ D) (hb : |b| ≤ G) : |a * b| ≤ D * G

theorem AVenhance.Infra.Section4.IteratesForcingGradient.forcing_four_abs_le (a b c d : ℝ) : |a + b + c + d| ≤ |a| + |b| + |c| + |d|

theorem AVenhance.Infra.Section4.IteratesForcingGradient.forcing_four_sq_le (a b c d : ℝ) : (a + b + c + d) ^ 2 ≤ 4 * (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2)