nat_diagonal_extraction
plain-language theorem explainer
Cantor diagonal extraction yields a strictly monotone index φ and columnwise limits g such that the subsequence f(φ(n), m) converges to g(m) for each m, given a bounded double sequence in a proper metric space. Analysts working on subsequential limits for double sequences would cite it to justify diagonal arguments in metric spaces. The proof is a one-line term packaging the pre-built diagonal selector D, the column limit map CL, and the supporting monotonicity and convergence theorems.
Claim. Let $(X,d)$ be a proper metric space, $c ∈ X$, $R > 0$, and let $f:ℕ→ℕ→X$ satisfy $d(f(n,m),c)≤R$ for all $n,m$. Then there exist a strictly increasing map $φ:ℕ→ℕ$ and a map $g:ℕ→X$ such that for every fixed $m$, $f(φ(n),m)→g(m)$ as $n→∞$.
background
The module supplies subsequential extraction tools for Fourier-space analysis. Its core objects are the diagonal index D (a strictly increasing selector built recursively) and the column limit map CL, defined by iterated application of bounded-subsequence extraction: CL(0) is the limit of a convergent subsequence of the zeroth column, while CL(m+1) extracts a further subsequence from the previous diagonal applied to column m+1. Properness of the metric space guarantees that closed balls are compact, enabling the existence of these convergent subsequences. Upstream lemmas D_strictMono and D_converges record that D is strictly monotone and that the extracted sequences converge pointwise to the values of CL.
proof idea
The proof is a one-line term that directly supplies the witnesses: D f c R hf as the strictly monotone index φ, CL f c R hf as the limit sequence g, D_strictMono f c R hf for the monotonicity claim, and D_converges f c R hf for the pointwise convergence at each column.
why it matters
This is the main theorem of the FourierExtraction module and supplies the Cantor diagonal argument required for extracting convergent subsequences from bounded double sequences. The module documentation presents it as the central proved result with no axioms or sorrys. It has no recorded downstream uses yet but forms the extraction infrastructure for subsequent Fourier-coefficient manipulations in the Navier-Stokes setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.