Compactness Joint Extract

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.exists_common_velocity_gradient_subsequence {U : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hU : IsOpen U) (hI : IsOpen I) (u : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (Du : ℕ → Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Foundation.Parabolic.Vec3) (huMeas : ∀ (n : ℕ), Measurable (u n)) (hDuMeas : ∀ (n : ℕ), Measurable (Du 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) (hgradBound : ∀ (C : Set Foundation.Parabolic.Vec3), IsCompact C → C ⊆ U → ∀ (J : Set ℝ), IsCompact J → J ⊆ I → ∃ G < ⊤, ∀ (n : ℕ), ∫⁻ (t : ℝ) in J, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (spatialGradientSq (u n) (Du n) (x, t)) ≤ G) (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 ^ θ) : ∃ (K : ℕ → Set Foundation.Parabolic.Vec3) (χ : ℕ → Foundation.Parabolic.Vec3 → ℝ) (J : ℕ → Set ℝ), (∀ (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) ∧ (∀ (j : ℕ), IsCompact (J j) ∧ J j ⊆ I ∧ J j ⊆ J (j + 1) ∧ J j ⊆ interior (J (j + 1))) ∧ ⋃ (j : ℕ), J j = I ∧ ∃ (hmem : ∀ (n j : ℕ) (t : ↑I), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => χ j x • WithLp.toLp 2 (u n (x, ↑t))) 2 MeasureTheory.volume) (σ : ℕ → ℕ), StrictMono σ ∧ ∃ (V : ℕ → ↑I → ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 MeasureTheory.volume)) (D : (j : ℕ) → ↥(MeasureTheory.Lp CompactnessGradientFiber 2 ((MeasureTheory.volume.restrict (K j)).prod (MeasureTheory.volume.restrict (J j))))), (∀ (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) < ε) ∧ ∀ (j : ℕ), ∃ (hgrad : ∀ (k : ℕ), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => toCompactnessGradientFiber (Du (σ k) z)) 2 ((MeasureTheory.volume.restrict (K j)).prod (MeasureTheory.volume.restrict (J j)))), ∀ (w : ↥(MeasureTheory.Lp CompactnessGradientFiber 2 ((MeasureTheory.volume.restrict (K j)).prod (MeasureTheory.volume.restrict (J j))))), Filter.Tendsto (fun (k : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => toCompactnessGradientFiber (Du (σ k) z)) ⋯) w) Filter.atTop (nhds (inner ℝ (D j) w))

The velocity slices and gradient fields admit a common subsequence on countable spatial and temporal exhaustions.