Compactness Representative Weak

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.tendsto_mollified_component_of_weak_cutoff {I : Set ℝ} (u : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (σ : ℕ → ℕ) (χ : Foundation.Parabolic.Vec3 → ℝ) (hmem : ∀ (n : ℕ) (t : ↑I), MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => χ y • WithLp.toLp 2 (u n (y, ↑t))) 2 MeasureTheory.volume) (V : ↑I → ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 MeasureTheory.volume)) (hweak : ∀ (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) => χ y • WithLp.toLp 2 (u (σ k) (y, ↑t))) ⋯) x) Filter.atTop (nhds (inner ℝ (V t) x))) (m : ℕ) (x : Foundation.Parabolic.Vec3) (i : Fin 3) (t : ↑I) (hχ : ∀ (y : Vec 3), mollifier (sliceRadius m) ⋯ (x - y) ≠ 0 → χ y = 1) : Filter.Tendsto (fun (k : ℕ) => mollify (fun (y : Vec 3) => u (σ k) (y, ↑t) i) (sliceRadius m) ⋯ x) Filter.atTop (nhds (inner ℝ (V t) (MeasureTheory.MemLp.toLp (fun (y : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (Pi.single i (mollifier (sliceRadius m) ⋯ (x - y)))) ⋯)))

At a fixed spatial scale, weak convergence of cutoff slices identifies the pointwise limit of their mollifications at every time.

theorem CKN.Leray.eventually_mollified_component_eq_weak_slice {I : Set ℝ} {K W : Set Foundation.Parabolic.Vec3} (hK : IsCompact K) (hW : IsOpen W) (hKW : K ⊆ W) (u : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (σ : ℕ → ℕ) (χ : Foundation.Parabolic.Vec3 → ℝ) (hχone : ∀ x ∈ W, χ x = 1) (hmem : ∀ (n : ℕ) (t : ↑I), MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => χ y • WithLp.toLp 2 (u n (y, ↑t))) 2 MeasureTheory.volume) (V : ↑I → ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 MeasureTheory.volume)) (hweak : ∀ (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) => χ y • WithLp.toLp 2 (u (σ k) (y, ↑t))) ⋯) x) Filter.atTop (nhds (inner ℝ (V t) x))) (t : ↑I) (x : Foundation.Parabolic.Vec3) : x ∈ K → ∀ (i : Fin 3), ∀ᶠ (m : ℕ) in Filter.atTop, (Filter.atTop.limUnder fun (k : ℕ) => mollify (fun (y : Foundation.Parabolic.Vec3) => u (σ k) (y, ↑t) i) (sliceRadius m) ⋯ x) = mollify (fun (y : Foundation.Parabolic.Vec3) => (↑↑(V t) y).ofLp i) (sliceRadius m) ⋯ x

On a compact region where a cutoff is one, all sufficiently small mollifications converge to those of the weak slice limit.

theorem CKN.Leray.compactnessMollifiedLimit_ae_eq_weak_slice {I : Set ℝ} {K W : Set Foundation.Parabolic.Vec3} (hK : IsCompact K) (hW : IsOpen W) (hKW : K ⊆ W) (u : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (σ : ℕ → ℕ) (χ : Foundation.Parabolic.Vec3 → ℝ) (hχone : ∀ x ∈ W, χ x = 1) (hmem : ∀ (n : ℕ) (t : ↑I), MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => χ y • WithLp.toLp 2 (u n (y, ↑t))) 2 MeasureTheory.volume) (V : ↑I → ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 MeasureTheory.volume)) (hweak : ∀ (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) => χ y • WithLp.toLp 2 (u (σ k) (y, ↑t))) ⋯) x) Filter.atTop (nhds (inner ℝ (V t) x))) (t : ↑I) : ∀ᵐ (x : Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict K, compactnessMollifiedLimit u σ (x, ↑t) = fun (i : Fin 3) => (↑↑(V t) x).ofLp i

The jointly measurable mollified limit represents every weak slice on each compact region where the selected cutoff is one nearby.