Slice Selected Gradient Potential

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

The pressure-gradient section of the paper controls ∇p through the weak pairing against a compactly supported test function, as in display (3.5). The Newtonian derivative potential of a source field is the kernel representation of that weak gradient. This file records the integrability input that display (3.5) assumes, the local integrability of a finite sum of such potentials, and the passage from a per-coordinate Calderón–Zygmund bound to the corresponding bound for the potential of a vector-valued source.

theorem CKN.Core.Step4.memLp_six_fifths_integrable_of_hasCompactSupport {G : Foundation.Parabolic.Vec3 → ℝ} (hG : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hGc : HasCompactSupport G) : MeasureTheory.Integrable G MeasureTheory.volume

A function in L^{6/5} with compact support is integrable. This is the integrability input that display (3.5) of the pressure-gradient section takes for granted: the source of the Newtonian derivative potential is supported on a compact set of finite measure, so membership in L^{6/5} may be lowered to membership in L^1.

theorem CKN.Core.Step4.newtonianDerivativeSum_locallyIntegrable {V : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hV : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => V x i) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hVc : ∀ (i : Fin 3), HasCompactSupport fun (x : Foundation.Parabolic.Vec3) => V x i) : MeasureTheory.LocallyIntegrable (fun (x : Foundation.Parabolic.Vec3) => ∑ i : Fin 3, pressureNewtonianDerivativePotential i (fun (y : Foundation.Parabolic.Vec3) => V y i) x) MeasureTheory.volume

The sum over coordinates of the Newtonian derivative potentials of the components of a compactly supported vector field in L^{6/5} is locally integrable. This is the weak gradient field appearing on the left-hand side of display (3.5) of the pressure-gradient section, assembled coordinate by coordinate from its per-coordinate kernel representation.

theorem CKN.Core.Step4.newtonian_derivative_sum_weak_gradient_of_extension (C_CZ : ℝ) (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_CZ * MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) {V : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hV : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => V x i) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hVc : ∀ (i : Fin 3), HasCompactSupport fun (x : Foundation.Parabolic.Vec3) => V x i) : ∃ (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), (∑ i : Fin 3, pressureNewtonianDerivativePotential i (fun (y : Foundation.Parabolic.Vec3) => V y i) x) * spatialDeriv ψ j x = -∫ (x : Foundation.Parabolic.Vec3), D x j * ψ x) ∧ MeasureTheory.eLpNorm D (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ≤ ENNReal.ofReal C_CZ * ∑ i : Fin 3, MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => V x i) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume

Display (3.5) of the pressure-gradient section for a vector-valued source: given a per-coordinate Calderón–Zygmund selection producing, for each scalar source G in L^{6/5} with compact support, a weak gradient D together with its pairing identity and its L^{6/5} bound against G, the coordinate sum of the Newtonian derivative potentials of the components of V has a weak gradient D satisfying the same pairing identity against every smooth compactly supported test function, with the L^{6/5} bound controlled by the sum of the component norms of V.