Piola push-forward for the row-Jacobian convention used by gradMatrix.

The cofactor-divergence identity is kept as an explicit hypothesis until the spatial Piola calculation for the inverse flow is supplied. The determinant-one input is separate and follows from Liouville once the stream velocity's classical divergence-free identity is available.

def AVenhance.Infra.Section5.rowCofactor (G : Matrix (Fin 2) (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ

Cofactor matrix for a row-Jacobian: adjugate(Gᵀ).

Equations

• AVenhance.Infra.Section5.rowCofactor G = G.transpose.adjugate

theorem AVenhance.Infra.Section5.vecDiv_rowCofactorPiola {M g : Homogenization.Vec 2 → Homogenization.Vec 2} {x : Homogenization.Vec 2} {LM Lg : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} {LQ : Fin 2 → Fin 2 → Homogenization.Vec 2 →L[ℝ] ℝ} (hM : HasFDerivAt M LM x) (hg : HasFDerivAt g Lg (M x)) (hQ : ∀ (i j : Fin 2), HasFDerivAt (fun (y : Homogenization.Vec 2) => rowCofactor (gradMatrix M y) i j) (LQ i j) x) (hPiolaDiv : ∀ (j : Fin 2), ∑ i : Fin 2, (LQ i j) (Homogenization.basisVec i) = 0) (hdet : (gradMatrix M x).det = 1) : vecDiv (fun (y : Homogenization.Vec 2) => (rowCofactor (gradMatrix M y)).mulVec (g (M y))) x = vecDiv g (M x)

The cofactor Piola formula in the repository's row-Jacobian convention. The derivative of the cofactor columns vanishes by the Piola identity; the chain contraction is reduced to the Jacobian determinant algebraically.

theorem AVenhance.Infra.Section5.xFlowInv_gradMatrix_det_eq_one {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (hdiv : ∀ (r : ℝ) (y : Homogenization.Vec 2), Flow.spatialDivergence (streamVel (Φ (m - 1))) r y = 0) : (gradMatrix (I.xFlowInv hΦ m l t) x).det = 1

The Liouville determinant-one bridge for a inverse-flow slice. Only classical divergence-freeness of the preceding stream velocity is explicit; smoothness and the flow characterization come from IsStreamSeq.

theorem AVenhance.Infra.Section5.xFlowInv_cofactorPiola {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (x : Homogenization.Vec 2) {g : Homogenization.Vec 2 → Homogenization.Vec 2} {LM Lg : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} {LQ : Fin 2 → Fin 2 → Homogenization.Vec 2 →L[ℝ] ℝ} (hM : HasFDerivAt (I.xFlowInv hΦ m l t) LM x) (hg : HasFDerivAt g Lg (I.xFlowInv hΦ m l t x)) (hQ : ∀ (i j : Fin 2), HasFDerivAt (fun (y : Homogenization.Vec 2) => rowCofactor (gradMatrix (I.xFlowInv hΦ m l t) y) i j) (LQ i j) x) (hPiolaDiv : ∀ (j : Fin 2), ∑ i : Fin 2, (LQ i j) (Homogenization.basisVec i) = 0) (hdiv : ∀ (r : ℝ) (y : Homogenization.Vec 2), Flow.spatialDivergence (streamVel (Φ (m - 1))) r y = 0) : vecDiv (fun (y : Homogenization.Vec 2) => (rowCofactor (gradMatrix (I.xFlowInv hΦ m l t) y)).mulVec (g (I.xFlowInv hΦ m l t y))) x = vecDiv g (I.xFlowInv hΦ m l t x)

inverse-flow version of the cofactor push-forward. The cofactor divergence identity is an explicit premise (a Piola lemma); the unit determinant is supplied by the Liouville bridge above.