Stability S1 #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.stability_suitable_data
{Ω : 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 → ℝ)
(v : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(Dv : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3)
(r : Foundation.Parabolic.ParabolicPoint → ℝ)
(hsol : ∀ (n : ℕ), IsSuitableWeakSolution Ω I q (u n) (Du n) (p n) 0)
(hbound :
∀ (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ),
localBox Ω I Ω' J →
∃ M < ⊤,
∀ (n : ℕ),
essSup (fun (t : ℝ) => ∫⁻ (x : Foundation.Parabolic.Vec3) in Ω', ‖u n (x, t)‖ₑ ^ 2)
(MeasureTheory.volume.restrict J) ≤ M)
(huConv :
∀ (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ),
localBox Ω I Ω' J →
Filter.Tendsto
(fun (n : ℕ) => MeasureTheory.eLpNorm (u n - v) 3 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J)))
Filter.atTop (nhds 0))
(hDv :
∀ (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ),
localBox Ω I Ω' J → MeasureTheory.MemLp Dv 2 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J)))
(hDuWeak :
∀ (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ),
localBox Ω I Ω' J →
∀ (i j : Fin 3) (w : Foundation.Parabolic.Vec3 × ℝ → ℝ),
MeasureTheory.MemLp w 2 ((MeasureTheory.volume.restrict Ω').prod (MeasureTheory.volume.restrict J)) →
Filter.Tendsto
(fun (n : ℕ) =>
∫ (z : Foundation.Parabolic.Vec3 × ℝ), Du n (z.1, z.2) i j * w z ∂(MeasureTheory.volume.restrict Ω').prod (MeasureTheory.volume.restrict J))
Filter.atTop
(nhds
(∫ (z : Foundation.Parabolic.Vec3 × ℝ), Dv (z.1, z.2) i j * w z ∂(MeasureTheory.volume.restrict Ω').prod (MeasureTheory.volume.restrict J))))
(hpConv :
∀ (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ),
localBox Ω I Ω' J →
Filter.Tendsto
(fun (n : ℕ) => MeasureTheory.eLpNorm (p n - r) (3 / 2) (MeasureTheory.volume.restrict (spaceTimeSet Ω' J)))
Filter.atTop (nhds 0))
:
IsSuitableWeakSolutionData Ω I q v Dv r 0
The local data clauses of suitable weak solutions are stable under the
convergences and the uniform slice bound in thm:stability.