Potential Local Lp Exponents

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

theorem CKN.Foundation.Euclidean.eLpNorm_le_eLpNorm_mul_rpow_measure_of_support {G : Parabolic.Vec3 → ℝ} {s : Set Parabolic.Vec3} (hs : MeasurableSet s) {p q : ENNReal} (hpq : p ≤ q) (hmeas : MeasureTheory.AEStronglyMeasurable G MeasureTheory.volume) (hzero : ∀ y ∉ s, G y = 0) : MeasureTheory.eLpNorm G p MeasureTheory.volume ≤ MeasureTheory.eLpNorm G q MeasureTheory.volume * MeasureTheory.volume s ^ (1 / p.toReal - 1 / q.toReal)

Hölder on a finite-measure support: a function vanishing off a measurable set s has its L^p size controlled by its L^q size for p ≤ q, with the explicit factor volume s ^ (1 / p - 1 / q).

theorem CKN.Foundation.Euclidean.memLp_of_memLp_of_support_closedBall {G : Parabolic.Vec3 → ℝ} {R : ℝ} {p q : ENNReal} (hpq : p ≤ q) (hG : MeasureTheory.MemLp G q MeasureTheory.volume) (hzero : ∀ y ∉ Metric.closedBall 0 R, G y = 0) : MeasureTheory.MemLp G p MeasureTheory.volume

Data supported in a closed ball and of class L^q is of class L^p for every p ≤ q.

theorem CKN.Foundation.Euclidean.memLp_six_fifths_of_memLp_ofReal {G : Parabolic.Vec3 → ℝ} {R q : ℝ} (hq : 6 / 5 ≤ q) (hG : MeasureTheory.MemLp G (ENNReal.ofReal q) MeasureTheory.volume) (hzero : ∀ y ∉ Metric.closedBall 0 R, G y = 0) : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume

The L^(6/5) instance used by the Young estimate for the Newtonian potential: compactly supported data of class L^q with 6 / 5 ≤ q is of class L^(6/5).

theorem CKN.Foundation.Euclidean.integrable_of_memLp_ofReal_of_support {G : Parabolic.Vec3 → ℝ} {R q : ℝ} (hq : 1 ≤ q) (hG : MeasureTheory.MemLp G (ENNReal.ofReal q) MeasureTheory.volume) (hzero : ∀ y ∉ Metric.closedBall 0 R, G y = 0) : MeasureTheory.Integrable G MeasureTheory.volume

Compactly supported data of class L^q with 1 ≤ q is integrable.