bounded_subseq_tendsto
In a proper metric space every sequence bounded inside a closed ball admits a convergent subsequence along some strictly increasing index map. Navier-Stokes analysts working in Fourier space cite this to start the diagonal extraction for double sequences. The proof splits on the sign of the radius bound and invokes compactness of the closed ball to obtain the subsequence.
claimLet $X$ be a proper metric space. Let $f:ℕ→X$ and $c∈X$ satisfy dist$(f(n),c)≤R$ for every $n∈ℕ$. Then there exist a strictly increasing map $φ:ℕ→ℕ$ and a point $x∈X$ such that $f∘φ$ converges to $x$ as $n→∞$.
background
The FourierExtraction module constructs Cantor diagonal extraction for bounded sequences in proper metric spaces; every result is proved with no axioms or sorry. This theorem supplies the single-sequence subsequence tool that the composed extraction CE and the column limits CL are built from. It draws on compactness of closed balls together with order transitivity from ArithmeticFromLogic.
proof idea
The tactic proof cases on whether $R≥0$. The nonnegative branch applies tendsto_subseq to the compact closed ball, feeding the membership proof from the bound hypothesis. The negative branch obtains a contradiction by combining dist_nonneg with the bound at index zero via le_trans.
why it matters in Recognition Science
This extraction lemma is the base case for the entire diagonal construction in the module, directly supplying the choose and choose_spec data used by CE, CL, LE, CE_strictMono, CE_conv_at and the remaining convergence statements. It therefore underpins the main nat_diagonal_extraction result that produces the limit function g(m) for every column m. In the Recognition framework it supplies the subsequence guarantee needed when bounded sequences appear in the Fourier-space treatment of the Navier-Stokes equations derived from the forcing chain.
scope and limits
- Does not apply outside proper metric spaces.
- Does not produce an explicit convergence rate.
- Does not guarantee uniqueness of the limit point.
- Does not handle bounds that may grow with the index.
formal statement (Lean)
30theorem bounded_subseq_tendsto {X : Type*} [MetricSpace X] [ProperSpace X]
31 (f : ℕ → X) (c : X) (R : ℝ) (hf : ∀ n, dist (f n) c ≤ R) :
32 ∃ (φ : ℕ → ℕ) (x : X), StrictMono φ ∧ Tendsto (f ∘ φ) atTop (𝓝 x) := by
proof body
Tactic-mode proof.
33 by_cases hR : 0 ≤ R
34 · obtain ⟨x, _, φ, hφ, htend⟩ := (isCompact_closedBall c R).tendsto_subseq
35 (fun n => Metric.mem_closedBall.mpr (hf n))
36 exact ⟨φ, x, hφ, htend⟩
37 · exact absurd (le_trans dist_nonneg (hf 0)) (not_le.mpr (lt_of_not_le hR))
38
39section Diagonal
40
41variable {X : Type*} [MetricSpace X] [ProperSpace X]
42variable (f : ℕ → ℕ → X) (c : X) (R : ℝ) (hf : ∀ n m, dist (f n m) c ≤ R)
43
44/-- Composed extraction at step m: makes columns 0..m converge. -/