CZHarmonic Corollary Force Slice #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
Almost-everywhere integrability of the force density f in the def:sws class,
restricted to spatial slices of an admissible parabolic cylinder. This is the
vector-valued analogue of sws_pressure_memLp_slice_ae.
theorem
CKN.sws_force_memLp_slice_ae
{Ω : 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)
{z : Foundation.Parabolic.ParabolicPoint}
{ρ : ℝ}
(hρ : 0 < ρ)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => f (x, s)) (ENNReal.ofReal q)
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ))