數列極限與精確尾界

數學敘述

實數列 u:N0→R 趨向 L，指對每個 ε>0，都存在自然數 N≥0，使所有 n≥N 有 |u(n)−L|<ε。本輪具體模型 u(n)=L+c/(n+d)，其中 d≥1，L、c為實數；整數參數切片的誤差是 |c|/(n+d)，不靠有限樣本猜收斂。

代表公式（精確 TeX）

u(n)

成立條件

• N0包含0，所有項分母n+d>0。題庫L、c、d為安全整數，ε=p/q且p、q>0，n及候選N為非負安全整數。
• 固定模型的全部尾項誤差不增，所以候選N的均勻尾界等價於 |c|q<p(N+d)。等號不符合嚴格誤差條件。
• 最小合法N為 max(0,floor(|c|q/p)−d+1)；c=0時N=0即可，L不影響誤差與尾界。

符號作用域

• u — 指定實數列
• n — 從0起算的自然索引

直觀、定義與常見誤解

尾界N可依ε改變，但選定後要管全部尾段，不是只檢查第N項或前幾項就能替任意數列證明。這個倒數模型另有單調誤差界，才可把均勻尾界化成一個精確不等式。

嚴格誤差會影響最小N：例如c=1、d=1、ε=1/2時，N=1的誤差等於容差，最小合法N是2。負c與正c的絕對誤差相同。

本輪核對的是已宣告倒數尾項模型的參數公式與資格，保留一般收斂證明及形式橋。改L不產生新誤差計算，改c、d不產生新極限L的題型。

把∀ε後的N固定死、只看有限項，或把誤差等於ε當作小於ε。

已採用的推導導讀

原始 MKO 保留；導讀有自己的追加式修訂與驗證界線，不代表新 Lean 證明。

前置知識

• 數列 — 先固定數列及索引慣例。
• 趨近關係 — 極限不是直接取到該值。
• 量詞與明示論域 — ∀ε、∃N、∀n≥N的順序。
• 有理數 — 精確正分母容差及誤差。

驗證界線

固定模型的精確參數與尾界可重算；一般實數列收斂未新增形式 Evidence。

not_formalized

這不表示內容錯誤；只表示尚未登錄可重播的計算或形式證據。

下一個義務

在固定版綁定 Tendsto atTop、實數鄰域、自然索引與倒數尾界的全尾段義務。

同源結構化資料

本頁與互動版共用同一個物件與既有語言 edition；未新增證明或人工審定。