Adams Endpoints

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

theorem CKN.Foundation.Parabolic.Morrey.parabolicRieszPotential_eq_zero_of_ae_eq_zero {β : ℝ} {f : ParabolicPoint → ℝ} (hzero : f =ᵐ[MeasureTheory.volume] 0) (z : ParabolicPoint) : parabolicRieszPotential β f z = 0

A potential vanishes when its input vanishes almost everywhere.

theorem CKN.Foundation.Parabolic.Morrey.ae_eq_zero_of_morreyNorm_eq_zero {q : ℝ} (hq : 1 ≤ q) {f : ParabolicPoint → ℝ} (hf : AEMeasurable f MeasureTheory.volume) (hN : morreyNorm 1 q f = 0) : f =ᵐ[MeasureTheory.volume] 0

A zero first-index Morrey seminorm forces global almost-everywhere vanishing.

theorem CKN.Foundation.Parabolic.Morrey.parabolicHedbergNearConstant_pos {β : ℝ} : 0 < parabolicHedbergNearConstant β

The near-field geometric constant is strictly positive.

theorem CKN.Foundation.Parabolic.Morrey.parabolicRieszPotential_hedberg' {β q : ℝ} (hβ : 0 < β) (hβ5 : β < 5) (hq : 1 ≤ q) (hβq : β * q < 5) {f : ParabolicPoint → ℝ} (hf : AEMeasurable f MeasureTheory.volume) {M : ParabolicPoint → ENNReal} (hM : IsParabolicMaximalMajorant f M) (z : ParabolicPoint) : parabolicRieszPotential β f z ≤ (parabolicHedbergNearConstant β + parabolicTailKernelConstant β q) * M z ^ (1 - β * q / 5) * morreyNorm 1 q f ^ (β * q / 5)

Hedberg's pointwise estimate, including zero and infinite endpoint data.