Pressure slices on the whole solution interval #
The local pressure integrability of a suitable weak solution supplies the
pressure premise of spatial weak-gradient gluing in prop:bootstrap.
A compact exhaustion of the time interval makes the exceptional set uniform
on the entire interval.
theorem
CKN.Core.Step4.pressure_slice_integrable_ae_on_origin_ball
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q R : ℝ}
{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)
(hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I)
(hR : 0 < R)
(hRone : R < 1)
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict I, MeasureTheory.IntegrableOn (fun (x : Foundation.Parabolic.Vec3) => p (x, t)) (Foundation.Parabolic.vec3Ball 0 R)
MeasureTheory.volume
Pressure is spatially integrable on the origin ball at almost every time
of the whole solution interval, as needed in prop:bootstrap.
theorem
CKN.Core.Step4.pressure_slice_locallyIntegrable_ae_on_origin_ball
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q R : ℝ}
{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)
(hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I)
(hR : 0 < R)
(hRone : R < 1)
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict I, MeasureTheory.LocallyIntegrableOn (fun (x : Foundation.Parabolic.Vec3) => p (x, t))
(Foundation.Parabolic.vec3Ball 0 R) MeasureTheory.volume
The locally integrable pressure slices required by the spatial gluing
step of prop:bootstrap follow from suitability alone.