Ball Mem Lp #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.memLp_euclideanBall_of_continuous
{d : ℕ}
{x₀ : Vec d}
{r : ℝ}
(hr : 0 < r)
{f : Vec d → ℝ}
(hf : Continuous f)
(p : ENNReal)
:
MeasureTheory.MemLp f p (MeasureTheory.volume.restrict (euclideanBall x₀ r))
A continuous function on Vec d is L^p with respect to the volume measure
restricted to any open Euclidean ball of positive radius, for every exponent p.