Noncompact potential tests for space-time pressure

The compact distributional identity extends first to arbitrary input classes and then to decaying potential tests by spatial cutoff and dominated convergence.

theorem CKN.Leray.rieszPressureSpaceTimeClass_noncompactPotential_duality (F : RieszPressureSpaceTimeTensorLp (3 / 2)) {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hdecay : RieszPressurePotentialDecay ψ) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ), ↑↑(rieszPressureSpaceTimeClass (3 / 2) rieszPressureSpaceTimeClass_noncompactPotential_duality._proof_2 F) z * rieszPressureJointLaplacian ψ z = -∑ i : Fin 3, ∑ j : Fin 3, ∫ (z : Foundation.Parabolic.Vec3 × ℝ), ↑↑(F i j) z * rieszPressureJointHessian ψ i j z

The noncompact-potential identity holds for every space-time tensor class in L^(3/2), as asserted in lem:riesz-duality.

theorem CKN.Leray.rieszPressureSpaceTime_noncompactPotential_duality (F : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 × ℝ → ℝ) (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hdecay : RieszPressurePotentialDecay ψ) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ), rieszPressureSpaceTime (3 / 2) rieszPressureSpaceTimeClass_noncompactPotential_duality._proof_2 F hF z * rieszPressureJointLaplacian ψ z = -∑ i : Fin 3, ∑ j : Fin 3, ∫ (z : Foundation.Parabolic.Vec3 × ℝ), F i j z * rieszPressureJointHessian ψ i j z

The measurable space-time pressure representative satisfies the noncompact-potential identity in lem:riesz-duality.