Distributional equation for space-time pressure slices

The spatial sign identity holds on almost every time slice of a space-time tensor, for every smooth compactly supported spatial test function.

theorem CKN.Leray.rieszPressureSpaceTime_slice_laplacian_identity (r : ℝ) (hr : 1 < r) (F : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 × ℝ → ℝ) (hF : ∀ (i j : Fin 3), MeasureTheory.MemLp (F i j) (ENNReal.ofReal r) MeasureTheory.volume) : ∀ᵐ (t : ℝ), ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Foundation.Parabolic.Vec3), rieszPressureSpaceTime r hr F hF (x, t) * -spatialLaplacian ψ x = ∑ i : Fin 3, ∑ j : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), F i j (x, t) * mixedSecond ψ i j x