CE
plain-language theorem explainer
CE recursively builds the composed subsequence extractor for the first m columns of a bounded double sequence f in a proper metric space. Analysts applying diagonal arguments to extract convergent subsequences column-by-column would cite this construction. The definition proceeds by recursion on m, selecting at each step the subsequence guaranteed by bounded_subseq_tendsto and composing it with the extractor from the prior stage.
Claim. Let $f : ℕ → ℕ → X$ be a double sequence bounded in a proper metric space $X$, with $c ∈ X$ and $R ≥ 0$ such that $dist(f(n,m),c) ≤ R$ for all $n,m$. The function $CE(m) : ℕ → ℕ$ is the strictly increasing map obtained by composing the subsequence extractions for columns $0$ through $m$, so that $n ↦ f(CE(m)(n),j)$ converges for every $j ≤ m$.
background
The module implements Cantor diagonal extraction for bounded sequences in proper metric spaces, with all results proved without axioms or sorry. The key upstream tool is bounded_subseq_tendsto, which states: given a sequence $f : ℕ → X$ with $dist(f n,c) ≤ R$, there exist a strictly increasing $φ : ℕ → ℕ$ and a limit point $x$ such that $f ∘ φ$ converges to $x$ (proved via compactness of the closed ball). CE is the recursive object that assembles these extractions column by column.
proof idea
The definition is recursive on the column index. For $m=0$ it returns the strictly increasing map chosen by bounded_subseq_tendsto applied to the zeroth column. For successor $m+1$ it sets $φ := CE m$, extracts a new subsequence from the shifted sequence $n ↦ f(φ n, m+1)$ via another application of bounded_subseq_tendsto, and returns the composition $φ ∘ ψ$.
why it matters
CE is the central inductive construction in the Fourier extraction module. It is invoked directly by CE_conv_at, CE_conv_le, CE_strictMono, CE_factor, and the limit map CL to establish column-wise convergence and monotonicity. The construction supplies the inductive step of the Cantor diagonal argument, feeding the main result nat_diagonal_extraction that produces a single strictly increasing φ such that every column converges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.