# 有限 filtration：以分割細化核對資訊嵌套，並區分 adapted 與獨立

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

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

derivation-mko-finite-filtration-01 · production-20261019-adopted-96



## 目標與範圍

在 Ω={0,1,2,3}（兩次擲幣：0=正正、1=正反、2=反正、3=反反）上，以分割編碼 P_0、P_1、P_2 表示時刻 0、1、2 的 σ 代數。證明「較晚分割細化較早分割 ⇔ σ 代數包含」，逐相鄰時刻完整核對，得出 (F_t) 是 filtration；給出不是 filtration 的分割序列；並證明 filtration 既不使每個過程 adapted，也不推出獨立。

只在 MKO 範圍內工作：所有分割使用同一樣本載體 0 到 3，每行的 label 只表示區塊等價（假設 a1）；細化逐相鄰時刻完整核對（假設 a2）。不宣稱 natural filtration、獨立或 Markov 性質；不處理 martingale；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- set_operations_def
- subset_def
- set_extensionality
- prob_axioms


- G1 — Ω={0,1,2,3}；結果的意義：0=正正、1=正反、2=反正、3=反反（只作說明，不影響分割的定義）。
- G2 — 分割編碼（依結果 0、1、2、3 給 label）：P_0=(a,a,a,a)、P_1=(a,a,b,b)、P_2=(a,b,c,d)；同一 label 表示同一區塊（MKO 假設 a1）。
- G3 — 定義：F_t=σ(P_t)；(F_t)_{t=0,1,2} 是 filtration，若 s≤t ⇒ F_s⊆F_t。P' 細化 P（記 P'⪯P），若 P' 的每個區塊都含於 P 的某個區塊。
- G4 — 對照序列：Q_0=(a,a,b,b)、Q_1=(a,b,a,b)。過程：X_1(ω)=1 若 ω∈{0,1}（第一次為正），否則 0；Y_1(ω)=1 若 ω∈{0,2}（第二次為正），否則 0。


- P_t — 時刻 t 的分割
- F_t=\sigma(P_t) — P_t 生成的 σ 代數（區塊的聯集）
- P'\preceq P — P' 細化 P：P' 的每個區塊含於 P 的某個區塊
- X_1,\ Y_1 — 第一次、第二次擲幣是否為正的指示函數
- Q_0,Q_1 — 不構成 filtration 的分割序列





## 規則與來源


- set_operations_def · prerequisite — 集合運算：x∈A∪B ⇔ x∈A 或 x∈B；x∈A∩B ⇔ x∈A 且 x∈B；x∈A∖B ⇔ x∈A 且 x∉B；在全集 U 中 Aᶜ=U∖A。
- subset_def · prerequisite — 子集：A⊆B 表示 A 的每個元素都是 B 的元素，即 ∀x (x∈A⇒x∈B)。
- set_extensionality · prerequisite — 集合相等：A=B 當且僅當 A⊆B 且 B⊆A，即兩者有相同元素。
- prob_axioms · prerequisite — 機率公理：P(A)≥0；P(Ω)=1；兩兩互斥事件的（可數）聯集機率等於各機率之和。由此 P(∅)=0、P(Aᶜ)=1−P(A)。
- set_builder · prerequisite — 集合建構式：x∈{y∈A ∣ P(y)} 當且僅當 x∈A 且 P(x)。
- def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
- logic_chain · prerequisite — 推論的傳遞：由 P⇒Q 與 Q⇒R 得 P⇒R；⇔ 同理。
- contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
- quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_filtration_def · cited — 以同一有限樣本空間上的 partition 表示各時刻 sigma 代數。F_s 包含於 F_t 等價於較晚 partition 細化較早 partition。filtration 只表資訊嵌套，不自動使過程 adapted，也不宣稱 natural filtration、獨立或 Markov 性。 · mko-finite-filtration
- sigma_partition · prerequisite — 有限集合 Ω 的分割 𝒫 生成的 σ 代數 σ(𝒫) 恰由區塊的聯集組成（含 ∅）；共有 2^{|𝒫|} 個事件。
- meas_const · prerequisite — Ω 上的實函數為 σ(𝒫) 可測，當且僅當它在 𝒫 的每個區塊上為常數。
- L_refine_iff · lemma — 對同一有限 Ω 的分割 P、P'：P'⪯P ⇔ σ(P)⊆σ(P')。





## 逐步主鏈

S01 · equivalent操作前

P_0=(a,a,a,a),\ P_1=(a,a,b,b),\ P_2=(a,b,c,d)

操作後

P_0=\{\Omega\},\ P_1=\{\{0,1\},\{2,3\}\},\ P_2=\{\{0\},\{1\},\{2\},\{3\}\}

條件：無

規則：set_builder · 依賴：G2, set_builder

葉節點依據：set_builder + def_unfold

ω 所在的區塊是 {ω'∈Ω ∣ ω' 與 ω 的 label 相同}。P_0 全部同 label，只有一個區塊 Ω；P_1 中 0、1 同為 a，2、3 同為 b；P_2 四個 label 互異，得四個單點。label 名稱本身沒有意義：把 P_1 寫成 (b,b,a,a) 是同一分割。



S02 · equivalent操作前

F_t=\sigma(P_t)

操作後

F_0=\{\varnothing,\Omega\},\ F_1=\{\varnothing,\{0,1\},\{2,3\},\Omega\},\ F_2=2^{\Omega}

條件：無

規則：sigma_partition · 依賴：S01, sigma_partition

葉節點依據：sigma_partition + set_operations_def + numeric_evaluation

σ 代數由區塊的聯集組成：F_0 有 2^1=2 個事件，F_1 有 2^2=4 個，F_2 有 2^4=16 個，即 Ω 的全部子集（N1 到 N3）。事件 A 在時刻 t 可測，當且僅當它是 P_t 區塊的聯集（MKO 段落 2）。



S03 · equivalent操作前

P'\preceq P

操作後

\sigma(P)\subseteq\sigma(P')

條件：P,P'\ \text{partitions of the same}\ \Omega

規則：L_refine_iff · 依賴：G3, sigma_partition

葉節點依據：sigma_partition + set_extensionality + subset_def

依引理 L_refine_iff（在 S03.1、S03.2 證明），細化與 σ 代數包含等價。這把有限事件族之間的包含核對，改寫成較精簡的區塊包含核對：本題 |Ω|=4，事件至多 2^4=16 個；有 b 個區塊的分割恰生成 2^b 個聯集事件，並非無限多種事件。



S04 · implies操作前

P_1\ \text{vs}\ P_0

操作後

\{0,1\}\subseteq\Omega,\ \{2,3\}\subseteq\Omega:\ P_1\preceq P_0

條件：無

規則：subset_def · 依賴：S01, G3

葉節點依據：subset_def + forall_intro

逐一核對 P_1 的全部 2 個區塊：{0,1} 與 {2,3} 都含於 P_0 的唯一區塊 Ω。核對是完整的，每個區塊都檢查了。



S05 · implies操作前

P_2\ \text{vs}\ P_1

操作後

\{0\},\{1\}\subseteq\{0,1\},\ \{2\},\{3\}\subseteq\{2,3\}:\ P_2\preceq P_1

條件：無

規則：subset_def · 依賴：S01, G3

葉節點依據：subset_def + forall_intro

逐一核對 P_2 的全部 4 個區塊：{0}、{1} 含於 {0,1}，{2}、{3} 含於 {2,3}。核對完整。



S06 · implies操作前

P_1\preceq P_0,\ P_2\preceq P_1

操作後

F_0\subseteq F_1\subseteq F_2,\ \text{so}\ (F_t)_{t=0,1,2}\ \text{is a filtration}

條件：無

規則：L_refine_iff · 依賴：S03, S04, S05

葉節點依據：subset_def + logic_chain + mko_filtration_def

依 L_refine_iff，S04 給 F_0⊆F_1，S05 給 F_1⊆F_2；包含關係可傳遞，所以 F_0⊆F_2。於是對所有 s≤t 都有 F_s⊆F_t（s=t 時自明），(F_t) 是 filtration。只需核相鄰時刻，正是因為包含可傳遞（MKO 假設 a2）。



S07 · implies操作前

A=\{0,1,2\}

操作後

A\in F_2,\ A\notin F_1

條件：無

規則：sigma_partition · 依賴：S02

葉節點依據：sigma_partition + contradiction

A 是 F_2 中單點的聯集，所以 A∈F_2。若 A 是 P_1 區塊的聯集，因 2∈A 而 2 所在區塊為 {2,3}，A 就必含 3，但 3∉A；所以 A∉F_1。資訊隨時間增加：時刻 2 可判定的事件，時刻 1 不一定可判定。



S08 · implies操作前

Q_0=\{\{0,1\},\{2,3\}\},\ Q_1=\{\{0,2\},\{1,3\}\}

操作後

Q_1\not\preceq Q_0,\ \text{so}\ \sigma(Q_0)\not\subseteq\sigma(Q_1)

條件：無

規則：L_refine_iff · 依賴：G4, S03, set_builder

葉節點依據：subset_def + quantifier_negation + sigma_partition

Q_1 的區塊 {0,2} 既不含於 {0,1}（2∉{0,1}），也不含於 {2,3}（0∉{2,3}），所以 Q_1 不細化 Q_0；依 L_refine_iff，σ(Q_0)⊄σ(Q_1)。具體見證：{0,1}∈σ(Q_0)，但它含 0 而不含 2，而 {0,2} 是 Q_1 的區塊，所以 {0,1} 不是 Q_1 區塊的聯集。這兩個時刻的資訊不嵌套：任意的分割序列不是 filtration。



S09 · implies操作前

X_1=(1,1,0,0)\ \text{on}\ (0,1,2,3)

操作後

X_1\ F_1\text{-measurable}

條件：無

規則：meas_const · 依賴：G4, S01, meas_const

葉節點依據：meas_const

X_1 在 {0,1} 上恆為 1、在 {2,3} 上恆為 0，即在 P_1 的每個區塊上為常數，所以 X_1 是 F_1 可測：第一次擲幣的結果在時刻 1 已知。



S10 · implies操作前

Y_1=(1,0,1,0)\ \text{on}\ (0,1,2,3)

操作後

Y_1\ \text{not}\ F_1\text{-measurable}

條件：無

規則：meas_const · 依賴：G4, S01, S06, meas_const

葉節點依據：meas_const + quantifier_negation

Y_1(0)=1、Y_1(1)=0，而 0、1 在 P_1 的同一區塊，所以 Y_1 在該區塊上不是常數，不是 F_1 可測。因此以 Y_1 作為時刻 1 值的過程不 adapted 於 (F_t)，即使 S06 已證明 (F_t) 是 filtration。Y_1 是 F_2 可測（任何函數在單點上都是常數）。



S11 · implies操作前

P(\{0\})=P(\{3\})=\tfrac12,\ P(\{1\})=P(\{2\})=0

操作後

P(X_1=1,\,Y_1=1)=\tfrac12\neq\tfrac14=P(X_1=1)P(Y_1=1)

條件：無

規則：prob_axioms · 依賴：S06, G4, prob_axioms

葉節點依據：prob_axioms + numeric_evaluation + quantifier_negation

(F_t) 的定義完全沒有用到機率。取一個合法的機率（總和 1/2+0+0+1/2=1，N5）：P(X_1=1)=P({0,1})=1/2，P(Y_1=1)=P({0,2})=1/2，但 P(X_1=1,Y_1=1)=P({0})=1/2≠1/4（N4）。兩次擲幣不獨立，而 filtration 不變。所以 filtration 不推出獨立；同理也不推出 Markov 性。



S12 · implies操作前

\text{S06, S08, S10, S11}

操作後

(F_t)\ \text{filtration};\ (\sigma(Q_t))\ \text{not};\ \text{adaptedness and independence not implied}

條件：無

規則：mko_filtration_def · 依賴：S06, S08, S10, S11

葉節點依據：and_intro_elim

完整的相鄰細化核對證明 (F_t) 是 filtration；Q 序列因一個區塊不細化而不是；filtration 只表資訊嵌套，以 Y_1 為時刻 1 值的過程不 adapted，擲幣也可以不獨立。







## 局部子步與引理

S03.1 · implies操作前

P'\preceq P,\ B\in P

操作後

B=\bigcup\{C\in P'\mid C\cap B\neq\varnothing\},\ \text{hence}\ \sigma(P)\subseteq\sigma(P')

條件：無

規則：set_extensionality · 依賴：G3, sigma_partition, set_operations_def

葉節點依據：set_extensionality + set_operations_def + sigma_partition

（⇒）取 B∈P。⊆：每個 ω∈B 屬於 P' 的某個區塊 C，且 C∩B 含 ω。⊇：若 C∩B≠∅，由細化 C⊆B' 對某個 B'∈P；則 B'∩B⊇C∩B≠∅，而 P 的區塊相等或互斥，所以 B'=B，C⊆B。因此每個 P 區塊是 P' 區塊的聯集；P 區塊的聯集也就是 P' 區塊的聯集，σ(P)⊆σ(P')。



S03.2 · implies操作前

\sigma(P)\subseteq\sigma(P'),\ C\in P',\ \omega\in C

操作後

C\subseteq B\ \text{for the block}\ B\in P\ \text{containing}\ \omega

條件：無

規則：subset_def · 依賴：G3, sigma_partition

葉節點依據：subset_def + sigma_partition + set_operations_def

（⇐）設 B 是含 ω 的 P 區塊。B∈σ(P)⊆σ(P')，所以 B 是若干 P' 區塊的聯集；ω∈B 落在其中某個 P' 區塊，而 ω 只屬於 P' 的區塊 C，所以 C 是其中之一，C⊆B。每個 C 都如此，所以 P'⪯P。S03.1 與 S03.2 合起來證得引理 L_refine_iff。







## 逐步反向審查


- S12 · sufficient_goal_reduction · S06, S08, S10, S11 — 目標 G：本稿目標的四個結論。足夠條件 H：S06、S08、S10、S11；H⇒G 由合取。H 由 G1 到 G4 正向證成，沒有把 G 當作前提。
- S11 · premise_audit · S06, prob_axioms — 一個反例就足以否定「filtration 推出獨立」；不宣稱在其他機率下也不獨立。
- S10 · premise_audit · meas_const, S06 — adapted 是過程與 filtration 之間的另一個條件，必須另核（MKO 段落 2）；filtration 的存在不提供它。
- S09 · premise_audit · meas_const, S01 — 要逐區塊核對常數，這裡 2 個區塊都通過。
- S08 · premise_audit · G4, L_refine_iff — 一個不通過的區塊就足以否定細化；見證事件獨立地確認包含失敗。
- S07 · premise_audit · S02, sigma_partition — 只需找到一個被切開的區塊 {2,3}；不宣稱反向。
- S06 · premise_audit · S03, S04, S05, subset_def — 需要每一對相鄰時刻都通過；不宣稱這個 filtration 是某個過程的 natural filtration。
- S05 · premise_audit · S01, subset_def — 4 個區塊全部通過；任一失敗就不是細化。
- S04 · premise_audit · S01, subset_def — 細化要求 P_1 的每個區塊都通過；這裡 2 個都通過。
- S03.2 · premise_audit · G3, sigma_partition, subset_def — 關鍵是 P' 的區塊互斥，使 ω 所在的 P' 區塊唯一。
- S03.1 · premise_audit · G3, set_extensionality, sigma_partition — 用到 P' 覆蓋 Ω 與 P 的區塊互斥；只證一個方向。
- S03 · inverse_equivalence · L_refine_iff — 兩個方向分別在 S03.1、S03.2 證明；兩個分割必須在同一 Ω 上。
- S02 · inverse_equivalence · sigma_partition — 列出的集合正是區塊的全部聯集；雙向成立。
- S01 · inverse_equivalence · set_builder, G2 — 由區塊可重建一行 label（每區塊給一個新 label），且只差 label 改名；兩種表示決定同一分割。





## 錯誤控制與反例

任意分割序列不一定是 filtrationMKO 指出的誤解：把任意 partition 序列叫 filtration。Q_0、Q_1 都是同一 Ω 上的分割，但 Q_1 不細化 Q_0，{0,1} 在時刻 0 可判定、在時刻 1 卻不可判定（S08）。必須逐相鄰時刻完整核對每個區塊。

filtration 不推出 adapted、獨立或 MarkovMKO 的第二個誤解。S06 證明 (F_t) 是 filtration，但 Y_1 不是 F_1 可測（S10），且在 P({0})=P({3})=1/2 下擲幣不獨立（S11）。adapted 要逐過程另核；獨立與 Markov 依賴機率，filtration 的定義不含機率。

抽查事件不能證明包含MKO 假設 a2：有限抽樣事件不足以證 σ 代數包含。對 Q 序列，事件 ∅ 與 Ω 都同時在 σ(Q_0) 與 σ(Q_1) 中，只抽這兩個會誤判包含成立；完整的區塊細化核對（S03 的引理）才是證書。


- σ(Q_0)、σ(Q_1) 都是同一 Ω 上的 σ 代數，所以 (σ(Q_0),σ(Q_1)) 是 filtration → reject — {0,1}∈σ(Q_0) 但不在 σ(Q_1)（S08）。
- (F_t) 是 filtration，所以第二次擲幣 Y_1 是 F_1 可測 → reject — Y_1 在區塊 {0,1} 上取 1 與 0（S10）。
- (F_t) 是 filtration，所以兩次擲幣獨立 → reject — P({0})=P({3})=1/2 時 P(兩次皆正)=1/2≠1/4（S11）。
- ∅、Ω 都屬於 σ(Q_1)，所以 σ(Q_0)⊆σ(Q_1) → reject — 包含要對 σ(Q_0) 的每個事件成立；{0,1} 失敗。
- 把 P_1 改寫成 (b,b,a,a) 就得到不同的分割與不同的 F_1 → reject — label 只表示區塊等價；區塊仍是 {0,1}、{2,3}（S01）。





## 結論與限制

對同一有限 Ω 的分割，較晚分割細化較早分割當且僅當 σ 代數包含。P_1 的 2 個區塊含於 Ω，P_2 的 4 個單點含於 P_1 的區塊，所以 F_0⊆F_1⊆F_2，(F_t) 是 filtration；Q_1 的區塊 {0,2} 不含於任何 Q_0 區塊，{0,1}∈σ(Q_0)∖σ(Q_1)，不是 filtration。第一次擲幣 X_1 是 F_1 可測，第二次擲幣 Y_1 不是；在 P({0})=P({3})=1/2 下兩次擲幣不獨立。filtration 只表示資訊嵌套。


- 本稿不宣稱 (F_t) 是某個過程的 natural filtration，也不處理 martingale（MKO 的下一步，需與條件期望一起加入）。





## 驗證及來源綁定

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


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: e6820be99eb83c1217b02247f1bc0e38f7ba1bd24ea85ba09fd8e6937818f6c0
- original source SHA-256: ab8a8b045d8752cb59b7afd124424df8d7210731678c8341756298606f15afcf
- Lean: NOT_RUN · independent AI: NOT_MEASURED

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