: the Piola column lemma. For a constant matrix P, the matrix field
κ I + F_kᵀ P (with F_k the l_k flow gradient) has zero column divergence, so the
divergence of (κ I + F_kᵀ P) V is the Frobenius contraction with ∇V.
theorem
AVenhance.Infra.Section5.LeftJacobian.flowGradK_transpose_eq_rowCofactor
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(k : ℤ)
(t : ℝ)
(y : Homogenization.Vec 2)
:
(flowGradK I hΦ m k t y).transpose = rowCofactor (gradMatrix (I.xFlowInv hΦ m (lIdx β I.Λ m k) t) y)
The transposed l_k flow gradient is the row cofactor of the inverse-flow Jacobian.
theorem
AVenhance.Infra.Section5.LeftJacobian.piola_column_hasFDerivAt
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(k : ℤ)
(t : ℝ)
(P : Matrix (Fin 2) (Fin 2) ℝ)
(κm : ℝ)
(x : Homogenization.Vec 2)
:
∃ (LA : Fin 2 → Fin 2 → Homogenization.Vec 2 →L[ℝ] ℝ),
(∀ (i j : Fin 2),
HasFDerivAt (fun (y : Homogenization.Vec 2) => (κm • 1 + (flowGradK I hΦ m k t y).transpose * P) i j) (LA i j)
x) ∧ ∀ (j : Fin 2), ∑ i : Fin 2, (LA i j) (Homogenization.basisVec i) = 0
The entries of κ I + F_kᵀ P are differentiable, with zero column divergence.
theorem
AVenhance.Infra.Section5.LeftJacobian.matDiv_piola_column
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(k : ℤ)
(t : ℝ)
(P : Matrix (Fin 2) (Fin 2) ℝ)
(κm : ℝ)
(x : Homogenization.Vec 2)
:
theorem
AVenhance.Infra.Section5.LeftJacobian.vecDiv_piola_mulVec
{β : ℝ}
(I : Ingredients β)
{Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ}
(hΦ : IsStreamSeq I Φ)
(m : ℕ)
(k : ℤ)
(t : ℝ)
(P : Matrix (Fin 2) (Fin 2) ℝ)
(κm : ℝ)
(V : Homogenization.Vec 2 → Homogenization.Vec 2)
(x : Homogenization.Vec 2)
(hV : DifferentiableAt ℝ V x)
:
Divergence of (κ I + F_kᵀ P) V is the Frobenius contraction with ∇V.