Coordinate directional derivative on a time slice

axisDeriv j is the directional derivative along the j-th coordinate axis on a spatial slice {t} fixed. The lemmas below transport the repository's spatialPartial / multiPartial derivatives — which are functions of a full ParabolicPoint — to iterated Fréchet derivatives of the spatial restriction h(·, t). This is the form consumed by the analyticity criterion (thm:analytic:interior).

noncomputable def CIV.axisDeriv (j : Fin 3) (G : CKN.Foundation.Parabolic.Vec3 → ℝ) : CKN.Foundation.Parabolic.Vec3 → ℝ

The directional derivative of a function of the space variable along a coordinate axis.

Equations

• CIV.axisDeriv j G x = (fderiv ℝ G x) (CKN.basisVec j)

theorem CIV.slice_spatialPartial_iterate (h : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (j : Fin 3) (m : ℕ) (t : ℝ) : (fun (x : CKN.Foundation.Parabolic.Vec3) => (fun (k : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) => CKN.spatialPartial k j)^[m] h (x, t)) = (axisDeriv j)^[m] fun (x : CKN.Foundation.Parabolic.Vec3) => h (x, t)

Iterating spatialPartial on a time slice produces iterated axisDeriv on the spatial restriction.

theorem CIV.multiPartial_slice (h : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (α : Fin 3 → ℕ) (t : ℝ) : (fun (x : CKN.Foundation.Parabolic.Vec3) => multiPartial h α (x, t)) = (axisDeriv 0)^[α 0] ((axisDeriv 1)^[α 1] ((axisDeriv 2)^[α 2] fun (x : CKN.Foundation.Parabolic.Vec3) => h (x, t)))

The multi-index spatial derivative on a time slice factors as iterated axisDeriv applied in coordinate order.