# 三點分布的完整CDF

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-cumulative-distribution-function/)

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

derivation-mko-cumulative-distribution-function-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

算出全實軸CDF、右連續值與跳躍。

完整有限離散分布；不把CDF當density。





## 已知條件與符號


- work


- G1 — X的support為{-1,1,3}，對應質量1/4、1/2、1/4。


- F — 累積分布函數
- t — 實數門檻





## 規則與來源


- mko_definition · cited — 完整有限實值分布下精確聚合所有x<=t的質量。CDF不是PMF或density；在support點的右值包含該點，jump為P(X=t)，端點極限為0與1。 · mko-cumulative-distribution-function
- work · prerequisite — 有限law的事件機率為所含質量和；CDF定義F(t)=P(X≤t)，jump為F(t)-F(t-)。





## 逐步主鏈

S01 · implies操作前

p=(-1:1/4,1:1/2,3:1/4)

操作後

1/4+1/2+1/4=1

條件：無

規則：work · 依賴：G1, work

葉節點依據：work

三個非負有理質量構成完整law。



S02 · implies操作前

F(t)=P(X\le t),\ t<-1

操作後

F(t)=0

條件：無

規則：work · 依賴：G1, S01, work

葉節點依據：work

門檻在最小support左側，累積事件為空。



S03 · implies操作前

-1\le t<1

操作後

\{X\le t\}=\{X=-1\},\ F(t)=1/4

條件：無

規則：work · 依賴：G1, S02, work

葉節點依據：work

這一整段只含-1的質量，包括左端。



S04 · implies操作前

1\le t<3

操作後

F(t)=1/4+1/2=3/4

條件：無

規則：work · 依賴：G1, S03, work

葉節點依據：work

跨過1時加入其完整1/2質量。



S05 · implies操作前

t\ge3

操作後

F(t)=1

條件：無

規則：work · 依賴：G1, S04, work

葉節點依據：work

最後一個區間含所有三點。



S06 · implies操作前

F(-1)-F(-1^-),F(1)-F(1^-),F(3)-F(3^-)

操作後

(1/4,1/2,1/4)

條件：無

規則：work · 依賴：G1, S05, work

葉節點依據：work

三個jump分別回復原PMF。



S07 · implies操作前

0\le1/4\le3/4\le1

操作後

F\text{ is nondecreasing and right-continuous}

條件：無

規則：work · 依賴：G1, S06, work

葉節點依據：work

常數區間與左閉右開的接合使每個support點右連續。



S08 · implies操作前

t<-1\text{ or }t\ge3

操作後

\lim_{t\to-\infty}F(t)=0,\quad\lim_{t\to\infty}F(t)=1

條件：無

規則：work · 依賴：G1, S07, work

葉節點依據：work

左右尾為恆0與恆1，端點極限因此完成。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, S07, work — 全實軸四段已覆蓋，非只測三個t值。
- S07 · premise_audit · G1, S06, work — 跳躍允許不連續；右連續不等於雙側連續。
- S06 · premise_audit · G1, S05, work — 左極限依前一段，不能以右值相減。
- S05 · premise_audit · G1, S04, work — t=3必須在此段而不是前段。
- S04 · premise_audit · G1, S03, work — CDF為3/4，不是單點P(X=1)=1/2。
- S03 · premise_audit · G1, S02, work — 不能在t=-1用左極限0代替函數值。
- S02 · premise_audit · G1, S01, work — t=-1不屬此區間，因定義包含等號。
- S01 · premise_audit · G1, work — support互異，沒有重複質量須合併。





## 錯誤控制與反例

端點四段使用左閉右開，最右段含3。

CDF與PMF用相鄰累積值之差還原點質量。


- F(1)=1/2。 → reject — 還須包含-1的1/4質量，故為3/4。
- F(-1)=0。 → reject — 事件使用≤，因此包含-1。
- 此CDF在1連續。 → reject — 左右差1/2，只有右連續。





## 結論與限制

CDF四段依序為0、1/4、3/4、1，三個jump正好是原質量。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 1df2921a8fc4b01d41e743dfcb4bed7628ea9a2b4e9edb112f1cbe3af187c073
- original source SHA-256: 48d250722a2d877fdc939dece0ff74b714aaa7b3d447e8ea86c8f60e1ca87802
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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