Vec Mem

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.morreyVecMem_mono {P τ : ℝ} (hP : 0 ≤ P) {S S' : Set Foundation.Parabolic.ParabolicPoint} (hS : S' ⊆ S) {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (h : morreyVecMem P τ S u) : morreyVecMem P τ S' u

Monotonicity of componentwise parabolic Morrey membership under subset restriction. If u has finite Morrey norm on S, then it also has finite Morrey norm on any subset S' ⊆ S.