Function representatives in Riesz pressure duality

The measurable representative of the pressure satisfies the same pairing as its canonical space-time L^r class.

theorem CKN.Leray.rieszPressureSpaceTime_duality (r : ℝ) (hr : 1 < r) (q : ℝ) (hq : 1 < q) (hHolder : r.HolderConjugate q) (F : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 × ℝ → ℝ) (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal r) MeasureTheory.volume) (g : Foundation.Parabolic.Vec3 × ℝ → ℝ) (hg : MeasureTheory.MemLp g (ENNReal.ofReal q) MeasureTheory.volume) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ), rieszPressureSpaceTime r hr F hF z * g z = ∑ i : Fin 3, ∑ j : Fin 3, ∫ (z : Foundation.Parabolic.Vec3 × ℝ), F i j z * ↑↑((rieszPressureSpaceTimeComponent q hq j i) (MeasureTheory.MemLp.toLp g hg)) z

The measurable space-time pressure representative satisfies the full duality formula, used by lem:riesz-duality.