RelativeError: the two-dimensional cofactor Piola identity

theorem AVenhance.Infra.Section5.RelativeError.TransportPiola.mixed_spaceGrad_commute {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 2 f) (x : Homogenization.Vec 2) : spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad f y 0) x 1 = spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad f y 1) x 0

theorem AVenhance.Infra.Section5.RelativeError.TransportPiola.spatialGradientMatrix_entry_eq_spaceGrad {Y : Homogenization.Vec 2 → Homogenization.Vec 2} (hY : ContDiff ℝ 1 Y) (x : Homogenization.Vec 2) (i j : Fin 2) : FaaDiBruno.spatialGradientMatrix Y x i j = spaceGrad (fun (y : Homogenization.Vec 2) => Y y i) x j

theorem AVenhance.Infra.Section5.RelativeError.cofactorTranspose_gradient_columns_divergence_free {Y : Homogenization.Vec 2 → Homogenization.Vec 2} (hY : ContDiff ℝ 2 Y) (x : Homogenization.Vec 2) (j : Fin 2) : ∑ i : Fin 2, (fderiv ℝ (fun (z : Homogenization.Vec 2) => FaaDiBruno.flowMatrixCofactorTranspose (FaaDiBruno.spatialGradientMatrix Y z) i j) x) (Homogenization.basisVec i) = 0

The columns of the transposed cofactor of a two-dimensional gradient are divergence-free. This is the classical Piola identity, proved by equality of mixed second derivatives.

theorem AVenhance.Infra.Section5.RelativeError.TransportPiola.continuousLinearMap_det_formula (L : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) : L.det = L (Homogenization.basisVec 0) 0 * L (Homogenization.basisVec 1) 1 - L (Homogenization.basisVec 1) 0 * L (Homogenization.basisVec 0) 1

theorem AVenhance.Infra.Section5.RelativeError.cofactorTranspose_gradient_chain {Y : Homogenization.Vec 2 → Homogenization.Vec 2} (x : Homogenization.Vec 2) (hdet : (fderiv ℝ Y x).det = 1) (j k : Fin 2) : ∑ i : Fin 2, FaaDiBruno.flowMatrixCofactorTranspose (FaaDiBruno.spatialGradientMatrix Y x) i j * (fderiv ℝ Y x) (Homogenization.basisVec i) k = if j = k then 1 else 0

A determinant-one inverse Jacobian obeys the cofactor chain identity used to transform divergence under a volume-preserving flow.