Pressure Gradient HGCloser Time Bounds #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.Core.Step4.lintegral_slice_eLpNorm_lt_top_of_memLp
{a : ℝ}
(ha : 1 ≤ a)
{B : Set Foundation.Parabolic.Vec3}
{J : Set ℝ}
(hJ : MeasureTheory.volume J < ⊤)
{F : Foundation.Parabolic.ParabolicPoint → ℝ}
(hF : MeasureTheory.MemLp F (ENNReal.ofReal a) (MeasureTheory.volume.restrict (B ×ˢ J)))
:
∫⁻ (t : ℝ) in J, MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => F (x, t)) (ENNReal.ofReal a)
(MeasureTheory.volume.restrict B) < ⊤
A finite space-time Lᵃ norm on a finite time interval supplies a
finite integral of the spatial slice norms.
theorem
CKN.Core.Step4.lintegral_cutoff_slice_eLpNorm_lt_top_of_memLp
{a : ℝ}
(ha : 1 ≤ a)
{B : Set Foundation.Parabolic.Vec3}
{J : Set ℝ}
(hB : MeasurableSet B)
(hJ : MeasureTheory.volume J < ⊤)
{η : Foundation.Parabolic.Vec3 → ℝ}
(hη : MeasureTheory.AEStronglyMeasurable η MeasureTheory.volume)
(hηbound : ∀ (x : Foundation.Parabolic.Vec3), |η x| ≤ 1)
(hηsupport : Function.support η ⊆ B)
{F : Foundation.Parabolic.ParabolicPoint → ℝ}
(hF : MeasureTheory.MemLp F (ENNReal.ofReal a) (MeasureTheory.volume.restrict (B ×ˢ J)))
:
∫⁻ (t : ℝ) in J, MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => η x * F (x, t)) (ENNReal.ofReal a)
MeasureTheory.volume < ⊤
A bounded spatial cutoff supported in the local carrier preserves finiteness of the time integral of spatial slice norms.
theorem
CKN.Core.Step4.lintegral_pressure_slice_eLpNorm_lt_top_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)
{B : Set Foundation.Parabolic.Vec3}
{J : Set ℝ}
(hbox : localBox Ω I B J)
:
∫⁻ (t : ℝ) in J, MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => p (x, t)) (ENNReal.ofReal (3 / 2))
(MeasureTheory.volume.restrict B) < ⊤
The pressure term of the slice gradient bound has a finite time integral on every compactly contained solution box.
theorem
CKN.Core.Step4.lintegral_force_slice_eLpNorm_lt_top_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)
{B : Set Foundation.Parabolic.Vec3}
{J : Set ℝ}
(hbox : localBox Ω I B J)
(i : Fin 3)
:
∫⁻ (t : ℝ) in J, MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => f (x, t) i) (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict B) < ⊤
Each force component supplies a finite time integral of its spatial
L^{6/5} norm using only the local force data of a suitable solution.
theorem
CKN.Core.Step4.lintegral_cutoff_force_slice_eLpNorm_lt_top_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)
{B : Set Foundation.Parabolic.Vec3}
{J : Set ℝ}
(hbox : localBox Ω I B J)
{η : Foundation.Parabolic.Vec3 → ℝ}
(hη : MeasureTheory.AEStronglyMeasurable η MeasureTheory.volume)
(hηbound : ∀ (x : Foundation.Parabolic.Vec3), |η x| ≤ 1)
(hηsupport : Function.support η ⊆ B)
(i : Fin 3)
:
∫⁻ (t : ℝ) in J, MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => η x * f (x, t) i) (ENNReal.ofReal (6 / 5))
MeasureTheory.volume < ⊤
The cutoff-force term has a finite time-integrated spatial norm without any global assumption or divergence constraint on the force.