The directional derivative of a vector field as a vector field

For a vector field v : Vec3 → Vec3 and a coordinate direction k, the field partialVec v k is ∂_k v, again a vector field on Vec3. It is introduced as a named definition, not as an inline nest of fderivs, because every second-order statement of the elliptic identity eq:aniso:closure:elliptic differentiates twice: written out, such a term is a lambda inside a lambda with no head symbol for the unifier to key on, and terms of that shape elaborate very badly. With the definition in place the unifier sees partialVec applied to arguments.

The file records that ∂_k v inherits smoothness and compact support from v, and that ∂_k commutes with both first-order differential operators of the identity:

• curlVec_partialVec — curl (∂_k v) = ∂_k (curl v);
• div_partialVec — div (∂_k v) = ∂_k (div v);
• sum_sq_partialVec_eq — summing |∇(∂_k v)|² over k recovers the full Hessian energy |∇²v|².

All three rest on the symmetry of the second derivative, which is the fderiv_fderiv_comp_symm of CIV.Analysis.DivCurl.

noncomputable def CIV.partialVec (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (k : Fin 3) (x : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.Vec3

The derivative of the vector field v in the coordinate direction k, as a vector field: partialVec v k x i = ∂_k v_i (x).

Equations

• CIV.partialVec v k x i = (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => v y i) x) (CKN.basisVec k)

theorem CIV.partialVec_apply (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (k : Fin 3) (x : CKN.Foundation.Parabolic.Vec3) (i : Fin 3) : partialVec v k x i = (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => v y i) x) (CKN.basisVec k)

The controlled unfolding channel for partialVec: its i-th component is the k-th partial derivative of the i-th component of v.

theorem CIV.contDiff_partialVec (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hv : ContDiff ℝ (↑⊤) v) (k : Fin 3) : ContDiff ℝ (↑⊤) (partialVec v k)

∂_k v is smooth whenever v is.

theorem CIV.hasCompactSupport_partialVec (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hsupp : HasCompactSupport v) (k : Fin 3) : HasCompactSupport (partialVec v k)

∂_k v has compact support whenever v does: off the support of v the field vanishes on a whole neighbourhood, so all of its derivatives vanish there.

theorem CIV.curlVec_partialVec (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hv : ContDiff ℝ (↑⊤) v) (k : Fin 3) (x : CKN.Foundation.Parabolic.Vec3) : curlVec (partialVec v k) x = fun (i : Fin 3) => (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => curlVec v y i) x) (CKN.basisVec k)

curl commutes with ∂_k.

theorem CIV.div_partialVec (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hv : ContDiff ℝ (↑⊤) v) (k : Fin 3) (x : CKN.Foundation.Parabolic.Vec3) : ∑ j : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => partialVec v k y j) x) (CKN.basisVec j) = (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, (fderiv ℝ (fun (z : CKN.Foundation.Parabolic.Vec3) => v z j) y) (CKN.basisVec j)) x) (CKN.basisVec k)

div commutes with ∂_k.

theorem CIV.sum_sq_partialVec_eq (v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hv : ContDiff ℝ (↑⊤) v) (x : CKN.Foundation.Parabolic.Vec3) : ∑ k : Fin 3, ∑ i : Fin 3, ∑ j : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => partialVec v k y i) x) (CKN.basisVec j) ^ 2 = ∑ i : Fin 3, ∑ j : Fin 3, ∑ k : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ (fun (z : CKN.Foundation.Parabolic.Vec3) => v z i) y) (CKN.basisVec j)) x) (CKN.basisVec k) ^ 2

Summing the gradient energy of ∂_k v over the three directions k recovers the full Hessian energy of v.