Compactness Time Glue

Supporting estimates for the Navier–Stokes development.

@[reducible, inline]

abbrev CKN.Leray.RationalTimeSlice {I : Set ℝ} (p : RationalCompactTimeWindow I) : Type

The compact time interval indexed by a rational window.

Equations

• CKN.Leray.RationalTimeSlice p = { t : ℝ // t ∈ Set.Icc ↑(↑p).1 ↑(↑p).2 }

theorem CKN.Leray.exists_all_time_weak_limit_from_rational_windows {I : Set ℝ} (hI : IsOpen I) {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : ℕ → ℝ → E) (v : (p : RationalCompactTimeWindow I) → RationalTimeSlice p → E) (hweak : ∀ (p : RationalCompactTimeWindow I) (t : RationalTimeSlice p) (x : E), Filter.Tendsto (fun (n : ℕ) => inner ℝ (f n ↑t) x) Filter.atTop (nhds (inner ℝ (v p t) x))) (hcontinuous : ∀ (p : RationalCompactTimeWindow I) (x : E), Continuous fun (t : RationalTimeSlice p) => inner ℝ (v p t) x) : ∃ (V : ↑I → E), (∀ (t : ↑I) (x : E), Filter.Tendsto (fun (n : ℕ) => inner ℝ (f n ↑t) x) Filter.atTop (nhds (inner ℝ (V t) x))) ∧ ∀ (x : E), Continuous fun (t : ↑I) => inner ℝ (V t) x

Weak limits selected on rational compact windows agree on overlaps and give an every-time weak limit with continuous scalar pairings.

theorem CKN.Leray.exists_common_subsequence_all_time_weak_limit {I : Set ℝ} (hI : IsOpen I) {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (f : ℕ → ℕ → ℝ → E) (ψ : ℕ → E) (hψ : DenseRange ψ) (C : ℕ → RationalCompactTimeWindow I → ℝ) (hC : ∀ (j : ℕ) (p : RationalCompactTimeWindow I), 0 ≤ C j p) (hbound : ∀ (n j : ℕ) (p : RationalCompactTimeWindow I), ∀ t ∈ Set.Icc ↑(↑p).1 ↑(↑p).2, ‖f n j t‖ ≤ C j p) (hmod : ∀ (j : ℕ) (p : RationalCompactTimeWindow I) (m : ℕ), ∃ (A : ℝ) (B : ℝ) (θ : ℝ), 0 ≤ A ∧ 0 ≤ B ∧ 0 < θ ∧ ∀ (n : ℕ) (s t : RationalTimeSlice p), |inner ℝ (f n j ↑t) (ψ m) - inner ℝ (f n j ↑s) (ψ m)| ≤ A * dist t s + B * dist t s ^ θ) : ∃ (σ : ℕ → ℕ), StrictMono σ ∧ ∃ (V : ℕ → ↑I → E), (∀ (j : ℕ) (t : ↑I) (x : E), Filter.Tendsto (fun (n : ℕ) => inner ℝ (f (σ n) j ↑t) x) Filter.atTop (nhds (inner ℝ (V j t) x))) ∧ (∀ (j : ℕ) (x : E), Continuous fun (t : ↑I) => inner ℝ (V j t) x) ∧ ∀ (j : ℕ) (p : RationalCompactTimeWindow I) (x : E) (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (t : RationalTimeSlice p), dist (inner ℝ (f (σ n) j ↑t) x) (inner ℝ (V j ⟨↑t, ⋯⟩) x) < ε

A single subsequence works for countably many Hilbert-valued slice families on all times of an open interval.

theorem CKN.Leray.eventually_uniform_on_compact_of_rational_windows {I J : Set ℝ} (hI : IsOpen I) (hJ : IsCompact J) (hJI : J ⊆ I) (a : ℕ → ↑I → ℝ) (b : ↑I → ℝ) (hwindow : ∀ (p : RationalCompactTimeWindow I) (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (t : RationalTimeSlice p), dist (a n ⟨↑t, ⋯⟩) (b ⟨↑t, ⋯⟩) < ε) (ε : ℝ) : 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (t : ℝ) (ht : t ∈ J), dist (a n ⟨t, ⋯⟩) (b ⟨t, ⋯⟩) < ε

Uniform convergence on rational compact windows extends to every compact time set inside the open domain.