The compactness limit with all its space-time weak derivatives #
The compactness limit of the regularized velocities, with its Leray--Hopf gradient, the weak limit
of the Hessians, and the weak limit of the time derivatives, satisfies the space-time weak
derivative relations of HasSpaceTimeWeakDerivs with square integrable fields
(prop:lps-local-strong).
theorem
ESS.LPS.lps_strong_limit_weak_derivatives
(ρ : CKN.Leray.RegMollifierProfile)
(b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3)
(Db : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3)
(hb :
(∀ (i : Fin 3),
∃ (h : CKN.H1Function Set.univ),
(h.toFun = fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) ∧ h.grad = fun (x : CKN.Foundation.Parabolic.Vec3) => Db x i) ∧ CKN.IsInJ b)
(T M : ℝ)
(hT : 0 < T)
(hM : 0 ≤ M)
(hUniformBounds :
∀ (ε : ℝ) (hε : 0 < ε),
have Uε := CKN.Leray.regR12Velocity ρ ε hε b ⋯;
have Dε := fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) =>
CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => Uε y i) j z;
have D2ε := fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j k : Fin 3) =>
CKN.spatialPartial
(fun (y : CKN.Foundation.Parabolic.ParabolicPoint) =>
CKN.spatialPartial (fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => Uε x i) j y)
k z;
(∀ t ∈ Set.Icc 0 T,
∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (Uε (x, t)) ^ 2 + CKN.spatialGradientSq Uε Dε (x, t) ≤ M) ∧ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), ∑ i : Fin 3, ∑ j : Fin 3, CKN.Foundation.Parabolic.vec3EuclideanNorm (D2ε z i j) ^ 2 ≤ M)
:
∃ (σ₀ : ℕ → ℕ),
StrictMono σ₀ ∧ ∃ (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du :
CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (D2u :
CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (Dtu :
CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3),
(∀ (x : CKN.Foundation.Parabolic.Vec3), u (x, 0) = b x) ∧ CKN.IsLerayHopfSolution T b u Du ∧ CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo 0 T) u Du D2u Dtu ∧ MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ MeasureTheory.MemLp D2u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ (∀ (t : ℝ),
0 < t →
∀ (w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3),
MeasureTheory.MemLp w 2 MeasureTheory.volume →
Filter.Tendsto
(fun (n : ℕ) =>
∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3,
CKN.Leray.regR12Uε ρ b ⋯ ((fun (m : ℕ) => 1 / (↑m + 1)) (σ₀ n)) (x, t) i * w x i)
Filter.atTop
(nhds (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i * w x i))) ∧ ∀ (z : CKN.Foundation.Parabolic.Vec3 × ℝ),
0 < z.2 →
u (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z) = CKN.Leray.compactnessMollifiedLimit
(fun (n : ℕ) (y : CKN.Foundation.Parabolic.Vec3 × ℝ) =>
CKN.Leray.regR12Uε ρ b ⋯ ((fun (m : ℕ) => 1 / (↑m + 1)) (σ₀ n))
(CKN.Foundation.Parabolic.parabolicHomeomorph.symm y))
σ₀ z
The compactness limit, its gradient, the weak limit of the Hessians and the weak limit of the
time derivatives have the space-time weak derivative relations and are square integrable on the
slab (prop:lps-local-strong).