Compact-time integrability of the complete centered slice majorant #
Every term of the explicit majorant in eq:pressure-gradient-morrey is
integrable in time at a fixed interior origin radius, on every local box of
the solution interval.
Time integrability of the direct force-gradient contribution #
Both cutoff source norms and the spatial force mass in
eq:pressure-gradient-morrey are time integrable on any interior local box.
theorem
CKN.Core.Step4.origin_force_gradient_integrable_on_local_box
{Ω : Set Foundation.Parabolic.Vec3}
{I J : Set ℝ}
{q ρ : ℝ}
{x : Foundation.Parabolic.Vec3}
{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)
(hρ : 0 < ρ)
(hbox : localBox Ω I (Foundation.Parabolic.vec3Ball x ρ) J)
(C D : ℝ)
:
MeasureTheory.Integrable (fun (s : ℝ) => sliceForceGradientBound C D x hρ f s) (MeasureTheory.volume.restrict J)
The direct force-gradient slot is time integrable from suitability, for arbitrary fixed real coefficients.
theorem
CKN.Core.Step4.origin_slice_majorant_integrable_on_local_box
{Ω : 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)
(hρ : 0 < ρ)
(hbox : localBox Ω I (Foundation.Parabolic.vec3Ball 0 ρ) J)
:
MeasureTheory.Integrable (fun (s : ℝ) => (originSliceGradientMajorant u Du p f (0, 0) hρ s).toReal)
(MeasureTheory.volume.restrict J)
Suitability gives time integrability of the complete fixed-origin slice majorant on every local box with its source ball.