Lp Extension Pairing Kernel

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

theorem CKN.Foundation.Euclidean.integrable_of_memLp_hasCompactSupport {p : ENNReal} (hp : 1 ≤ p) {G : Parabolic.Vec3 → ℝ} (hG : MeasureTheory.MemLp G p MeasureTheory.volume) (hGc : HasCompactSupport G) : MeasureTheory.Integrable G MeasureTheory.volume

A function in L^p with compact support is integrable.

The compact support confines the function to a finite-measure set, where the L^p membership with p ≥ 1 yields integrability, and integrability on the support is equivalent to integrability on the whole space. This is the integrability input for the pairing identities of cor:CZ-harmonic.

theorem CKN.Foundation.Euclidean.pressureNewtonianDerivativePotential_pairing_potential {i j : Fin 3} {G ψ : Parabolic.Vec3 → ℝ} (hG : MeasureTheory.Integrable G MeasureTheory.volume) (hGc : HasCompactSupport G) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∫ (x : Parabolic.Vec3), pressureNewtonianDerivativePotential i G x * spatialDeriv ψ j x = ∫ (y : Parabolic.Vec3), G y * pressureNewtonianPotential (mixedSecond ψ i j) y

The derivative potential paired against a spatial derivative of a smooth compactly supported test function equals the Newtonian potential of the mixed second derivative paired against G.

The inner integral over x is the first-order adjoint identity of the Newtonian kernel, and the remaining y-integration is the Fubini identity for potentials against compactly supported data. This is the pairing form of cor:CZ-harmonic used to move derivatives off the pressure potential.