Arbitrary-order actual velocity-Jacobian operator rates from the stream-regularity estimates.

theorem AVenhance.Infra.Section4.amnr_velocityJacobian_iteratedFDeriv_coordinate {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) (n : ℕ) (t : ℝ) (x : Homogenization.Vec 2) (v : Fin n → Homogenization.Vec 2) (i p : Fin 2) : ((iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => Flow.jointSpatialFDeriv b t y) x) v) (Homogenization.basisVec p) i = (iteratedFDeriv ℝ n (fun (y : Homogenization.Vec 2) => amnrVelocityGradient (fun (z : AmnrSpace) => b z.1 z.2) i p (t, y)) x) v

Spatial differentiation of the actual Jacobian commutes with its coordinate projection. This is an exact operator identity at every order.