LeftJacobian the left-Jacobian form: the Piola coefficient identity.

K + s⁺ = Σ_l ξ̂_l [κ F_l + F_lᵀ (K - κ) F_l] for a generic matrix K (no scalar structure), and its action on ∇T.

theorem AVenhance.Infra.Section5.LeftJacobian.tsum_hatXiML_smul_eq_sum {β : ℝ} (I : Ingredients β) {α : Type u_1} [AddCommMonoid α] [TopologicalSpace α] [Module ℝ α] (m : ℕ) (hm : 1 ≤ m) (t : ℝ) (f : ℤ → α) : ∑' (l : ℤ), I.hatXiML m l t • f l = ∑ l ∈ ⋯.toFinset, I.hatXiML m l t • f l

A ξ̂-weighted tsum is the finite sum over the support of ξ̂.

theorem AVenhance.Infra.Section5.LeftJacobian.sum_hatXiML_support {β : ℝ} (I : Ingredients β) (m : ℕ) (hm : 1 ≤ m) (t : ℝ) : ∑ l ∈ ⋯.toFinset, I.hatXiML m l t = 1

The ξ̂ weights sum to one over their finite support.

theorem AVenhance.Infra.Section5.LeftJacobian.piola_matrix_identity (K F : Matrix (Fin 2) (Fin 2) ℝ) (κ : ℝ) : K + K * (F - 1) + (F.transpose - 1) * (K - κ • 1) * F = κ • F + F.transpose * (K - κ • 1) * F

The matrix identity behind the Piola flux: K + K(F - 1) + (Fᵀ - 1)(K - κ)F = κF + Fᵀ(K - κ)F.

theorem AVenhance.Infra.Section5.LeftJacobian.Kmat_add_sMatPlus_eq_coarseFluxPlus {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm t : ℝ) (x : Homogenization.Vec 2) : I.Kmat κm m t + sMatPlus I hΦ m κm t x = coarseFluxPlus I hΦ m κm t x

theorem AVenhance.Infra.Section5.LeftJacobian.Kmat_add_sMatPlus_mulVec {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (hm : 1 ≤ m) (κm t : ℝ) (x : Homogenization.Vec 2) (T : ℝ → Homogenization.Vec 2 → ℝ) : (I.Kmat κm m t + sMatPlus I hΦ m κm t x).mulVec (spaceGrad (T t) x) = ∑' (l : ℤ), I.hatXiML m l t • (κm • I.flowGrad hΦ m l t x + (I.flowGrad hΦ m l t x).transpose * (I.Kmat κm m t - κm • 1) * I.flowGrad hΦ m l t x).mulVec (spaceGrad (T t) x)