Actual Eulerian material differentiation of the pulled-back flow gradient.

theorem AVenhance.Infra.Section4.amnr_flowGrad_contDiff_one {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (k p : Fin 2) : ContDiff ℝ 1 fun (z : AmnrSpace) => I.flowGrad hΦ m l z.1 z.2 k p

The actual pulled-back Jacobian entry is jointly C¹ in Eulerian variables. This supplies its material differentiability rather than assuming it.

theorem AVenhance.Infra.Section4.amnr_flowGrad_material_equation {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (k p : Fin 2) (z : AmnrSpace) : amnrOp (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) none (fun (y : AmnrSpace) => I.flowGrad hΦ m l y.1 y.2 k p) z = ∑ q : Fin 2, I.flowGrad hΦ m l z.1 z.2 k q * amnrVelocityGradient (fun (y : AmnrSpace) => streamVel (Φ (m - 1)) y.1 y.2) p q z

Eulerian material differentiation of the actual flow gradient follows its variational equation, with the exact source row convention.