Spatial Partial #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
noncomputable def
CKN.spatialPartial
(g : Foundation.Parabolic.ParabolicPoint → ℝ)
(i : Fin 3)
(z : Foundation.Parabolic.ParabolicPoint)
:
Factor-wise spatial derivative on the ordinary product space described in docs/DESIGN_NOTES.md.
Equations
- CKN.spatialPartial g i z = (fderiv ℝ (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, z.2)) z.1) (CKN.basisVec i)