Actual spatial/material commutators for the T and flow estimates.

theorem AVenhance.Infra.Section4.amnrOp_space {b : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} {z : AmnrSpace} (hf : DifferentiableAt ℝ f z) (i : Fin 2) : amnrOp b (some i) f z = spaceGrad (fun (y : Homogenization.Vec 2) => f (z.1, y)) z.2 i

The spatial directional operator equals the spatial gradient.

theorem AVenhance.Infra.Section4.amnrFDeriv_vertical (f : AmnrSpace → ℝ) (z : AmnrSpace) (v : Homogenization.Vec 2) : (fderiv ℝ f z) (0, v) = ∑ p : Fin 2, v p * (fderiv ℝ f z) (0, Homogenization.basisVec p)

Expansion of a vertical differential in the actual two-coordinate basis.

theorem AVenhance.Infra.Section4.amnr_material_spatial_commutator {b : AmnrSpace → Homogenization.Vec 2} {f : AmnrSpace → ℝ} {z : AmnrSpace} (hb : DifferentiableAt ℝ b z) (hf : ContDiffAt ℝ 2 f z) (i : Fin 2) : amnrOp b none (amnrOp b (some i) f) z = amnrOp b (some i) (amnrOp b none f) z - ∑ p : Fin 2, amnrVelocityGradient b p i z * amnrOp b (some p) f z

The material/spatial commutator in source coordinates, with the precise transpose contraction on the gradient.