Compactness Slice

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.exists_cutoff_l2_fields_of_local_slice_bounds {U : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hU : IsOpen U) (hI : IsOpen I) (u : ℕ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (huMeas : ∀ (n : ℕ), Measurable (u n)) (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) : ∃ (K : ℕ → Set Foundation.Parabolic.Vec3) (χ : ℕ → Foundation.Parabolic.Vec3 → ℝ), (∀ (j : ℕ), IsCompact (K j) ∧ K j ⊆ U ∧ K j ⊆ K (j + 1) ∧ K j ⊆ interior (K (j + 1))) ∧ ⋃ (j : ℕ), K j = U ∧ (∀ (j : ℕ), ContDiff ℝ (↑⊤) (χ j) ∧ HasCompactSupport (χ j) ∧ tsupport (χ j) ⊆ U ∧ (∀ (x : Foundation.Parabolic.Vec3), χ j x ∈ Set.Icc 0 1) ∧ ∀ x ∈ K j, χ j x = 1) ∧ ∀ (n j : ℕ) (t : ↑I), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => χ j x • WithLp.toLp 2 (u n (x, ↑t))) 2 MeasureTheory.volume

Local slice energy bounds supply global L² fields after multiplication by the cutoffs of a compact exhaustion.

theorem CKN.Leray.cutoff_l2_norm_bound_on_time_window {J : Set ℝ} (u : ℕ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (huMeas : ∀ (n : ℕ), Measurable (u n)) (χ : Foundation.Parabolic.Vec3 → ℝ) (hχsmooth : ContDiff ℝ (↑⊤) χ) (hχcompact : HasCompactSupport χ) (hχrange : ∀ (x : Foundation.Parabolic.Vec3), χ x ∈ Set.Icc 0 1) (hmem : ∀ (n : ℕ), ∀ t ∈ J, MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => χ x • WithLp.toLp 2 (u n (x, t))) 2 MeasureTheory.volume) (M : ENNReal) (hM : M < ⊤) (hbound : ∀ (n : ℕ), ∀ t ∈ J, ∫⁻ (x : Foundation.Parabolic.Vec3) in tsupport χ, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u n (x, t))) ^ 2 ≤ M) (n : ℕ) (t : ℝ) (ht : t ∈ J) : ‖MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => χ x • WithLp.toLp 2 (u n (x, t))) ⋯‖ ≤ (M ^ (1 / 2)).toReal

A compact-time slice energy bound controls the norms of the corresponding global cutoff L² fields.

theorem CKN.Leray.exists_common_subsequence_cutoff_weak_slices {U : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hI : IsOpen I) (u : ℕ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (huMeas : ∀ (n : ℕ), Measurable (u n)) (χ : ℕ → Foundation.Parabolic.Vec3 → ℝ) (hχ : ∀ (j : ℕ), ContDiff ℝ (↑⊤) (χ j) ∧ HasCompactSupport (χ j) ∧ tsupport (χ j) ⊆ U ∧ ∀ (x : Foundation.Parabolic.Vec3), χ j x ∈ Set.Icc 0 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) (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) (hmod : ∀ (C : Set Foundation.Parabolic.Vec3), IsCompact C → C ⊆ U → ∀ (J : Set ℝ), IsCompact J → J ⊆ I → ∀ (w : Foundation.Parabolic.Vec3 → Foundation.Parabolic.L2Vec3), ContDiff ℝ (↑⊤) w → HasCompactSupport w → tsupport w ⊆ C → ∃ (A : ℝ) (B : ℝ) (θ : ℝ), 0 ≤ A ∧ 0 ≤ B ∧ 0 < θ ∧ ∀ (n : ℕ) (s t : ℝ), s ∈ J → t ∈ J → |(∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u n (x, t) i * (w x).ofLp i) - ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u n (x, s) i * (w x).ofLp i| ≤ A * dist t s + B * dist t s ^ θ) : ∃ (σ : ℕ → ℕ), StrictMono σ ∧ ∃ (V : ℕ → ↑I → ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 MeasureTheory.volume)), (∀ (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 : ℕ) (x : ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 MeasureTheory.volume)), Continuous fun (t : ↑I) => inner ℝ (V j t) x) ∧ ∀ (j : ℕ) (p : RationalCompactTimeWindow I) (x : ↥(MeasureTheory.Lp (WithLp 2 Foundation.Parabolic.Vec3) 2 MeasureTheory.volume)) (ε : ℝ), 0 < ε → ∀ᶠ (k : ℕ) in Filter.atTop, ∀ (t : RationalTimeSlice p), dist (inner ℝ (MeasureTheory.MemLp.toLp (fun (y : Foundation.Parabolic.Vec3) => χ j y • WithLp.toLp 2 (u (σ k) (y, ↑t))) ⋯) x) (inner ℝ (V j ⟨↑t, ⋯⟩) x) < ε

The local slice bounds and smooth-test time modulus select one subsequence whose cutoff slices converge weakly at every time.