Compactness Product Slices

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.exists_subsequence_ae_slices_of_strong_product_l2 {K : Set Foundation.Parabolic.Vec3} {J : Set ℝ} (f : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.L2Vec3) (g : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.L2Vec3) (hf : ∀ (n : ℕ), MeasureTheory.MemLp (f n) 2 ((MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J))) (hg : MeasureTheory.MemLp g 2 ((MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J))) (hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - g) 2 ((MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J))) Filter.atTop (nhds 0)) : ∃ (τ : ℕ → ℕ), StrictMono τ ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, ∀ᵐ (x : Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict K, Filter.Tendsto (fun (k : ℕ) => f (τ k) (x, t)) Filter.atTop (nhds (g (x, t)))

Strong convergence on a product has a subsequence converging pointwise almost everywhere on almost every spatial slice.