D_converges
D_converges shows that the diagonal sequence D(n) = CE(n,n) makes the m-th column of f converge to the pre-chosen column limit CL(m) for every fixed m. Analysts constructing diagonal subsequences in proper metric spaces cite it to guarantee pointwise convergence after the recursive extraction steps. The argument reduces the claim to CE_conv_at by index decomposition via CE_factor and a max bound on the witness K.
claimLet $D(n) := CE(n,n)$ where $CE$ is the composed extraction that forces the first $m$ columns to converge, and let $CL(m)$ be the recursively chosen column limit. Then for each fixed $m$, the sequence $nmapsto f(D(n),m)$ converges to $CL(m)$ in the metric as $nto infty$.
background
The module constructs Cantor diagonal extraction for a bounded map $f:mathbb{N}to mathbb{N}to X$ in a proper metric space. The auxiliary $CE(m)$ is the composed extraction that selects a subsequence making columns 0 through $m$ converge; its definition recurses by applying bounded_subseq_tendsto at each new column. $CL(m)$ is the corresponding column limit, defined by choosing the limit of the extracted subsequence at step $m+1$ from the previous extraction at step $m$. $D$ is the diagonal map $D(n)=CE(n,n)$. The local setting is the fully proved extraction theorem nat_diagonal_extraction, which assembles $D$, $CL$, strict monotonicity of $D$, and the present convergence statement.
proof idea
The proof is a direct metric-space argument. It unfolds Tendsto atTop, invokes CE_conv_at to obtain a witness $K$ for the given $varepsilon$, then takes $ngeq max(m,K)$. It decomposes $n=m+p$, applies CE_factor to produce a strictly increasing $rho$ with $CE(m+p,m+p)=rho(m+p)$, rewrites the distance via $h_rho_eq$, and chains the inequality through $hK$ at the shifted index $rho(m+p)$ using le_trans.
why it matters in Recognition Science
D_converges supplies the convergence half of nat_diagonal_extraction, the main theorem that produces a strictly increasing $phi$ and pointwise limits $g(m)$ for any bounded sequence in a proper space. It closes the recursive construction begun by CE and CL, completing the FourierExtraction module's extraction result without axioms or sorrys. In the broader Recognition framework this supplies the subsequential tool needed for Fourier-space analysis of bounded sequences.
scope and limits
- Does not claim uniform convergence over all columns m simultaneously.
- Does not supply explicit convergence rates or moduli.
- Does not extend beyond proper metric spaces.
- Does not treat unbounded sequences.
Lean usage
exact D_converges f c R hf mformal statement (Lean)
139private theorem D_converges (m : ℕ) :
140 Tendsto (fun n => f (D f c R hf n) m) atTop (𝓝 (CL f c R hf m)) := by
proof body
Term-mode proof.
141 rw [Metric.tendsto_atTop]
142 intro ε hε
143 have h_base := CE_conv_at f c R hf m
144 rw [Metric.tendsto_atTop] at h_base
145 obtain ⟨K, hK⟩ := h_base ε hε
146 refine ⟨max m K, fun n hn => ?_⟩
147 have hm : m ≤ n := le_of_max_le_left hn
148 have hK_le : K ≤ n := le_of_max_le_right hn
149 obtain ⟨p, rfl⟩ := Nat.exists_eq_add_of_le hm
150 obtain ⟨ρ, _hρ_mono, hρ_ge, hρ_eq⟩ := CE_factor f c R hf m p
151 show dist (f (CE f c R hf (m + p) (m + p)) m) (CL f c R hf m) < ε
152 rw [hρ_eq (m + p)]
153 exact hK (ρ (m + p)) (le_trans hK_le (hρ_ge (m + p)))
154
155end Diagonal
156
157/-- **Cantor diagonal extraction** for ℕ-indexed bounded sequences
158in a proper metric space. Fully proved. -/