Uniform bounds on time slices of L²(I; H²) fields

prop:lps-smoothing: an L²(I; H²) space-time field is bounded, on almost every time slice, by the H² norm of the slice.

theorem ESS.lps_ae_slice_sup_bound : ∃ (K : ℝ), 0 ≤ K ∧ ∀ {a b : ℝ} {f : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} {D : List (Fin 3) → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}, CKN.IsL2SobolevFamilyOn 2 Set.univ (Set.Ioo a b) f D → ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), f (x, t) ^ 2 ≤ K * ∑ α ∈ CKN.sobolevWords 2, ∫ (y : CKN.Foundation.Parabolic.Vec3), D α (y, t) ^ 2

On almost every time slice an L²(I;H²) field is bounded by a universal multiple of the H² norm of the slice (prop:lps-smoothing).