Tail

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

theorem CKN.Foundation.Parabolic.Morrey.cylinderAbsIntegral_le_morreyNorm {q : ℝ} (hq : 1 ≤ q) {f : ParabolicPoint → ℝ} : AEMeasurable f MeasureTheory.volume → ∀ (z : ParabolicPoint) {r : ℝ} (hr : 0 < r), ∫⁻ (w : ParabolicPoint) in parabolicCylinder z.1 z.2 r, ENNReal.ofReal |f w| ≤ ENNReal.ofReal r ^ (5 * (1 - 1 / q)) * morreyNorm 1 q f

The absolute integral on a positive cylinder is controlled by its Morrey norm.

theorem CKN.Foundation.Parabolic.Morrey.exists_positive_shell {z w : ParabolicPoint} {R : ℝ} (hR : 0 < R) (hRρ : R ≤ parabolicRho₂ z w) : ∃ (k : ℕ), w ∈ parabolicRieszShell R (↑k) z

def CKN.Foundation.Parabolic.Morrey.positiveShell (R : ℝ) (n : ℕ) (z : ParabolicPoint) : Set ParabolicPoint

Nonnegative-index parabolic shell for the far-field Morrey estimate.

Equations

• CKN.Foundation.Parabolic.Morrey.positiveShell R n z = CKN.Foundation.Parabolic.Morrey.parabolicRieszShell R (↑n) z

noncomputable def CKN.Foundation.Parabolic.Morrey.parabolicTailKernelConstant (β q : ℝ) : ENNReal

The dyadic constant used by the Morrey tail estimate.

Equations

• CKN.Foundation.Parabolic.Morrey.parabolicTailKernelConstant β q = ∑' (n : ℕ), ENNReal.ofReal 2 ^ (↑n * (β - 5 / q) + 2 * (5 * (1 - 1 / q)))

theorem CKN.Foundation.Parabolic.Morrey.parabolicRieszKernel_tail_le {β q : ℝ} (hβ : 0 < β) (hβ5 : β < 5) (hq : 1 ≤ q) (hβq : β * q < 5) {R : ℝ} (hR : 0 < R) {f : ParabolicPoint → ℝ} (hf : AEMeasurable f MeasureTheory.volume) (z : ParabolicPoint) : ∫⁻ (w : ParabolicPoint) in {w : ParabolicPoint | R ≤ parabolicRho₂ z w}, parabolicRieszKernel β z w * ENNReal.ofReal |f w| ≤ parabolicTailKernelConstant β q * ENNReal.ofReal R ^ (β - 5 / q) * morreyNorm 1 q f