Slice Selected Gradient Centred Source Tensor

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

Pairing identity for the force-free centred source

The weak product rule converts the centred cutoff source into the second pressure pairing, with the divergence-free trace term cancelling after summing the spatial indices.

theorem CKN.Core.Step4.pressureDivergenceCutoffSourceCentredTensor_pairing_of_weak_data {U : Set Foundation.Parabolic.Vec3} (hU : IsOpen U) {η : Foundation.Parabolic.Vec3 → ℝ} {dη : Fin 3 → Foundation.Parabolic.Vec3 → ℝ} {u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.Vec3 → Fin 3 → Fin 3 → ℝ} {c : Foundation.Parabolic.Vec3} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hηU : tsupport η ⊆ U) (hdη : ∀ (j : Fin 3), dη j = spatialDeriv η j) (hUfinite : (MeasureTheory.volume.restrict U) Set.univ < ⊤) (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)) (hweak : ∀ (i : Fin 3), HasWeakGradientOn U (fun (x : Vec 3) => u x i) fun (x : Vec 3) => Du x i) (htrace : (fun (x : Foundation.Parabolic.Vec3) => ∑ i : Fin 3, Du x i i) =ᵐ[MeasureTheory.volume.restrict U] 0) {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) : ∑ i : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), pressureDivergenceCutoffSourceCentredTensor η dη 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 cutoff source pairs against a test gradient as the second pressure pairing of the cutoff centred tensor.