Compactness Strong

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.exists_limit_of_cauchy_uniform_approximations {E : Type u_1} [NormedAddCommGroup E] [CompleteSpace E] (f : ℕ → E) (P : ℕ → ℕ → E) (hP : ∀ (m : ℕ), CauchySeq fun (n : ℕ) => P m n) (happrox : ∀ (ε : ℝ), 0 < ε → ∃ (m : ℕ), ∀ (n : ℕ), dist (f n) (P m n) < ε) : ∃ (g : E), Filter.Tendsto f Filter.atTop (nhds g)

If a sequence admits arbitrarily accurate uniform approximations by sequences that are Cauchy, then it converges in a complete normed space. This is the final Cauchy step for the finite ball-average approximations in lem:compactness.

theorem CKN.Leray.cauchySeq_of_approximating_cauchy_sequences {E : Type u_1} [PseudoMetricSpace E] (f : ℕ → E) (happrox : ∀ (ε : ℝ), 0 < ε → ∃ (p : ℕ → E), CauchySeq p ∧ ∀ (n : ℕ), dist (f n) (p n) < ε) : CauchySeq f

If every requested accuracy admits a Cauchy approximating sequence, then the original sequence is Cauchy. This is the radius-by-radius form used when each finite ball cover has its own finite index type.