Compactness Slice Representative

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.compactnessMollifiedLimit_ae_eq_on_exhaustion {I : Set ℝ} (u : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (σ : ℕ → ℕ) (K : ℕ → Set Foundation.Parabolic.Vec3) (χ : ℕ → Foundation.Parabolic.Vec3 → ℝ) (hK : ∀ (j : ℕ), IsCompact (K j) ∧ K j ⊆ K (j + 1) ∧ K j ⊆ interior (K (j + 1))) (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))) (j : ℕ) (t : ↑I) : ∀ᵐ (x : Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict (K j), compactnessMollifiedLimit u σ (x, ↑t) = fun (i : Fin 3) => (↑↑(V (j + 1) t) x).ofLp i

The measurable mollified representative agrees with every weak slice limit on the compact exhaustion.

theorem CKN.Leray.compactnessMollifiedLimit_memLp_on_exhaustion {I : Set ℝ} (u : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (σ : ℕ → ℕ) (K : ℕ → Set Foundation.Parabolic.Vec3) (χ : ℕ → Foundation.Parabolic.Vec3 → ℝ) (hK : ∀ (j : ℕ), IsCompact (K j) ∧ K j ⊆ K (j + 1) ∧ K j ⊆ interior (K (j + 1))) (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))) (j : ℕ) (t : ↑I) : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (compactnessMollifiedLimit u σ (x, ↑t))) 2 (MeasureTheory.volume.restrict (K j))

The measurable representative has the same L² class as the local weak limit on every member of the exhaustion.

theorem CKN.Leray.memLp_original_slice_on_exhaustion {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) (hK : ∀ (j : ℕ), IsCompact (K j) ∧ K j ⊆ U) (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) (n j : ℕ) (t : ↑I) : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (u n (x, ↑t))) 2 (MeasureTheory.volume.restrict (K j))

Uniform local slice energy puts each original slice in the L² space of every compact member of the spatial exhaustion.

theorem CKN.Leray.weak_slices_to_compactnessMollifiedLimit_on_exhaustion {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))) (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))) (j : ℕ) (t : ↑I) : ∃ (hsource : ∀ (k : ℕ), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (u (σ k) (x, ↑t))) 2 (MeasureTheory.volume.restrict (K j))) (hlimit : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (compactnessMollifiedLimit u σ (x, ↑t))) 2 (MeasureTheory.volume.restrict (K j))), ∀ (w : ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 (MeasureTheory.volume.restrict (K j)))), 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))) hlimit) w))

At every time, the original slices converge weakly to the jointly measurable representative on each compact member of the exhaustion.