Stability Local Product Lp

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_eLpNorm_tendsto_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) (G : Foundation.Parabolic.ParabolicPoint → E) (hF : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (F n) (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) (hG : MeasureTheory.AEStronglyMeasurable G (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) (hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - G) r (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (fun (z : Foundation.Parabolic.Vec3 × ℝ) => F n (z.1, z.2) - G (z.1, z.2)) r ((MeasureTheory.volume.restrict Ω').prod (MeasureTheory.volume.restrict J))) Filter.atTop (nhds 0)

Strong convergence on a CKN local box agrees with strong convergence in its ordinary product coordinates.