Compact-time integrability of the actual harmonic force constant #
The harmonic force term in eq:pressure-gradient-morrey, including both
potential-growth constants, is measurable and integrable on interior time boxes.
theorem
CKN.Core.Step4.origin_cutoff_product_aestronglyMeasurable
{B : Set Foundation.Parabolic.Vec3}
{J : Set ℝ}
{G : Foundation.Parabolic.Vec3 × ℝ → ℝ}
{η : Foundation.Parabolic.Vec3 → ℝ}
(hB : MeasurableSet B)
(hG : MeasureTheory.AEStronglyMeasurable G ((MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict J)))
(hη : MeasureTheory.AEStronglyMeasurable η MeasureTheory.volume)
(hs : Function.support η ⊆ B)
:
MeasureTheory.AEStronglyMeasurable (fun (w : Foundation.Parabolic.Vec3 × ℝ) => η w.1 * G w)
(MeasureTheory.volume.prod (MeasureTheory.volume.restrict J))
Multiplication by a spatial cutoff supported in the local ball extends local product measurability to the full spatial space.
theorem
CKN.Core.Step4.origin_harmonic_force_integrable_on_local_box
{Ω : Set Foundation.Parabolic.Vec3}
{I J : 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)
(hR : 0 < R)
(hbox : localBox Ω I (Foundation.Parabolic.vec3Ball 0 R) J)
:
MeasureTheory.Integrable (fun (s : ℝ) => harmonicRemainderForceBound (0, 0) hR f s) (MeasureTheory.volume.restrict J)
The actual harmonic force constant is time integrable on every local origin box of a suitable weak solution.