Stability Energy Derivatives

Supporting estimates for the Navier–Stokes development.

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

The time derivative of a smooth energy test is bounded on a local box.

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

A second spatial derivative of a smooth energy test is bounded on a local box.

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

The coefficient of the quadratic energy term is bounded on a local box.

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

A first spatial derivative of a smooth energy test is bounded on a local box.