Coordinate Piola formula for a corrected push-forward matrix.

theorem AVenhance.Infra.Section5.vecDiv_correctedPiola {M g : Homogenization.Vec 2 → Homogenization.Vec 2} {Q : Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ} {x : Homogenization.Vec 2} {LQ : Fin 2 → Fin 2 → Homogenization.Vec 2 →L[ℝ] ℝ} {LM Lg : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hQ : ∀ (i j : Fin 2), HasFDerivAt (fun (y : Homogenization.Vec 2) => Q y i j) (LQ i j) x) (hM : HasFDerivAt M LM x) (hg : HasFDerivAt g Lg (M x)) (hPiolaDiv : ∀ (j : Fin 2), ∑ i : Fin 2, (LQ i j) (Homogenization.basisVec i) = 0) (hPiolaChain : ∀ (j k : Fin 2), ∑ i : Fin 2, Q x i j * LM (Homogenization.basisVec i) k = if j = k then 1 else 0) : vecDiv (fun (y : Homogenization.Vec 2) => (Q y).mulVec (g (M y))) x = vecDiv g (M x)

The divergence of Q (g ∘ M) is the pulled-back divergence of g when the columns of Q are divergence-free and Q is the inverse chain matrix. These are the two coordinate Piola identities needed from a smooth volume-preserving change of variables.