Pressure Gradient SWS

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

The p₁ slot is supplied by the completed weak-gradient extension. This adapter deliberately consumes the D15 existential and never differentiates the literal first-potential representative.

theorem CKN.Core.Step4.pressure_slice_bound_of_riesz_weak_extension {B B' : Set Foundation.Parabolic.Vec3} (hB : IsOpen B) {p H gh G : Foundation.Parabolic.Vec3 → ℝ} {i : Fin 3} {ρ C : ℝ} (hP1 : ∀ (i : Fin 3) (G : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume → HasCompactSupport G → ∃ (D : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3), MeasureTheory.MemLp D (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ∧ (∀ (j : Fin 3) (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Foundation.Parabolic.Vec3), pressureNewtonianDerivativePotential i G x * spatialDeriv ψ j x = -∫ (x : Foundation.Parabolic.Vec3), D x j * ψ x) ∧ MeasureTheory.eLpNorm D (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ≤ ENNReal.ofReal C * MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) {k : Fin 3} (hG : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hGc : HasCompactSupport G) (hrep : p =ᵐ[MeasureTheory.volume.restrict B] pressureNewtonianDerivativePotential i G + H) (hH : HasWeakPartialDerivOn B k H gh) (hPloc : MeasureTheory.LocallyIntegrableOn (pressureNewtonianDerivativePotential i G) B MeasureTheory.volume) (hHloc : MeasureTheory.LocallyIntegrableOn H B MeasureTheory.volume) (hghloc : MeasureTheory.LocallyIntegrableOn gh B MeasureTheory.volume) (hgh : MeasureTheory.eLpNorm gh (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B') ≤ ENNReal.ofReal C * ENNReal.ofReal (ρ ^ (-1 / 2)) * MeasureTheory.eLpNorm p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict B)) : ∃ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrableOn g B MeasureTheory.volume ∧ HasWeakPartialDerivOn B k p g ∧ MeasureTheory.eLpNorm g (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B') ≤ ENNReal.ofReal C * (MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume + ENNReal.ofReal (ρ ^ (-1 / 2)) * MeasureTheory.eLpNorm p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict B))

The solution-level local decomposition used by the slice gradient route. The harmonic-gradient estimate is deliberately not folded into this bridge: the harmonic slice producer supplies that estimate separately.

theorem CKN.Core.Step4.pressure_slice_representation_of_sws {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), (fun (x : Foundation.Parabolic.Vec3) => p (x, s)) =ᵐ[MeasureTheory.volume.restrict (euclideanBall z.1 (13 * ρ / 20))] pressureP1 (mollifiedBallCutoff z.1 hρ) u (fun (t : ℝ) (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j) p f s + harmonicPressurePart (mollifiedBallCutoff z.1 hρ) u (fun (t : ℝ) (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j) p s + (pressureP7 (mollifiedBallCutoff z.1 hρ) f s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s) ∧ Foundation.Heat.WeaklyHarmonicOn (euclideanBall z.1 (13 * ρ / 20)) (harmonicPressurePart (mollifiedBallCutoff z.1 hρ) u (fun (t : ℝ) (j : Fin 3) => ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j) p s)