CE
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not produce a single extractor that works for all columns simultaneously without the auxiliary limit map CL.
- Does not apply to sequences that are unbounded or to spaces that are not proper metric spaces.
- Does not supply an explicit closed-form expression for the extractor, only a recursive definition via choice.
- Does not guarantee uniqueness of the extracted subsequence.
formal statement (Lean)
45private noncomputable def CE : ℕ → (ℕ → ℕ)
46 | 0 => (bounded_subseq_tendsto (fun n => f n 0) c R (fun n => hf n 0)).choose
47 | m + 1 =>
48 let φ := CE m
proof body
Definition body.
49 let ψ := (bounded_subseq_tendsto (fun n => f (φ n) (m + 1)) c R
50 (fun n => hf (φ n) (m + 1))).choose
51 φ ∘ ψ
52
53/-- Limit at column m. -/