由逐點不等式得到Markov界

目標與範圍

證有限law的界並比較exact tail。

完整有限機率分布上的非負隨機變數；一般測度版本不由有限抽樣證明。

已知條件與符號

• work

• G1 — X取0、2、6，質量分別1/2、1/3、1/6；閾值a=3。

• a — 正閾值
• 1_A — 事件指示函數

規則與來源

• mko_definition · cited — 要求X>=0 almost surely、a>0及E[X]<infinity，結論P(X>=a)<=E[X]/a。完整有限有理law可精確算實際tail與bound；bound不等於tail，signed variable不可直接套用，零閾值禁止。 · mko-markov-inequality
• work · prerequisite — indicator期望等於事件機率；非負加權和保序；除以正數保序。

逐步主鏈

1/2+1/3+1/6=1

X\ge0,\quad a=3>0,\quad E[X]<\infty

x<3,\ x\in\{0,2,6\}

3\mathbf1_{\{x\ge3\}}=0\le x

x\ge3

3\mathbf1_{\{x\ge3\}}=3\le x

3\mathbf1_{\{X\ge3\}}\le X

3P(X\ge3)\le E[X]

E[X]=0/2+2/3+6/6

E[X]=5/3

3P(X\ge3)\le5/3

P(X\ge3)\le5/9

\{X\ge3\}=\{X=6\}

P(X\ge3)=1/6<5/9

a\mathbf1_{\{X\ge a\}}\le X,\quad a>0

P(X\ge a)\le E[X]/a

局部子步與引理

本稿無局部子步。

逐步反向審查

• S08 · premise_audit · G1, S07, work — 此一般化依逐點證明，不依本例數字看似成立。
• S07 · premise_audit · G1, S06, work — 不要把5/9回填為實際事件機率。
• S06 · premise_audit · G1, S05, work — 正閾值保證除法合法且不反向。
• S05 · premise_audit · G1, S04, work — 6的質量為1/6，不可當均勻三點。
• S04 · premise_audit · G1, S03, work — 使用全部support而非隨機抽幾個值。
• S03 · premise_audit · G1, S02, work — 兩分支合起來覆蓋全部support。
• S02 · premise_audit · G1, S01, work — signed x在此分支可能失敗，正是非負性用途。
• S01 · premise_audit · G1, work — 三項資格各自必要，不能只核mean為正。

錯誤控制與反例

非負性

先核每個正質量值非負，不能只看mean。

界非機率值

tail獨立由{6}求得1/6，再比較5/9。

• tail一定等於E[X]/a。 → reject — 此例1/6≠5/9。
• a=0仍可除。 → reject — 正閾值是分母資格。
• signed X只要mean正就能直接套。 → reject — 低閾值分支0≤X可能不成立。

結論與限制

本例tail=1/6，Markov界=5/9；有限law版本由逐點不等式證成。

驗證及來源綁定

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

• source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
• adopted source SHA-256: c8a078764616e58290cc4d16694339f57787010b9ba42b16d383b7a1a892a42c
• original source SHA-256: 1ef70a0328ec764a48d0df0ab90defc38d6cbe51d3d15f7ef7e50556ddc7cdc8
• Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

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