bounded_subseq_tendsto
plain-language theorem explainer
In a proper metric space every sequence bounded inside a closed ball admits a convergent subsequence along some strictly increasing index map. Navier-Stokes analysts working in Fourier space cite this to start the diagonal extraction for double sequences. The proof splits on the sign of the radius bound and invokes compactness of the closed ball to obtain the subsequence.
Claim. Let $X$ be a proper metric space. Let $f:ℕ→X$ and $c∈X$ satisfy dist$(f(n),c)≤R$ for every $n∈ℕ$. Then there exist a strictly increasing map $φ:ℕ→ℕ$ and a point $x∈X$ such that $f∘φ$ converges to $x$ as $n→∞$.
background
The FourierExtraction module constructs Cantor diagonal extraction for bounded sequences in proper metric spaces; every result is proved with no axioms or sorry. This theorem supplies the single-sequence subsequence tool that the composed extraction CE and the column limits CL are built from. It draws on compactness of closed balls together with order transitivity from ArithmeticFromLogic.
proof idea
The tactic proof cases on whether $R≥0$. The nonnegative branch applies tendsto_subseq to the compact closed ball, feeding the membership proof from the bound hypothesis. The negative branch obtains a contradiction by combining dist_nonneg with the bound at index zero via le_trans.
why it matters
This extraction lemma is the base case for the entire diagonal construction in the module, directly supplying the choose and choose_spec data used by CE, CL, LE, CE_strictMono, CE_conv_at and the remaining convergence statements. It therefore underpins the main nat_diagonal_extraction result that produces the limit function g(m) for every column m. In the Recognition framework it supplies the subsequence guarantee needed when bounded sequences appear in the Fourier-space treatment of the Navier-Stokes equations derived from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.