Pressure pairing for the regularized equation

The canonical spatial pressure has the distributional Laplacian required in (R4) of thm:regularised.

theorem CKN.Leray.instFactLeENNRealOfNatOfRealReal_leanPool : Fact (1 ≤ ENNReal.ofReal 2)

theorem CKN.Leray.instHolderTripleOfRealOfNatRealENNReal_leanPool : (ENNReal.ofReal 2).HolderTriple (ENNReal.ofReal 2) 1

theorem CKN.Leray.regularisedPressureSlice_riesz_laplacian_pairing (F : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ) (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal 2) MeasureTheory.volume) (ψ : Foundation.Parabolic.Vec3 → ℝ) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∫ (x : Foundation.Parabolic.Vec3), rieszPressureSliceRepresentative 2 regularisedPressureSlice_riesz_laplacian_pairing._proof_1 (fun (i j : Fin 3) => MeasureTheory.MemLp.toLp (F i j) ⋯) x * spatialLaplacian ψ x = -∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), F i j x * mixedSecond ψ i j x

The canonical regularized pressure slice has the signed Laplacian pairing in (R4) of thm:regularised.