Compactness Weak Local

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.weak_slices_to_compactnessMollifiedLimit_on_compact {U : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hI : IsOpen I) (u : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (σ : ℕ → ℕ) (huMeas : ∀ (n : ℕ), Measurable (u n)) (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) (hbound : ∀ (C : Set Foundation.Parabolic.Vec3), IsCompact C → C ⊆ U → ∀ (J : Set ℝ), IsCompact J → J ⊆ I → ∃ M < ⊤, ∀ (n : ℕ), ∀ t ∈ J, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u n (x, t))) ^ 2 ≤ M) (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))) (C : Set Foundation.Parabolic.Vec3) (hC : IsCompact C) (hCU : C ⊆ U) (t : ↑I) : ∃ (hs : ∀ (k : ℕ), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (u (σ k) (x, ↑t))) 2 (MeasureTheory.volume.restrict C)) (hl : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (compactnessMollifiedLimit u σ (x, ↑t))) 2 (MeasureTheory.volume.restrict C)), ∀ (w : ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 (MeasureTheory.volume.restrict C))), Filter.Tendsto (fun (k : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (u (σ k) (x, ↑t))) ⋯) w) Filter.atTop (nhds (inner ℝ (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (compactnessMollifiedLimit u σ (x, ↑t))) hl) w))

Every time slice of the selected subsequence converges weakly on every compact spatial subset to the jointly measurable representative.