Stability Weak Gradient Product #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.stability_weak_partial_on_localBox_of_product_limits
{Ω : Set Foundation.Parabolic.Vec3}
{J : Set ℝ}
(hΩ : IsOpen Ω)
(hΩfinite : MeasureTheory.volume Ω < ⊤)
(hJfinite : MeasureTheory.volume J < ⊤)
(U D : ℕ → Foundation.Parabolic.Vec3 × ℝ → ℝ)
(u d : Foundation.Parabolic.Vec3 × ℝ → ℝ)
(j : Fin 3)
(hU : ∀ (n : ℕ), MeasureTheory.MemLp (U n) 3 ((MeasureTheory.volume.restrict Ω).prod (MeasureTheory.volume.restrict J)))
(hD : ∀ (n : ℕ), MeasureTheory.MemLp (D n) 2 ((MeasureTheory.volume.restrict Ω).prod (MeasureTheory.volume.restrict J)))
(hd : MeasureTheory.MemLp d 2 ((MeasureTheory.volume.restrict Ω).prod (MeasureTheory.volume.restrict J)))
(hUconv :
Filter.Tendsto
(fun (n : ℕ) =>
MeasureTheory.eLpNorm (U n - u) 3 ((MeasureTheory.volume.restrict Ω).prod (MeasureTheory.volume.restrict J)))
Filter.atTop (nhds 0))
(hDweak :
∀ (w : Foundation.Parabolic.Vec3 × ℝ → ℝ),
MeasureTheory.MemLp w 2 ((MeasureTheory.volume.restrict Ω).prod (MeasureTheory.volume.restrict J)) →
Filter.Tendsto
(fun (n : ℕ) =>
∫ (z : Foundation.Parabolic.Vec3 × ℝ), D n z * w z ∂(MeasureTheory.volume.restrict Ω).prod (MeasureTheory.volume.restrict J))
Filter.atTop
(nhds
(∫ (z : Foundation.Parabolic.Vec3 × ℝ), d z * w z ∂(MeasureTheory.volume.restrict Ω).prod (MeasureTheory.volume.restrict J))))
(hgrad :
∀ (n : ℕ),
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, HasWeakPartialDerivOn Ω j (fun (x : Vec 3) => U n (x, t)) fun (x : Vec 3) => D n (x, t))
:
Weak L² convergence of a spatial derivative and strong L³
convergence of its primitive preserve the almost-every-time weak derivative
identity on a local box.