Spatial Second Partial #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
noncomputable def
CKN.spatialSecondPartial
(g : Foundation.Parabolic.ParabolicPoint → ℝ)
(i j : Fin 3)
(z : Foundation.Parabolic.ParabolicPoint)
:
The iterated spatial derivative used in the local energy inequality.
Equations
- CKN.spatialSecondPartial g i j z = CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial g i w) j z