Space-time weak derivatives of the compactness limit #
The compactness limit of the regularized velocities, its gradient, its Hessian, and the weak limit
of
the time derivatives satisfy the space-time weak derivative relations against smooth compactly
supported tests (prop:lps-local-strong).
theorem
ESS.LPS.lps_regR12_derivs_memLp_slab
(ρ : CKN.Leray.RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3)
(hb : CKN.IsInJ b)
{δ T : ℝ}
(hδ : 0 < δ)
(hδT : δ < T)
(i j k : Fin 3)
:
MeasureTheory.MemLp
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => lpsRegU ρ ε hε b hb y i) j z)
2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo δ T))) ∧ MeasureTheory.MemLp
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
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 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo δ T)))
The first and second spatial derivatives of the regularized velocity are square integrable on
every positive-time slab (thm:regularised of the CKN manuscript, (R3)).
theorem
ESS.LPS.lps_regR12_hessian_ibp
(ρ : CKN.Leray.RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
(b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3)
(hb : CKN.IsInJ b)
{T : ℝ}
(hT : 0 < T)
(i j k : Fin 3)
{φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo 0 T))
:
∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab 0 T, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => lpsRegU ρ ε hε b hb y i) j z * CKN.spatialPartial φ k z = -∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab 0 T, 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 * φ z
Integration by parts for the gradient of the regularized velocity on a slab:
∫ ∂ⱼUᵢ ∂ₖφ = -∫ ∂ₖ∂ⱼUᵢ φ.
theorem
ESS.LPS.lps_strong_limit_time_derivative
(ρ : 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)
(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)
{σ : ℕ → ℕ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hUconv :
Filter.Tendsto
(fun (n : ℕ) =>
MeasureTheory.eLpNorm (CKN.Leray.regR12Uε ρ b ⋯ ((fun (m : ℕ) => 1 / (↑m + 1)) (σ n)) - u) 2
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
Filter.atTop (nhds 0))
:
∃ (Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3),
MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo 0 T),
∀ (i : Fin 3),
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), u z i * CKN.timePartial φ z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), Dtu z i * φ z
The weak limit of the time derivatives of the regularized velocities along the compactness
subsequence is the weak time derivative of the limit (prop:lps-local-strong).