Morrey Vec Mem #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
def
CKN.morreyVecMem
(P τ : ℝ)
(S : Set Foundation.Parabolic.ParabolicPoint)
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
:
Componentwise parabolic Morrey membership used by paper label def:parabolic-morrey.
Equations
- CKN.morreyVecMem P τ S u = ∀ (i : Fin 3), CKN.Foundation.Parabolic.Morrey.morreyBallNorm P τ (S.indicator fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => u z i) < ⊤