CE_conv_at
plain-language theorem explainer
The theorem asserts pointwise convergence of each column under the composed extraction map to its designated limit in a bounded double sequence. Analysts constructing diagonal subsequences for sequences indexed by two naturals in proper metric spaces would reference it to confirm columnwise limits. The argument proceeds by case analysis on the column index, delegating the base case to the subsequence extraction theorem and successor cases to the local convergence lemma.
Claim. Let $f : ℕ → ℕ → X$ be bounded in a proper metric space $X$ with center $c$ and radius $R$. For every column index $m$, the sequence $n ↦ f(φ_m(n), m)$ converges to the column limit $L_m$ as $n → ∞$, where $φ_m$ is the composed extraction up to column $m$ and $L_m$ is the corresponding limit point.
background
The FourierExtraction module constructs a diagonal subsequence for a double-indexed bounded sequence $f : ℕ → ℕ → X$ in a proper metric space, guaranteeing that every column converges. The composed extraction is defined recursively: it begins with the subsequence chosen by bounded_subseq_tendsto for column 0 and at each successor composes the prior extraction with a new subsequence extraction for the next column. The column limit is the point to which the extracted subsequence converges at that column, again chosen via bounded_subseq_tendsto. This local setting supports the main result nat_diagonal_extraction by ensuring all columns stabilize under the final diagonal map. Upstream, bounded_subseq_tendsto guarantees a strictly monotone extraction with convergent image for any bounded sequence in a proper space.
proof idea
The proof opens with intro m and then cases on m. The zero case extracts the convergence specification directly from the choose_spec of bounded_subseq_tendsto applied to the zeroth column sequence. The successor case invokes the lemma LE_conv, which itself applies bounded_subseq_tendsto to the image of the prior extraction at the next column.
why it matters
CE_conv_at supplies the columnwise convergence needed for the inductive extension in CE_conv_le and for the final diagonal convergence in D_converges. It fills the convergence verification step in the Cantor diagonal construction described in the module documentation for Fourier-space extraction. Within the Recognition Science framework this supports subsequence limits required for analyzing the Fourier-transformed Navier-Stokes equations, closing one link in the chain from boundedness to convergent subsequences.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.