Compactness Pairing Continuity

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.continuous_compactnessMollifiedLimit_local_pairing {U : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (u : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (σ : ℕ → ℕ) (K : ℕ → Set Foundation.Parabolic.Vec3) (χ : ℕ → Foundation.Parabolic.Vec3 → ℝ) (hK : ∀ (j : ℕ), IsCompact (K j) ∧ K j ⊆ U ∧ K j ⊆ K (j + 1) ∧ K j ⊆ interior (K (j + 1))) (hKcover : ⋃ (j : ℕ), K j = U) (hχ : ∀ (j : ℕ), ∀ x ∈ K j, χ j x = 1) (hmem : ∀ (n j : ℕ) (t : ↑I), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => χ j x • WithLp.toLp 2 (u n (x, ↑t))) 2 MeasureTheory.volume) (V : ℕ → ↑I → ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 MeasureTheory.volume)) (hweak : ∀ (j : ℕ) (t : ↑I) (x : ↥(MeasureTheory.Lp (WithLp 2 Foundation.Parabolic.Vec3) 2 MeasureTheory.volume)), Filter.Tendsto (fun (k : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (fun (y : Foundation.Parabolic.Vec3) => χ j y • WithLp.toLp 2 (u (σ k) (y, ↑t))) ⋯) x) Filter.atTop (nhds (inner ℝ (V j t) x))) (hVcont : ∀ (j : ℕ) (x : ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 MeasureTheory.volume)), Continuous fun (t : ↑I) => inner ℝ (V j t) x) (C : Set Foundation.Parabolic.Vec3) (hC : IsCompact C) (hCU : C ⊆ U) (w : ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 (MeasureTheory.volume.restrict C))) : Continuous fun (t : ↑I) => ∫ (x : Foundation.Parabolic.Vec3) in C, ∑ i : Fin 3, compactnessMollifiedLimit u σ (x, ↑t) i * (↑↑w x).ofLp i

Pairing the selected representative against a fixed local L² test is continuous in time.