Near

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

Morrey

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

theorem CKN.Core.HeatPotential.morrey_cylinder_lp_bound {P θ : ℝ} (hP : 1 ≤ P) (hPθ : P ≤ θ) {f : Foundation.Parabolic.ParabolicPoint → ℝ} : AEMeasurable f MeasureTheory.volume → ∀ (z : Foundation.Parabolic.ParabolicPoint) {r : ℝ} (hr : 0 < r), Foundation.Parabolic.Morrey.cylinderPowerIntegral P f z r ^ (1 / P) ≤ ENNReal.ofReal r ^ (5 * (1 / P - 1 / θ)) * Foundation.Parabolic.Morrey.morreyNorm P θ f

The source block used for the local part of a heat potential. The radius is written with the gauge parabolicRho₂, whose time component is symmetric; this is the geometry needed for a genuine parabolic metric ball.

def CKN.Core.HeatPotential.heatPotentialNearSet (z : Foundation.Parabolic.ParabolicPoint) (r : ℝ) : Set Foundation.Parabolic.ParabolicPoint

Near region separated from the far shells at parabolic distance 64 * r.

Equations

• CKN.Core.HeatPotential.heatPotentialNearSet z r = {v : CKN.Foundation.Parabolic.ParabolicPoint | CKN.Foundation.Parabolic.Morrey.parabolicRho₂ z v < 64 * r}