Ordered coordinate and Fréchet derivatives

An ordered list of coordinate derivatives is the Fréchet derivative applied to its corresponding tuple of coordinate basis vectors.

def CKN.Leray.regularisedListBasisTuple (α : List (Fin 3)) : Fin α.length → Foundation.Parabolic.Vec3

The tuple of coordinate basis vectors associated with an ordered list.

Equations

• CKN.Leray.regularisedListBasisTuple α k = CKN.basisVec (α.get k)

theorem CKN.Leray.regularisedListBasisTuple_cons (i : Fin 3) (α : List (Fin 3)) : regularisedListBasisTuple (i :: α) = Fin.cons (basisVec i) (regularisedListBasisTuple α)

Prepending a direction prepends its basis vector to the tuple.

theorem CKN.Leray.regularisedOrderedSpatialDerivative_eq_iteratedFDeriv (f : Foundation.Parabolic.Vec3 → ℝ) (hf : ContDiff ℝ (↑⊤) f) (α : List (Fin 3)) (x : Foundation.Parabolic.Vec3) : regularisedOrderedSpatialDerivative α f x = (iteratedFDeriv ℝ α.length f x) (regularisedListBasisTuple α)

An ordered coordinate derivative equals the matching Fréchet derivative evaluated on its coordinate basis tuple.