Integration by parts for the centred tensor

Without a finite-measure assumption on the open set, the identity for eq:pressure-gradient-decomposition follows by differentiating the quadratic product, subtracting its constant-vector correction, and using the vanishing trace of the weak velocity gradient.

theorem CKN.Core.Step4.pressureDivergenceCutoffSourceCentredTensor_pairing_of_divfree {U : Set Foundation.Parabolic.Vec3} (hU : IsOpen U) {η : Foundation.Parabolic.Vec3 → ℝ} {u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.Vec3 → Fin 3 → Foundation.Parabolic.Vec3} {c : Foundation.Parabolic.Vec3} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hηU : tsupport η ⊆ U) (hu : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u x i) 2 (MeasureTheory.volume.restrict U)) (hDu : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => Du x i j) 2 (MeasureTheory.volume.restrict U)) (hw : ∀ (i : Fin 3), HasWeakGradientOn U (fun (x : Vec 3) => u x i) fun (x : Vec 3) => Du x i) (hdiv : ∀ (φ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ U → ∫ (x : Foundation.Parabolic.Vec3) in U, ∑ i : Fin 3, u x i * spatialDeriv φ i x = 0) {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∑ i : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), pressureDivergenceCutoffSourceCentredTensor η (spatialDeriv η) u Du c x i * spatialDeriv ψ i x = pressureSecondPairing (fun (i j : Fin 3) (x : Foundation.Parabolic.Vec3) => η x * (-u x i * (u x j - c j))) ψ

The force-free centred source pairs with the singly centred tensor in eq:pressure-gradient-decomposition for every compactly supported smooth test.