Distributional pairing for the tensor-indexed pressure extension

The nine completed scalar identities sum to the pressure identity. Hölder integrability justifies the finite-sum interchanges without compact support of the tensor inputs or any condition on chosen Lp representatives.

theorem CKN.Core.Endgame.rieszSecondP1ExtensionTensor_distributional_identity (hL2 : (i j : Fin 3) → Foundation.Euclidean.RieszSecondL2Input i j) (hWeak11 : ∀ (i j : Fin 3) (f : Foundation.Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Foundation.Parabolic.Vec3 | l < |Foundation.Euclidean.rieszSecondL2RawOperator (hL2 i j) f x|} ≤ (ENNReal.ofReal Foundation.Euclidean.rieszSecondWeakTypeConstant * ∫⁻ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.absE f x) / ENNReal.ofReal l) {G : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ} (hG : ∀ (i j : Fin 3), MeasureTheory.MemLp (G i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∫ (x : Foundation.Parabolic.Vec3), (∑ i : Fin 3, ∑ j : Fin 3, Foundation.Euclidean.rieszSecondP1ExtensionOperator (hL2 i j) ⋯ (G i j) x) * spatialLaplacian ψ x = ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, G i j x * mixedSecond ψ i j x

The tensor sum of the actual completed operators satisfies the distributional pressure identity for arbitrary L^(3/2) component inputs.