Symmetry of classical spatial second derivatives

Twice continuously differentiable scalar fields have commuting coordinate second derivatives. This identifies the leading differentiated transport term with the transport of a first derivative.

theorem CKN.Leray.regularised_mixedSecondPartial_comm (v : Foundation.Parabolic.Vec3 → ℝ) (hv : ContDiff ℝ 2 v) (x : Foundation.Parabolic.Vec3) (i j : Fin 3) : (fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => (fderiv ℝ v y) (basisVec i)) x) (basisVec j) = (fderiv ℝ (fun (y : Foundation.Parabolic.Vec3) => (fderiv ℝ v y) (basisVec j)) x) (basisVec i)

Coordinate second derivatives commute for a twice continuously differentiable scalar field.