Higher material differentiation of the actual pulled-back Jacobian. The coefficients below are derived from its evolution equation.

def AVenhance.Infra.Section4.amnrFlowMaterialCoefficient (b : AmnrSpace → Homogenization.Vec 2) : ℕ → Fin 2 → Fin 2 → AmnrSpace → ℝ

Coefficients of the repeated material derivative of a transported row. The order of indices agrees with amnr_flowGrad_material_equation.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Section4.amnrFlowMaterialCoefficient b 0 x✝¹ x✝ = fun (x : AVenhance.Infra.Section4.AmnrSpace) => if x✝¹ = x✝ then 1 else 0

theorem AVenhance.Infra.Section4.amnrFlowMaterialCoefficient_contDiff {b : AmnrSpace → Homogenization.Vec 2} (hb : ContDiff ℝ (↑⊤) b) (n : ℕ) (q p : Fin 2) : ContDiff ℝ (↑⊤) (amnrFlowMaterialCoefficient b n q p)

Coefficients of every finite material order are smooth because the velocity is smooth; no high regularity of the flow is used here.

theorem AVenhance.Infra.Section4.amnrWord_material_transport {b : AmnrSpace → Homogenization.Vec 2} (hb : ContDiff ℝ (↑⊤) b) (G : Fin 2 → AmnrSpace → ℝ) (hG : ∀ (p : Fin 2), ContDiff ℝ 1 (G p)) (heq : ∀ (p : Fin 2) (z : AmnrSpace), amnrOp b none (G p) z = ∑ q : Fin 2, G q z * amnrVelocityGradient b p q z) (n : ℕ) (p : Fin 2) : amnrWord b (List.replicate n none) (G p) = fun (z : AmnrSpace) => ∑ q : Fin 2, G q z * amnrFlowMaterialCoefficient b n q p z

Repeated material derivatives are explicit finite combinations of the original row and the derived coefficients. Joint C¹ of the row suffices.