The regularized velocity on the whole slab #
The uniform bound of the regularized family makes the regularized velocity square integrable on the
whole slab ℝ³ × (0, T), including times arbitrarily close to zero (prop:lps-local-strong).
theorem
ESS.LPS.lps_regR12_l2Energy_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 L² norm of every slice
(lem:lps-regularized-Hk-start).
theorem
ESS.LPS.lps_regR12_velocity_memLp_open_slab
(ρ : CKN.Leray.RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3)
(hb : CKN.IsInJ b)
{T M : ℝ}
(h : ∀ t ∈ Set.Ioc 0 T, ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, lpsRegU ρ ε hε b hb (x, t) i ^ 2 ≤ M)
(i : Fin 3)
:
MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => lpsRegU ρ ε hε b hb z i) 2
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))
The regularized velocity is square integrable on the whole slab when its slices are uniformly
bounded in L².