Compactness Limit Slices

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.ae_memLp_slice_of_memLp_product_vec3 {K : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (g : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.L2Vec3) (hg : MeasureTheory.MemLp g 2 ((MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J))) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => g (x, t)) 2 (MeasureTheory.volume.restrict K)

A space-time L² vector field belongs to spatial L² on almost every time slice of a rectangle.