Compactness Strong Local #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.Leray.strong_l2_on_compacts_of_exhaustion
{U : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
(K : ℕ → Set Foundation.Parabolic.Vec3)
(J : ℕ → Set ℝ)
(hKmono : ∀ (j : ℕ), K j ⊆ K (j + 1))
(hKinner : ∀ (j : ℕ), K j ⊆ interior (K (j + 1)))
(hKcover : ⋃ (j : ℕ), K j = U)
(hJmono : ∀ (j : ℕ), J j ⊆ J (j + 1))
(hJinner : ∀ (j : ℕ), J j ⊆ interior (J (j + 1)))
(hJcover : ⋃ (j : ℕ), J j = I)
(f : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.L2Vec3)
(g : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.L2Vec3)
(hstrong :
∀ (j : ℕ),
Filter.Tendsto
(fun (k : ℕ) =>
MeasureTheory.eLpNorm (f k - g) 2
((MeasureTheory.volume.restrict (K j)).prod (MeasureTheory.volume.restrict (J j))))
Filter.atTop (nhds 0))
(Q : Set (Foundation.Parabolic.Vec3 × ℝ))
:
IsCompact Q →
Q ⊆ U ×ˢ I →
Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (f k - g) 2 (MeasureTheory.volume.restrict Q)) Filter.atTop
(nhds 0)
Strong convergence on a nested rectangle exhaustion gives strong convergence on every compact subset of the open product domain.
theorem
CKN.Leray.compact_subset_inner_rectangle_exhaustion
{U : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
(K : ℕ → Set Foundation.Parabolic.Vec3)
(J : ℕ → Set ℝ)
(hKmono : ∀ (j : ℕ), K j ⊆ K (j + 1))
(hKinner : ∀ (j : ℕ), K j ⊆ interior (K (j + 1)))
(hKcover : ⋃ (j : ℕ), K j = U)
(hJmono : ∀ (j : ℕ), J j ⊆ J (j + 1))
(hJinner : ∀ (j : ℕ), J j ⊆ interior (J (j + 1)))
(hJcover : ⋃ (j : ℕ), J j = I)
(Q : Set (Foundation.Parabolic.Vec3 × ℝ))
(hQ : IsCompact Q)
(hQI : Q ⊆ U ×ˢ I)
:
Every compact subset of an open product domain lies in an open inner spatial member times a compact temporal member of nested exhaustions.