Compactness Gradient Diagonal

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.exists_common_subsequence_weak_limit_of_bounded {ι : Type u_1} [Countable ι] {E : ι → Type u_2} [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → InnerProductSpace ℝ (E i)] [∀ (i : ι), CompleteSpace (E i)] [∀ (i : ι), TopologicalSpace.SeparableSpace (E i)] (u : ℕ → (i : ι) → E i) (C : ι → ℝ) (hC : ∀ (i : ι), 0 ≤ C i) (hbound : ∀ (n : ℕ) (i : ι), ‖u n i‖ ≤ C i) : ∃ (σ : ℕ → ℕ), StrictMono σ ∧ ∃ (v : (i : ι) → E i), ∀ (i : ι) (x : E i), Filter.Tendsto (fun (n : ℕ) => inner ℝ (u (σ n) i) x) Filter.atTop (nhds (inner ℝ (v i) x))

A countable family of uniformly bounded Hilbert-space sequences has one subsequence that converges weakly in every member of the family.