Stability Test Bounds

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_timePartial_memLp_top {Ω Ω' : Set Foundation.Parabolic.Vec3} {I J : Set ℝ} (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (hφ : φ ∈ spaceTimeTestFunction Ω I) (i : Fin 3) : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => timePartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) z) ⊤ (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))

The time derivative of a component of a smooth compactly supported momentum test is bounded on every local box.

theorem CKN.stability_spatialPartial_memLp_top {Ω Ω' : Set Foundation.Parabolic.Vec3} {I J : Set ℝ} (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (hφ : φ ∈ spaceTimeTestFunction Ω I) (i j : Fin 3) : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) j z) ⊤ (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))

A spatial derivative of a component of a smooth momentum test is bounded on every local box.

theorem CKN.stability_testDivergence_memLp_top {Ω Ω' : Set Foundation.Parabolic.Vec3} {I J : Set ℝ} (φ : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (hφ : φ ∈ spaceTimeTestFunction Ω I) : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.ParabolicPoint) => ∑ i : Fin 3, spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w i) i z) ⊤ (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))

The divergence of a smooth momentum test is bounded on every local box.