Slice Integrability

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.slice_memLp_ae_of_sws {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (h : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (hbox : localBox Ω I Ω' J) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => u (x, s)) 2 (MeasureTheory.volume.restrict Ω') ∧ MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => Du (x, s)) 2 (MeasureTheory.volume.restrict Ω')

The velocity and gradient have square-integrable spatial slices almost everywhere in every local space-time box.