Bernoulli參數尾端的CDF證書

目標與範圍

在極限CDF連續點證依分布收斂。

不要求共同coupling；不推出更強模式。

已知條件與符號

• work

• G1 — n≥1，X_n為Bernoulli(p_n)，p_n=1/3+1/(n+2)；X為Bernoulli(1/3)。只宣告laws，不宣告coupling。

• p_n — Bernoulli參數
• F_n,F — 各自CDF

規則與來源

• mko_definition · cited — 不要求共同機率空間或coupling。有限prefix不證收斂，極限CDF不連續點不要求收斂；依分布收斂不一般推出依機率、a.s.或Lp。 · mko-convergence-in-distribution
• work · prerequisite — Bernoulli CDF分段；依分布收斂只要求在極限CDF每個連續點收斂；floor(u)+1>u。

逐步主鏈

n\ge1

1/3<p_n\le2/3<1

t<0

F_n(t)=F(t)=0

0\le t<1

F_n(t)=1-p_n=2/3-1/(n+2),\quad F(t)=2/3

t\ge1

F_n(t)=F(t)=1

F\text{ is Bernoulli}(1/3)\text{ CDF}

\operatorname{Cont}(F)=\mathbb R\setminus\{0,1\}

0<t<1

|F_n(t)-F(t)|=1/(n+2)

\eta>0,\quad N=\lfloor1/\eta\rfloor+1

n\ge N\implies1/(n+2)<\eta

F_n(t)\to F(t)\quad(t\in\operatorname{Cont}(F))

X_n\Rightarrow X

局部子步與引理

本稿無局部子步。

逐步反向審查

• S08 · premise_audit · G1, S07, work — 沒有共同空間，故不把此結論寫成依機率收斂。
• S07 · premise_audit · G1, S06, work — eta任意且嚴格正，選N在取極限前。
• S06 · premise_audit · G1, S05, work — 區間內每個t同受這個界，不是固定幾點。
• S05 · premise_audit · G1, S04, work — 定義不要求在這兩個jump點收斂。
• S04 · premise_audit · G1, S03, work — t=1屬右段，雖是極限CDF的jump點。
• S03 · premise_audit · G1, S02, work — 不可把p_n誤作此區間CDF。
• S02 · premise_audit · G1, S01, work — 這是所有t<0的完整分支。
• S01 · premise_audit · G1, work — 最大值在n=1，不是以幾個樣本推估。

錯誤控制與反例

合法參數

對全部n≥1證p_n≤2/3。

模式邊界

law收斂不自行提供同空間差值。

• 此例已指定所有變數共用一個coin。 → reject — 資料僅指定laws，沒有coupling。
• 須先核jump點才符合定義。 → reject — 定義只要求極限CDF連續點。
• CDF有限多個n接近即可證收斂。 → reject — 本證明用任意eta的全稱尾端。

結論與限制

Bernoulli(1/3+1/(n+2))依分布收斂到Bernoulli(1/3)。

驗證及來源綁定

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

• source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
• adopted source SHA-256: 57b8fd580f0c495a9a33f194a0df094ac8136b1ac350e6e98cc85f9a09eff859
• original source SHA-256: 3f7025055c3497aa6b82b00d019258a96a7e7d544c185df0da1bf15436bbdbd0
• Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

同源完整 JSON（含公式、AST、反控制與修訂記錄）