Identifying a fixed pressure derivative with the completed operators

The first-potential pairing has positive sign, so the derivative of its sum is the negative Riesz sum. The negative first-potential sum of the near force has the opposite sign. Uniqueness identifies these terms with an already chosen weak pressure derivative.

theorem CKN.Core.Step4.newtonian_derivative_sum_hasWeakPartialDerivOn_riesz {B : Set Foundation.Parabolic.Vec3} (hB : IsOpen B) (i : Fin 3) {V : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hV : ∀ (j : Fin 3), MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => V y j) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hVc : ∀ (j : Fin 3), HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => V y j) : HasWeakPartialDerivOn B i (fun (x : Vec 3) => ∑ j : Fin 3, pressureNewtonianDerivativePotential j (fun (y : Foundation.Parabolic.Vec3) => V y j) x) fun (x : Vec 3) => -∑ j : Fin 3, Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ (fun (y : Foundation.Parabolic.Vec3) => V y j) x

The sum of first potentials has the negative completed Riesz sum as its weak derivative on every open spatial carrier.

theorem CKN.Core.Step4.weak_pressure_derivative_eq_riesz_sum_remainder {B : Set Foundation.Parabolic.Vec3} (hB : IsOpen B) (i : Fin 3) {p h g : Foundation.Parabolic.Vec3 → ℝ} {V W : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hV : ∀ (j : Fin 3), MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => V y j) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hVc : ∀ (j : Fin 3), HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => V y j) (hW : ∀ (j : Fin 3), MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => W y j) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hWc : ∀ (j : Fin 3), HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => W y j) (hh : ContDiffOn ℝ (↑1) h B) (hrep : p =ᵐ[MeasureTheory.volume.restrict B] fun (x : Foundation.Parabolic.Vec3) => ∑ j : Fin 3, pressureNewtonianDerivativePotential j (fun (y : Foundation.Parabolic.Vec3) => V y j) x + (h x - ∑ j : Fin 3, pressureNewtonianDerivativePotential j (fun (y : Foundation.Parabolic.Vec3) => W y j) x)) (hg : MeasureTheory.LocallyIntegrableOn g B MeasureTheory.volume) (hpg : HasWeakPartialDerivOn B i p g) : g =ᵐ[MeasureTheory.volume.restrict B] fun (x : Foundation.Parabolic.Vec3) => -∑ j : Fin 3, Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ (fun (y : Foundation.Parabolic.Vec3) => V y j) x + classicalGradient h x i + ∑ j : Fin 3, Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ (fun (y : Foundation.Parabolic.Vec3) => W y j) x

A fixed weak pressure derivative agrees with the signed Riesz sums and the classical derivative of the smooth remainder.