Compact-time integrability of the centered source majorant

The centered tensor-source bound in eq:pressure-gradient-morrey is finite and integrable on compact time windows of any local box. This is the source contribution to the time obligations in prop:bootstrap; the pressure and force-potential contributions are separate.

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) : MeasureTheory.LocallyIntegrableOn (fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u w) ^ 3) (spaceTimeSet Ω I) MeasureTheory.volume

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.

noncomputable def CKN.Core.Step4.originCenteredSourceMajorant (x : Foundation.Parabolic.Vec3) (ρ : ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (s : ℝ) : ENNReal

The two-term bound for the sum of the centered tensor-source norms.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Core.Step4.origin_centered_source_majorant_obligations_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) (hbox : localBox Ω I (Foundation.Parabolic.vec3Ball x ρ) J) : AEMeasurable (originCenteredSourceMajorant x ρ u Du) (MeasureTheory.volume.restrict J) ∧ (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, originCenteredSourceMajorant x ρ u Du s ≠ ⊤) ∧ MeasureTheory.Integrable (fun (s : ℝ) => (originCenteredSourceMajorant x ρ u Du s).toReal) (MeasureTheory.volume.restrict J)

On any local ball-times-window box, suitability gives measurable, finite and integrable centered-source majorant without a decay hypothesis.