Ordered spatial derivatives

An ordered list of coordinate directions defines a classical iterated spatial derivative. This notation supports finite-order transport commutator identities in the Sobolev energy argument.

def CKN.Leray.regularisedOrderedSpatialDerivative : List (Fin 3) → (Foundation.Parabolic.Vec3 → ℝ) → Foundation.Parabolic.Vec3 → ℝ

Classical derivatives applied in the order of a list of coordinate directions.

Equations

• CKN.Leray.regularisedOrderedSpatialDerivative [] x✝ = x✝
• CKN.Leray.regularisedOrderedSpatialDerivative (i :: is) x✝ = fun (x : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ (CKN.Leray.regularisedOrderedSpatialDerivative is x✝) x) (CKN.basisVec i)

theorem CKN.Leray.regularisedOrderedSpatialDerivative_contDiff (f : Foundation.Parabolic.Vec3 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (α : List (Fin 3)) : ContDiff ℝ (↑⊤) (regularisedOrderedSpatialDerivative α f)

Every ordered spatial derivative of a smooth scalar field remains smooth.

theorem CKN.Leray.regularisedOrderedSpatialDerivative_comm_spatialDerivative (f : Foundation.Parabolic.Vec3 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (α : List (Fin 3)) (i : Fin 3) (x : Foundation.Parabolic.Vec3) : regularisedOrderedSpatialDerivative α (fun (y : Foundation.Parabolic.Vec3) => (fderiv ℝ f y) (basisVec i)) x = (fderiv ℝ (regularisedOrderedSpatialDerivative α f) x) (basisVec i)

A coordinate derivative commutes with an ordered finite derivative of an all-order smooth scalar field.