Pairing the first derivative potential with the completed operator

The first Newtonian derivative potential Pᵢ(G) = ∂ᵢN * G and the completed L^(6/5) second-derivative operator Tᵢⱼ are adjoint to one another in the distributional sense: for compactly supported L^(6/5) data G and smooth compactly supported ψ,

∫ Pᵢ(G) ∂ⱼψ = ∫ Tᵢⱼ(G) ψ.

The sign is positive: the completed operator is the unnegated second derivative of the Newtonian potential, so the pairing selects -Tᵢⱼ(G) as the weak derivative ∂ⱼPᵢ(G).

The proof moves both derivatives onto the test function. On smooth compactly supported data the completed operator is the classical Hessian ∂ᵢ∂ⱼ(N * G), and two classical integrations by parts turn the left side into ∫ G · (N * ∂ᵢ∂ⱼψ). Both sides of the resulting identity are continuous linear functionals of G ∈ L^(6/5): the left through the operator norm bound of the extension and Hölder against ψ ∈ L⁶, the right through Hölder against the Newtonian potential N * ∂ᵢ∂ⱼψ ∈ L⁶. Density of smooth compactly supported classes in L^(6/5) closes the argument.

theorem CKN.Foundation.Euclidean.pressureNewtonianDerivativePotential_gradient_extension_pairing {i j : Fin 3} (hL2 : RieszSecondL2Input i j) (hWeak11 : ∀ (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |rieszSecondL2RawOperator hL2 f x|} ≤ (ENNReal.ofReal rieszSecondWeakTypeConstant * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) {G : Parabolic.Vec3 → ℝ} (hG : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hGc : HasCompactSupport G) {ψ : Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∫ (x : Parabolic.Vec3), pressureNewtonianDerivativePotential i G x * spatialDeriv ψ j x = ∫ (x : Parabolic.Vec3), rieszSecondGradientExtensionOperator hL2 hWeak11 G x * ψ x

The first derivative potential is adjoint to the completed exponent 6 / 5 operator, with a positive sign.

theorem CKN.Foundation.Euclidean.rieszSecondGradientExtension_weak_gradient_pairing (hL2 : (i j : Fin 3) → RieszSecondL2Input i j) (hWeak11 : ∀ (i j : Fin 3) (f : Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Parabolic.Vec3 | l < |rieszSecondL2RawOperator (hL2 i j) f x|} ≤ (ENNReal.ofReal rieszSecondWeakTypeConstant * ∫⁻ (x : Parabolic.Vec3), absE f x) / ENNReal.ofReal l) (i j : Fin 3) (G : Parabolic.Vec3 → ℝ) : MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume → HasCompactSupport G → ∀ (ψ : Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Parabolic.Vec3), pressureNewtonianDerivativePotential i G x * spatialDeriv ψ j x = ∫ (x : Parabolic.Vec3), rieszSecondGradientExtensionOperator (hL2 i j) ⋯ G x * ψ x

The indexed family of pairing identities, in the shape consumed by the weak-gradient selection: the pairing is positive, so the selected weak derivative is the negative of the completed operator.