The uniform slab bound for the time derivative of the regularized velocity #
The slice bound of the time derivative and the uniform H¹, L²_tH² bounds give a bound on the
slab L² norm of the time derivative of every regularized velocity that does not depend on the
regularization parameter (prop:lps-local-strong).
theorem
ESS.LPS.lps_slab_integrable_of_slice_bound
{a τ : ℝ}
{F : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hF : MeasureTheory.AEStronglyMeasurable F (MeasureTheory.volume.restrict (CKN.vlSlab a τ)))
(hnn : ∀ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), 0 ≤ F z)
{g : ℝ → ℝ}
(hg : MeasureTheory.IntegrableOn g (Set.Ioo a τ) MeasureTheory.volume)
(hslice :
∀ t ∈ Set.Ioo a τ,
MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, t)) MeasureTheory.volume ∧ ∫ (x : CKN.Foundation.Parabolic.Vec3), F (x, t) ≤ g t)
:
MeasureTheory.Integrable F (MeasureTheory.volume.restrict (CKN.vlSlab a τ)) ∧ ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a τ, F z ≤ ∫ (t : ℝ) in Set.Ioo a τ, g t
A nonnegative slab function whose slice integrals are dominated by an integrable function of time is integrable on the slab, with integral at most the time integral of the bound.
theorem
ESS.LPS.lps_regR12_gradEnergy_le
(ρ : CKN.Leray.RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3)
(hb : CKN.IsInJ b)
{t : ℝ}
(ht : 0 ≤ t)
{M : ℝ}
(h :
∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (lpsRegU ρ ε hε b hb (x, t)) ^ 2 + CKN.spatialGradientSq (lpsRegU ρ ε hε b hb)
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) =>
CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => lpsRegU ρ ε hε b hb y i) j z)
(x, t) ≤ M)
:
The uniform bound of the regularized family controls the gradient energy of every slice
(lem:lps-regularized-Hk-start).
theorem
ESS.LPS.lps_regR12_Q_slab
(ρ : CKN.Leray.RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3)
(hb : CKN.IsInJ b)
{T M : ℝ}
(hT : 0 < T)
(hy : ∀ t ∈ Set.Ioc 0 T, lpsRegGradEnergy ρ ε hε b hb t ≤ M)
(hH :
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), ∑ i : Fin 3,
∑ j : Fin 3,
∑ k : Fin 3,
CKN.spatialPartial
(fun (y : CKN.Foundation.Parabolic.ParabolicPoint) =>
CKN.spatialPartial (fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => lpsRegU ρ ε hε b hb x i) j y)
k z ^ 2 ≤ M)
:
(∀ (i : Fin 3),
MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => lpsRegQ ρ ε hε b hb z i) 2
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) ∧ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), ∑ i : Fin 3, lpsRegQ ρ ε hε b hb z i ^ 2 ≤ (3 + 81 * (CKN.gagliardoNirenbergSobolevConstant.toReal ^ 3 * M ^ (3 / 2))) * M + 81 * (CKN.gagliardoNirenbergSobolevConstant.toReal ^ 3 * M ^ (3 / 2)) * T
The slab L² norm of the time derivative of the regularized velocity is bounded uniformly in
the regularization parameter by the uniform H¹ and L²_tH² bounds (prop:lps-local-strong).