Unrestricted space-time Riesz duality

The compact-core pairing extends to arbitrary dual L^r classes by continuity and density.

theorem CKN.Leray.rieszPressureSpaceTimeComponent_duality (r : ℝ) (hr : 1 < r) (q : ℝ) (hq : 1 < q) (hHolder : r.HolderConjugate q) (i j : Fin 3) (u : ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal r) MeasureTheory.volume)) (v : ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal q) MeasureTheory.volume)) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ), ↑↑((rieszPressureSpaceTimeComponent r hr i j) u) z * ↑↑v z = ∫ (z : Foundation.Parabolic.Vec3 × ℝ), ↑↑u z * ↑↑((rieszPressureSpaceTimeComponent q hq j i) v) z

The component adjoint identity holds for every space-time L^r input, used by lem:riesz-duality.

theorem CKN.Leray.rieszPressureSpaceTimeClass_duality (r : ℝ) (hr : 1 < r) (q : ℝ) (hq : 1 < q) (hHolder : r.HolderConjugate q) (F : RieszPressureSpaceTimeTensorLp r) (g : ↥(MeasureTheory.Lp ℝ (ENNReal.ofReal q) MeasureTheory.volume)) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ), ↑↑(rieszPressureSpaceTimeClass r hr F) z * ↑↑g z = ∑ i : Fin 3, ∑ j : Fin 3, ∫ (z : Foundation.Parabolic.Vec3 × ℝ), ↑↑(F i j) z * ↑↑((rieszPressureSpaceTimeComponent q hq j i) g) z

The nine pressure components satisfy the unrestricted tensor duality in lem:riesz-duality.