Compact-core duality for the space-time pressure operators

The spatial CKN L² pairing yields duality first for compact space-time data.

theorem CKN.Leray.rieszPressureComponentCompactClass_pairing (r : ℝ) (hr : 1 < r) (q : ℝ) (hq : 1 < q) (hHolder : r.HolderConjugate q) (i j : Fin 3) {F G : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : Continuous F) (hFc : HasCompactSupport F) (hG : Continuous G) (hGc : HasCompactSupport G) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ), ↑↑(rieszPressureComponentCompactClass r hr i j hF hFc) z * G z = ∫ (z : Foundation.Parabolic.Vec3 × ℝ), F z * ↑↑(rieszPressureComponentCompactClass q hq j i hG hGc) z

The joint compact representative obeys the adjoint identity, used by lem:riesz-duality.