Stability Energy Test

Supporting estimates for the Navier–Stokes development.

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

A smooth compactly supported energy test is essentially bounded on each local box.