# 有限定義域的逐點尾項證書

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-pointwise-convergence-of-functions/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-pointwise-convergence-of-functions-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

證 f_n(p)=1+2/(n+1), f_n(q)=-2-3/(n+1) 逐點趨於 f。

共同有限域 {p,q}、R 值、n≥0；先以正有理容差建立精確尾項證書，再以 Archimedean 性銜接每個正實數 epsilon；不外推無限域。





## 已知條件與符號


- algebra
- epsilon
- definition_here


- G1 — D={p,q}, f(p)=1,f(q)=-2；所有 n≥0 都由上述完整公式定義 f_n。


- D — 共同有限域
- N_p,N_q — 逐點尾端索引





## 規則與來源


- mko_definition · cited — 本輪用完整有限domain及f_n(x)=f(x)+c_x/(n+s)的symbolic tail。逐x給exact epsilon witness；有限domain可取所有N的最大值推出該有限模型的一致收斂，但不可外推無限domain。有限prefix不足。 · mko-pointwise-convergence-of-functions
- algebra · prerequisite — 實數域的等式運算；除法前分母必非零，不等式乘正數保持方向。
- epsilon · prerequisite — 收斂表示每個正 epsilon 有一個整數 N，使全部 n≥N 的誤差嚴格小於 epsilon；使用實數 Archimedean 性。
- definition_here · prerequisite — 逐點收斂：每個 x、每個正 epsilon 皆有 N(x,epsilon)，使全部 n≥N 的該點誤差小於 epsilon。





## 逐步主鏈

S01 · implies操作前

n\ge0

操作後

n+1>0,\quad f_n:D\to\mathbb R

條件：無

規則：algebra · 依賴：G1

葉節點依據：algebra

分母不零，共同定義域與值域明確。



S02 · equivalent操作前

f_n(p)-f(p)=2/(n+1)

操作後

|f_n(p)-f(p)|=2/(n+1)

條件：無

規則：algebra · 依賴：G1, S01

葉節點依據：algebra

先固定 p，絕對值因分母正與分子正可直接去除。



S03 · implies操作前

\varepsilon>0,\quad N_p=\lfloor2/\varepsilon\rfloor+1

操作後

n\ge N_p\Longrightarrow n+1>2/\varepsilon

條件：\varepsilon\in\mathbb Q_{>0}

規則：epsilon · 依賴：S02

葉節點依據：epsilon

取嚴格大於 2/epsilon 的整數，全部尾端分母更大。



S04 · implies操作前

n+1>2/\varepsilon

操作後

|f_n(p)-f(p)|<\varepsilon\quad(n\ge N_p)

條件：無

規則：algebra · 依賴：S02, S03

葉節點依據：algebra

正數取倒數反向，得到嚴格 epsilon 界。



S05 · equivalent操作前

f_n(q)-f(q)=-3/(n+1)

操作後

|f_n(q)-f(q)|=3/(n+1)

條件：無

規則：algebra · 依賴：G1, S01

葉節點依據：algebra

固定另一點 q，負號在絕對值中消失。



S06 · implies操作前

N_q=\lfloor3/\varepsilon\rfloor+1

操作後

n\ge N_q\Longrightarrow |f_n(q)-f(q)|<\varepsilon

條件：\varepsilon>0

規則：epsilon · 依賴：S05

葉節點依據：epsilon

同一分母比較給 q 的全尾證書。



S07 · definition操作前

\forall x\in D\ \forall\varepsilon>0\ \exists N_x\ \forall n\ge N_x

操作後

f_n(x)\to f(x)\text{ pointwise on }D

條件：無

規則：definition_here · 依賴：G1, S04, S06

葉節點依據：definition_here

任給實數 epsilon>0，由已宣告的 Archimedean 性選正整數 k>1/epsilon，令 delta=1/k，則 0<delta<epsilon 且 delta 為有理數。把前述尾項證書的容差實例化為 delta，得到 N_p=2k+1、N_q=3k+1；取 N=3k+1。當 n≥N，兩點的誤差皆不超過 3/(n+1)<1/k<epsilon，故全部正實數容差的逐點量詞成立，並且這個兩點模型還有共同尾端。



S08 · implies操作前

N=\max(N_p,N_q)

操作後

n\ge N\Longrightarrow\forall x\in D\ |f_n(x)-f(x)|<\varepsilon

條件：無

規則：epsilon · 依賴：S03, S06

葉節點依據：epsilon

對任給正實數 epsilon，沿用 S07 的有理容差 delta=1/k；此處 N_p、N_q 是在 delta 處取得的索引，取其有限最大值 N=3k+1，便對全部 n≥N 與兩個 x 同時給出小於 epsilon 的誤差。這是有限域的額外推論，不外推到無限域。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · S03, S06 — 共同 N 是額外有限性推論，不是逐點定義自帶。
- S07 · premise_audit · G1, S04, S06 — 沒有交換 x 與 N 的量詞來定義逐點收斂。
- S06 · premise_audit · S05 — 逐點定義允許 N_q 與 N_p 不同。
- S05 · inverse_equivalence · G1, S01 — 不是把原函數的負值當負誤差。
- S04 · premise_audit · S02, S03 — 未把 ≤epsilon 誤作所需嚴格界。
- S03 · premise_audit · S02 — N_p 只依 p 與 epsilon，不依後來的 n。
- S02 · inverse_equivalence · G1, S01 — 符號核對依完整公式，不靠有限值表。
- S01 · premise_audit · G1 — 不是每個 n 換不同定義域。





## 錯誤控制與反例

嚴格 epsilon取 floor(C/epsilon)+1 保留嚴格不等式。

完整域兩點已窮盡，但不把兩點測試當無限域證明。


- 只核 n≤100 就證逐點收斂。 → reject — 尚有所有 n≥N 的責任。
- 負號使 q 的絕對誤差為負。 → reject — 誤差為 3/(n+1)>0。
- 任意無限域逐點收斂亦可取有限最大 N。 → reject — 無限多個逐點索引可能無共同上界。





## 結論與限制

兩點均逐點收斂，且此有限例另有共同 N=max(N_p,N_q)。







## 驗證及來源綁定

2 個本稿宣告算術檢查；只支持所列算式。


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: f6cce455f215e1c616bf5c32ac57230c794304a90156dbf919ff58b5b4258783
- original source SHA-256: a911769c2c8e25b8fc40746c08867b7ff998c9f34caf51de52c5f65f95c6a20a
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-pointwise-convergence-of-functions-01.json)