Stability Weighted Gradient Matrix #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.stability_weighted_gradient_matrix
{Ω Ω' : Set Foundation.Parabolic.Vec3}
{I J : 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)
(hsol : ∀ (n : ℕ), IsSuitableWeakSolution Ω I q (u n) (Du n) (p n) 0)
(hbox : localBox Ω I Ω' J)
(hDv : MeasureTheory.MemLp Dv 2 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J)))
(hDuWeak :
∀ (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))))
(ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ)
(hψ : ψ ∈ spaceTimeTestFunction Ω I)
(hψpos : ∀ (z : Foundation.Parabolic.Vec3 × ℝ), 0 ≤ ψ z)
:
Filter.Tendsto
(fun (n : ℕ) =>
∑ i : Fin 3,
∑ j : Fin 3, ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, Du n z i j * Dv z i j * ψ z)
Filter.atTop
(nhds (∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, spatialGradientSq v Dv z * ψ z)) ∧ ∀ (n : ℕ),
2 * ∑ i : Fin 3,
∑ j : Fin 3, ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, Du n z i j * Dv z i j * ψ z ≤ (∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, spatialGradientSq (u n) (Du n) z * ψ z) + ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, spatialGradientSq v Dv z * ψ z
Weak gradient convergence supplies the weighted mixed-energy limit and the polarization bound used in (S4).