CE_conv_le
plain-language theorem explainer
The theorem states that the composed extraction CE at level m makes every column j ≤ m converge to its limit CL(j) under the subsequence index. Analysts using diagonal arguments for bounded sequences in proper metric spaces cite it to control uniform columnwise convergence. The proof is by induction on m: the base case invokes CE_conv_at directly, while the successor step splits on whether j equals the new level or is smaller and applies CE_succ together with tendsto_comp_strictMono and LE_strictMono.
Claim. For all natural numbers $m,j$ with $j≤m$, the sequence $n↦f(CE(f,c,R,hf,m,n),j)$ converges to $CL(f,c,R,hf,j)$ as $n→∞$, where $CE(m)$ is the recursively composed subsequence extraction that forces columns $0$ through $m$ to converge and $CL(j)$ is the corresponding column limit.
background
The module implements Cantor diagonal extraction for a bounded sequence $f:ℕ→ℕ→X$ in a proper metric space. The auxiliary definition CE builds a strictly increasing index map recursively: at step 0 it extracts a convergent subsequence for column 0; at step $m+1$ it composes the previous map with a fresh extraction on the already-extracted subsequence for column $m+1$. The companion definition CL records the resulting columnwise limits. The upstream lemma CE_conv_at already gives convergence on the diagonal (column $m$ under CE($m$)), while CE_succ records the composition identity CE($m+1$)=CE($m$)∘LE($m$) and LE_strictMono asserts that each local extraction map is strictly increasing.
proof idea
Proof by induction on $m$. For the base case $m=0$ the hypothesis $j≤0$ forces $j=0$ and the claim reduces to CE_conv_at at 0. In the successor case $m=k+1$, if $j=k+1$ the claim is again CE_conv_at at $k+1$. If $j<k+1$ the composition identity CE_succ rewrites the sequence as the composition of the inductive hypothesis sequence with LE($k$); tendsto_comp_strictMono then lifts the inductive convergence through the strictly monotone LE($k$) supplied by LE_strictMono.
why it matters
The result completes the induction that CE($m$) forces convergence of every column up to $m$, which is the key inductive step inside the module’s main theorem nat_diagonal_extraction. Without it the diagonal argument would only control the highest column at each stage; the lemma therefore supplies the uniform columnwise control required for the full subsequence extraction. It sits inside the Fourier-space extraction layer used for the Navier–Stokes analysis and inherits the module’s guarantee that all steps are proved without axioms or sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.