Stability Local Product Mem Lp

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_memLp_localBox_prod {E : Type u_1} [NormedAddCommGroup E] {Ω Ω' : Set Foundation.Parabolic.Vec3} {I J : Set ℝ} (hbox : localBox Ω I Ω' J) {r : ENNReal} {f : Foundation.Parabolic.ParabolicPoint → E} (hf : MeasureTheory.MemLp f r (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => f (z.1, z.2)) r ((MeasureTheory.volume.restrict Ω').prod (MeasureTheory.volume.restrict J))

Local Lᵖ membership agrees in CKN and product coordinates.