Stability Weak Component Local

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_weak_component_localBox {Ω Ω' : Set Foundation.Parabolic.Vec3} {I J : Set ℝ} (hbox : localBox Ω I Ω' J) (D : ℕ → Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (d : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (hweak : ∀ (i j : Fin 3) (w : Foundation.Parabolic.Vec3 × ℝ → ℝ), MeasureTheory.MemLp w 2 ((MeasureTheory.volume.restrict Ω').prod (MeasureTheory.volume.restrict J)) → Filter.Tendsto (fun (n : ℕ) => ∫ (z : Foundation.Parabolic.Vec3 × ℝ), D n (z.1, z.2) i j * w z ∂(MeasureTheory.volume.restrict Ω').prod (MeasureTheory.volume.restrict J)) Filter.atTop (nhds (∫ (z : Foundation.Parabolic.Vec3 × ℝ), d (z.1, z.2) i j * w z ∂(MeasureTheory.volume.restrict Ω').prod (MeasureTheory.volume.restrict J)))) (i j : Fin 3) (w : Foundation.Parabolic.ParabolicPoint → ℝ) (hw : MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) : Filter.Tendsto (fun (n : ℕ) => ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, D n z i j * w z) Filter.atTop (nhds (∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω' J, d z i j * w z))

Componentwise weak L² convergence in product coordinates transfers to CKN local-box integrals.