Shared symmetry of second spatial derivatives.

theorem AVenhance.Infra.SpatialSecondDerivatives.coordinate_derivatives_commute {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ (↑⊤) f) (i j : Fin 2) (x : Homogenization.Vec 2) : spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad f y i) x j = spaceGrad (fun (y : Homogenization.Vec 2) => spaceGrad f y j) x i

Smooth coordinate derivatives commute at every spatial point.