Matrix-vector divergence with column divergence and row Jacobians.

theorem AVenhance.Infra.Section5.vecDiv_matrixMulVec_frob {A : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {V : Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} {LA : Fin 2 → Fin 2 → Homogenization.Vec 2 →L[ℝ] ℝ} {LV : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hA : ∀ (i j : Fin 2), HasFDerivAt (fun (y : Homogenization.Vec 2) => A y i j) (LA i j) x) (hV : HasFDerivAt V LV x) : vecDiv (fun (y : Homogenization.Vec 2) => (A y).mulVec (V y)) x = Homogenization.vecDot (matDiv A x) (V x) + frob (A x) (gradMatrix V x)

The divergence product rule in the matrix convention used by the corrector flux: column divergence pairs with the vector, while the remaining contribution is the Frobenius contraction with its row-Jacobian.