Square integrability of smooth space-time tests

A compactly supported smooth test and each first spatial derivative are square integrable on every measurable time slab. These test classes pass the ordered weak-derivative identities to limits.

theorem ESS.lps_spaceTimeTest_spatial_memLp_two {φ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => φ p) (hφc : HasCompactSupport fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => φ p) (I : Set ℝ) : MeasureTheory.MemLp φ 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ I)) ∧ ∀ (j : Fin 3), MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial φ j z) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ I))

A compactly supported smooth scalar test and all first spatial partials belong to L² on an arbitrary time slab (prop:lps-smoothing).