LE_conv
The theorem establishes that the subsequence obtained by feeding the local extraction LE(m) into the composed extraction CE(m) converges in the (m+1)-th column to the column limit CL(m+1). Analysts building diagonal arguments for double-indexed bounded sequences in proper metric spaces cite it to close the inductive step on column convergence. The proof is a direct one-line extraction of the Tendsto component from the choose specification of bounded_subseq_tendsto applied to the relevant column sequence.
claimLet $f : ℕ → ℕ → X$ be bounded in a proper metric space with center $c$ and radius $R$. For each $m ∈ ℕ$, the sequence $n ↦ f(CE(m)(LE(m,n)), m+1)$ converges to $CL(m+1)$ as $n → ∞$, where $CE(m)$ is the composed extraction making columns $0$ through $m$ converge, $LE(m)$ is the local extraction chosen for column $m+1$, and $CL(m+1)$ is the corresponding column limit.
background
The module develops Cantor diagonal extraction for a double sequence $f : ℕ → ℕ → X$ that is bounded in a proper metric space. The supporting definitions are: CE, the composed extraction that iteratively selects subsequences so columns $0$ to $m$ converge; CL, the function recording the limit of column $m$ under the extraction up to $m-1$; and LE, the local extraction that selects the subsequence making column $m+1$ converge when composed with CE(m). These rest on the upstream theorem bounded_subseq_tendsto, which asserts that any bounded sequence in a proper metric space admits a strictly monotone subsequence converging to some point in the space.
proof idea
The proof is a one-line term that applies the choose specification of bounded_subseq_tendsto to the column sequence fun n => f (CE m n) (m+1). It extracts the second component of choose_spec.choose_spec, which is precisely the required Tendsto statement to the column limit CL(m+1).
why it matters in Recognition Science
LE_conv supplies the successor case for the main convergence result CE_conv_at, which states that the composed extraction CE(m) makes column m converge to CL(m) for every m. This completes the columnwise convergence needed for the module's diagonal extraction theorem. In the Recognition Science setting the lemma supports analytic control of bounded sequences that appear in Fourier representations of fluid dynamics, consistent with the framework's use of unique limits and self-similar fixed points.
scope and limits
- Does not prove existence of the extraction functions CE or LE themselves.
- Does not supply convergence rates or quantitative bounds.
- Does not extend to sequences that are unbounded or to non-proper spaces.
- Does not address joint convergence in multiple columns simultaneously.
Lean usage
exact LE_conv f c R hf kformal statement (Lean)
81private theorem LE_conv (m : ℕ) :
82 Tendsto (fun n => f (CE f c R hf m (LE f c R hf m n)) (m + 1)) atTop
83 (𝓝 (CL f c R hf (m + 1))) :=
proof body
Term-mode proof.
84 (bounded_subseq_tendsto (fun n => f (CE f c R hf m n) (m + 1)) c R
85 (fun n => hf (CE f c R hf m n) (m + 1))).choose_spec.choose_spec.2
86