Local velocity moments throughout the solution domain #
The cylinder integrability of the velocity cube extends to every compact
space-time subset of the solution domain. This supplies the time integrals
on arbitrary compact windows in prop:bootstrap, without restricting time
to the origin unit cylinder.
theorem
CKN.Core.Step4.origin_velocity_cube_locallyIntegrableOn_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)
:
The velocity cube of a suitable solution is locally integrable at every point of its open space-time domain.
theorem
CKN.Core.Step4.origin_velocity_cube_integrable_on_local_box
{Ω B : Set Foundation.Parabolic.Vec3}
{I J : 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)
(hbox : localBox Ω I B J)
:
MeasureTheory.IntegrableOn
(fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u w) ^ 3) (spaceTimeSet B J)
MeasureTheory.volume
The velocity cube is integrable on any local box, including compact time windows anywhere in the solution interval.