Agreement of pressure extensions

The bounded extensions at different exponents define one operator on their common domains, as in def:riesz-pressure.

theorem CKN.Leray.rieszPressureSpaceTime_ae_eq_of_memLp_common (r : ℝ) (hr : 1 < r) (s : ℝ) (hs : 1 < s) (F : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 × ℝ → ℝ) (hFr : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal r) MeasureTheory.volume) (hFs : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal s) MeasureTheory.volume) : rieszPressureSpaceTime r hr F hFr =ᵐ[MeasureTheory.volume] rieszPressureSpaceTime s hs F hFs