有平坦段的連續CDF

目標與範圍

從knots完整構造CDF並核atomless性。

piecewise-linear exact family；不由連續性推一般density存在。

已知條件與符號

• work

• G1 — knots為(0,0)、(1,1/2)、(2,1/2)、(3,1)；相鄰間線性插值，左側0、右側1。

• F — 實數CDF
• t — 任意實數門檻

規則與來源

本稿部分規則文字經本輪讀者釐清，屬於改述而非逐字引文；被引用的原始來源內容及雜湊沒有改動。

• mko_definition · cited — continuous CDF沒有jumps，所以每個singleton probability為0。這不等於sample-space上的random-variable map連續，也不推出density或absolute continuity；affine Cantor distribution提供continuous atomless singular boundary。CDF可有flat intervals，不必strictly increasing。 · mko-continuous-real-distribution-function
• work · prerequisite — 分段線性函數在每段連續；接點左右值一致使全域連續；CDF存在定理與jump identity為前提。

逐步主鏈

0<1<2<3,\quad0\le1/2\le1/2\le1

\text{strict knot order and nondecreasing levels}

t\le0\text{ or }t\ge3

F(t)=0\ (t\le0),\quad F(t)=1\ (t\ge3)

0\le t\le1

F(t)=t/2

1\le t\le2

F(t)=1/2

2\le t\le3

F(t)=1/2+(t-2)/2=(t-1)/2

t\in\{0,1,2,3\}

F(t^-)=F(t)=F(t^+)

F\text{ nondecreasing and continuous, with tails }0,1

\exists X:\ F(t)=P(X\le t);\quad P(X=t)=F(t)-F(t^-)=0\quad(t\in\mathbb R)

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

F\text{ is a continuous CDF, not strictly increasing}

局部子步與引理

本稿無局部子步。

逐步反向審查

• S08 · premise_audit · G1, S07, work — 一般continuous CDF可能singular，如Cantor law；不能由本例外推density。
• S07 · premise_audit · G1, S06, work — 先取得law才談P(X=t)；無原子不等於區間機率零，例如P(0<X≤1)=1/2。
• S06 · premise_audit · G1, S05, work — 逐接點核對才證全域連續，不是只取樣。
• S05 · premise_audit · G1, S04, work — t=2要給1/2，不能用t/2接錯。
• S04 · premise_audit · G1, S03, work — CDF不必嚴格遞增。
• S03 · premise_audit · G1, S02, work — t=0、1代回得到正確兩knots。
• S02 · premise_audit · G1, S01, work — 端點0與3將和內插值一致。
• S01 · premise_audit · G1, work — 相同level允許，只有x座標必須嚴格遞增。

錯誤控制與反例

接點

逐核0、1、2、3的左值與右值。

查詢排序

例如1/2、3/2、5/2嚴格遞增，值為1/4、1/2、3/4。

• 所有continuous CDF都strictly increasing。 → reject — 此例[1,2]恆為1/2。
• continuous CDF必有density。 → reject — Cantor型singular law是邊界反例。
• P(X=1)=F(1)=1/2。 → reject — singleton mass為jump，此處為零。

結論與限制

這是一個有[1,2]平坦段的連續無原子CDF。

驗證及來源綁定

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

• source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
• adopted source SHA-256: 79d7922fc70bd68789e0c257bdf10bf05aae23f17410f0343d79c5d7cb7756de
• original source SHA-256: 5f3d06982951d8148e60031cd501f7fc189242eca7f7a442857ec8ad6f770380
• Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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