Identification Extension Pairing Slice

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

theorem CKN.pressureCutoff_slice_data_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} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {η : Foundation.Parabolic.Vec3 → ℝ} (hηc : HasCompactSupport η) (hηΩ : tsupport η ⊆ Ω) (c : ℝ → Foundation.Parabolic.Vec3) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, (∀ (i j : Fin 3), MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j) (tsupport η) MeasureTheory.volume) ∧ MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => p (y, s)) (tsupport η) MeasureTheory.volume ∧ ∀ (j : Fin 3), MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => f (y, s) j) (tsupport η) MeasureTheory.volume

Almost-everywhere slice integrability of the velocity tensor, the pressure and the force on the support of a spatial cut-off. For a suitable weak solution on Ω × I, a compactly supported cut-off η whose topological support lies in Ω, and any c : ℝ → Vec3, for almost every time s the functions pressureUTensor u c (·, s) i j, p (·, s) and f (·, s) j are integrable on tsupport η with respect to the spatial measure. This supplies the slice data consumed by the localized pressure pairing identity (paper label: pressure cut-off identity).