Mem Lp Three Halves Lift

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

theorem CKN.memLp_three_halves_of_restrict_of_tsupport_subset {g : Foundation.Parabolic.Vec3 → ℝ} {B : Set Foundation.Parabolic.Vec3} [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict B)] (hB : MeasureTheory.MemLp g (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict B)) (hBsupport : tsupport g ⊆ B) : MeasureTheory.MemLp g (ENNReal.ofReal (3 / 2)) MeasureTheory.volume

A function in L^{3/2} of a finite-measure ball, with topological support contained in that ball, is in L^{3/2} of the whole space.