Local Lp #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
def
CKN.localLp
(E : Set Foundation.Parabolic.ParabolicPoint)
(p : ℝ)
(g : Foundation.Parabolic.ParabolicPoint → ℝ)
:
Local scalar Lp membership used by paper label def:sws.
Equations
- CKN.localLp E p g = MeasureTheory.MemLp g (ENNReal.ofReal p) (MeasureTheory.volume.restrict E)