Local Vec Lp #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
def
CKN.localVecLp
(E : Set Foundation.Parabolic.ParabolicPoint)
(p : ℝ)
(g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
:
Componentwise local vector Lp membership used by paper label def:sws.
Equations
- CKN.localVecLp E p g = ∀ (i : Fin 3), CKN.localLp E p fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => g z i