# Finite filtration: checking information nesting by partition refinement, and separating it from adaptedness and independence [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-finite-filtration/) This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented. derivation-mko-finite-filtration-01 · production-20261019-adopted-96 ## Goal and scope On Ω={0,1,2,3} (two coin tosses: 0=HH, 1=HT, 2=TH, 3=TT), represent the σ-algebras at times 0, 1, 2 by partition rows P_0, P_1, P_2. Prove that 'the later partition refines the earlier one ⇔ the σ-algebras are nested', check every adjacent pair of times completely and conclude that (F_t) is a filtration; give a sequence of partitions that is not a filtration; and show that a filtration neither makes every process adapted nor implies independence. Works inside the MKO's scope: every partition uses the same outcomes 0 to 3, and labels within a row indicate only block equivalence (assumption a1); refinement is checked completely at every pair of adjacent times (assumption a2). No natural-filtration, independence or Markov claim is made; martingales are not treated; the canonical MKO and its English edition are not changed. ## Givens and symbols - set_operations_def - subset_def - set_extensionality - prob_axioms - G1 — Ω={0,1,2,3}; meaning of the outcomes: 0=HH, 1=HT, 2=TH, 3=TT (for orientation only; it does not affect the partitions). - G2 — Partition rows (labels for outcomes 0, 1, 2, 3): P_0=(a,a,a,a), P_1=(a,a,b,b), P_2=(a,b,c,d); equal labels mean the same block (MKO assumption a1). - G3 — Definitions: F_t=σ(P_t); (F_t)_{t=0,1,2} is a filtration if s≤t ⇒ F_s⊆F_t. P' refines P (written P'⪯P) if every block of P' is contained in some block of P. - G4 — Contrast sequence: Q_0=(a,a,b,b), Q_1=(a,b,a,b). Processes: X_1(ω)=1 if ω∈{0,1} (first toss heads), else 0; Y_1(ω)=1 if ω∈{0,2} (second toss heads), else 0. - P_t — the partition at time t - F_t=\sigma(P_t) — the σ-algebra generated by P_t (unions of blocks) - P'\preceq P — P' refines P: each block of P' lies inside some block of P - X_1,\ Y_1 — indicators that the first, respectively second, toss is heads - Q_0,Q_1 — a sequence of partitions that is not a filtration ## Rules and sources - set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A. - subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B). - set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements. - prob_axioms · prerequisite — Probability axioms: P(A)≥0; P(Ω)=1; the probability of a (countable) union of pairwise disjoint events is the sum of their probabilities. Hence P(∅)=0 and P(Aᶜ)=1−P(A). - set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x). - def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true. - numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable. - forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain. - logic_chain · prerequisite — Chaining: from P⇒Q and Q⇒R infer P⇒R; likewise for ⇔. - contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds. - quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x). - and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q. - mko_filtration_def · cited — Represent each time's sigma-algebra by a partition of the same finite sample space. F_s being contained in F_t means the later partition refines the earlier one. A filtration specifies information nesting only: a process is not automatically adapted, and no natural-filtration, independence or Markov claim follows. · mko-finite-filtration - sigma_partition · prerequisite — The σ-algebra σ(𝒫) generated by a partition 𝒫 of a finite set Ω consists exactly of the unions of blocks (including ∅); it has 2^{|𝒫|} events. - meas_const · prerequisite — A real function on Ω is σ(𝒫)-measurable exactly when it is constant on each block of 𝒫. - L_refine_iff · lemma — For partitions P and P' of the same finite Ω: P'⪯P ⇔ σ(P)⊆σ(P'). ## Main derivation S01 · equivalentBefore P_0=(a,a,a,a),\ P_1=(a,a,b,b),\ P_2=(a,b,c,d) After P_0=\{\Omega\},\ P_1=\{\{0,1\},\{2,3\}\},\ P_2=\{\{0\},\{1\},\{2\},\{3\}\} Conditions: none Rule: set_builder · Uses: G2, set_builder Leaf basis: set_builder + def_unfold The block of ω is {ω'∈Ω ∣ ω' has the same label as ω}. In P_0 all labels agree, giving the single block Ω; in P_1, 0 and 1 share a and 2 and 3 share b; in P_2 the four labels differ, giving four singletons. The label names carry no meaning: writing P_1 as (b,b,a,a) gives the same partition. S02 · equivalentBefore F_t=\sigma(P_t) After F_0=\{\varnothing,\Omega\},\ F_1=\{\varnothing,\{0,1\},\{2,3\},\Omega\},\ F_2=2^{\Omega} Conditions: none Rule: sigma_partition · Uses: S01, sigma_partition Leaf basis: sigma_partition + set_operations_def + numeric_evaluation A σ-algebra consists of the unions of blocks: F_0 has 2^1=2 events, F_1 has 2^2=4, and F_2 has 2^4=16, all subsets of Ω (N1 to N3). An event A is measurable at time t exactly when it is a union of blocks of P_t (MKO paragraph 2). S03 · equivalentBefore P'\preceq P After \sigma(P)\subseteq\sigma(P') Conditions: P,P'\ \text{partitions of the same}\ \Omega Rule: L_refine_iff · Uses: G3, sigma_partition Leaf basis: sigma_partition + set_extensionality + subset_def By Lemma L_refine_iff (proved in S03.1 and S03.2), refinement is equivalent to inclusion of σ-algebras. This recasts inclusion between finite event families as a more compact complete check of block inclusions. Here |Ω|=4, so there are at most 2^4=16 events; a partition with b blocks generates exactly 2^b union events, not infinitely many events. S04 · impliesBefore P_1\ \text{vs}\ P_0 After \{0,1\}\subseteq\Omega,\ \{2,3\}\subseteq\Omega:\ P_1\preceq P_0 Conditions: none Rule: subset_def · Uses: S01, G3 Leaf basis: subset_def + forall_intro Check both blocks of P_1: {0,1} and {2,3} each lie inside Ω, the only block of P_0. The check is complete; every block was examined. S05 · impliesBefore P_2\ \text{vs}\ P_1 After \{0\},\{1\}\subseteq\{0,1\},\ \{2\},\{3\}\subseteq\{2,3\}:\ P_2\preceq P_1 Conditions: none Rule: subset_def · Uses: S01, G3 Leaf basis: subset_def + forall_intro Check all 4 blocks of P_2: {0} and {1} lie in {0,1}, and {2} and {3} lie in {2,3}. The check is complete. S06 · impliesBefore P_1\preceq P_0,\ P_2\preceq P_1 After F_0\subseteq F_1\subseteq F_2,\ \text{so}\ (F_t)_{t=0,1,2}\ \text{is a filtration} Conditions: none Rule: L_refine_iff · Uses: S03, S04, S05 Leaf basis: subset_def + logic_chain + mko_filtration_def By L_refine_iff, S04 gives F_0⊆F_1 and S05 gives F_1⊆F_2; inclusion is transitive, so F_0⊆F_2. Hence F_s⊆F_t for all s≤t (trivially when s=t), and (F_t) is a filtration. Checking adjacent times suffices precisely because inclusion is transitive (MKO assumption a2). S07 · impliesBefore A=\{0,1,2\} After A\in F_2,\ A\notin F_1 Conditions: none Rule: sigma_partition · Uses: S02 Leaf basis: sigma_partition + contradiction A is a union of singletons, so A∈F_2. If A were a union of P_1-blocks, then since 2∈A and the block of 2 is {2,3}, A would contain 3; but 3∉A, so A∉F_1. Information grows with time: an event decidable at time 2 need not be decidable at time 1. S08 · impliesBefore Q_0=\{\{0,1\},\{2,3\}\},\ Q_1=\{\{0,2\},\{1,3\}\} After Q_1\not\preceq Q_0,\ \text{so}\ \sigma(Q_0)\not\subseteq\sigma(Q_1) Conditions: none Rule: L_refine_iff · Uses: G4, S03, set_builder Leaf basis: subset_def + quantifier_negation + sigma_partition The Q_1-block {0,2} lies neither in {0,1} (2∉{0,1}) nor in {2,3} (0∉{2,3}), so Q_1 does not refine Q_0; by L_refine_iff, σ(Q_0)⊄σ(Q_1). A concrete witness: {0,1}∈σ(Q_0), but it contains 0 and not 2, while {0,2} is a Q_1-block, so {0,1} is not a union of Q_1-blocks. The information at the two times is not nested: an arbitrary sequence of partitions is not a filtration. S09 · impliesBefore X_1=(1,1,0,0)\ \text{on}\ (0,1,2,3) After X_1\ F_1\text{-measurable} Conditions: none Rule: meas_const · Uses: G4, S01, meas_const Leaf basis: meas_const X_1 equals 1 throughout {0,1} and 0 throughout {2,3}, i.e. it is constant on every block of P_1, so X_1 is F_1-measurable: the first toss is known at time 1. S10 · impliesBefore Y_1=(1,0,1,0)\ \text{on}\ (0,1,2,3) After Y_1\ \text{not}\ F_1\text{-measurable} Conditions: none Rule: meas_const · Uses: G4, S01, S06, meas_const Leaf basis: meas_const + quantifier_negation Y_1(0)=1 and Y_1(1)=0, while 0 and 1 lie in the same block of P_1, so Y_1 is not constant there and is not F_1-measurable. Hence a process whose time-1 value is Y_1 is not adapted to (F_t), even though S06 proved that (F_t) is a filtration. Y_1 is F_2-measurable (every function is constant on singletons). S11 · impliesBefore P(\{0\})=P(\{3\})=\tfrac12,\ P(\{1\})=P(\{2\})=0 After P(X_1=1,\,Y_1=1)=\tfrac12\neq\tfrac14=P(X_1=1)P(Y_1=1) Conditions: none Rule: prob_axioms · Uses: S06, G4, prob_axioms Leaf basis: prob_axioms + numeric_evaluation + quantifier_negation The definition of (F_t) uses no probability at all. Take a valid probability (total 1/2+0+0+1/2=1, N5): P(X_1=1)=P({0,1})=1/2 and P(Y_1=1)=P({0,2})=1/2, but P(X_1=1,Y_1=1)=P({0})=1/2≠1/4 (N4). The two tosses are not independent, while the filtration is unchanged. So a filtration does not imply independence; likewise it implies no Markov property. S12 · impliesBefore \text{S06, S08, S10, S11} After (F_t)\ \text{filtration};\ (\sigma(Q_t))\ \text{not};\ \text{adaptedness and independence not implied} Conditions: none Rule: mko_filtration_def · Uses: S06, S08, S10, S11 Leaf basis: and_intro_elim The complete adjacent refinement check proves that (F_t) is a filtration; the sequence Q is not, because one block fails to refine; a filtration expresses information nesting only, a process with Y_1 as its time-1 value is not adapted, and the tosses need not be independent. ## Substeps and lemmas S03.1 · impliesBefore P'\preceq P,\ B\in P After B=\bigcup\{C\in P'\mid C\cap B\neq\varnothing\},\ \text{hence}\ \sigma(P)\subseteq\sigma(P') Conditions: none Rule: set_extensionality · Uses: G3, sigma_partition, set_operations_def Leaf basis: set_extensionality + set_operations_def + sigma_partition (⇒) Take B∈P. ⊆: each ω∈B lies in some block C of P', and C∩B contains ω. ⊇: if C∩B≠∅, refinement gives C⊆B' for some B'∈P; then B'∩B⊇C∩B≠∅, and blocks of P are equal or disjoint, so B'=B and C⊆B. Hence each block of P is a union of blocks of P'; unions of P-blocks are then unions of P'-blocks, so σ(P)⊆σ(P'). S03.2 · impliesBefore \sigma(P)\subseteq\sigma(P'),\ C\in P',\ \omega\in C After C\subseteq B\ \text{for the block}\ B\in P\ \text{containing}\ \omega Conditions: none Rule: subset_def · Uses: G3, sigma_partition Leaf basis: subset_def + sigma_partition + set_operations_def (⇐) Let B be the block of P containing ω. B∈σ(P)⊆σ(P'), so B is a union of blocks of P'; ω∈B lies in one of them, and ω belongs only to the P'-block C, so C is one of them and C⊆B. This holds for every C, so P'⪯P. S03.1 and S03.2 together prove Lemma L_refine_iff. ## Reverse audits - S12 · sufficient_goal_reduction · S06, S08, S10, S11 — Goal G: the four conclusions stated in the goal. Sufficient condition H: S06, S08, S10 and S11; H⇒G by conjunction. H is proved forwards from G1 to G4; G is never used as a premise. - S11 · premise_audit · S06, prob_axioms — One counterexample suffices to refute 'a filtration implies independence'; it is not claimed that independence fails under every probability. - S10 · premise_audit · meas_const, S06 — Adaptedness is a separate condition linking a process to a filtration and must be checked on its own (MKO paragraph 2); the existence of a filtration does not supply it. - S09 · premise_audit · meas_const, S01 — Constancy must be checked block by block; here both blocks pass. - S08 · premise_audit · G4, L_refine_iff — One failing block suffices to refute refinement; the witness event independently confirms that inclusion fails. - S07 · premise_audit · S02, sigma_partition — One split block, {2,3}, suffices; no converse is claimed. - S06 · premise_audit · S03, S04, S05, subset_def — Every adjacent pair of times must pass; it is not claimed that this filtration is the natural filtration of any process. - S05 · premise_audit · S01, subset_def — All 4 blocks pass; a single failure would rule out refinement. - S04 · premise_audit · S01, subset_def — Refinement requires every block of P_1 to pass; here both do. - S03.2 · premise_audit · G3, sigma_partition, subset_def — The key is that the blocks of P' are disjoint, so the P'-block containing ω is unique. - S03.1 · premise_audit · G3, set_extensionality, sigma_partition — It uses that P' covers Ω and that the blocks of P are disjoint; only one direction is proved here. - S03 · inverse_equivalence · L_refine_iff — The two directions are proved in S03.1 and S03.2; both partitions must be on the same Ω. - S02 · inverse_equivalence · sigma_partition — The listed sets are exactly all unions of blocks; the step holds both ways. - S01 · inverse_equivalence · set_builder, G2 — From the blocks a label row can be rebuilt (one new label per block), unique up to renaming labels; both descriptions determine the same partition. ## Error controls and negative controls An arbitrary partition sequence need not be a filtrationThe MKO's misconception: calling any sequence of partitions a filtration. Q_0 and Q_1 are both partitions of the same Ω, but Q_1 does not refine Q_0, and {0,1} is decidable at time 0 but not at time 1 (S08). Every block must be checked at every adjacent pair of times. A filtration implies no adaptedness, independence or Markov propertyThe MKO's second misconception. S06 proves that (F_t) is a filtration, yet Y_1 is not F_1-measurable (S10), and under P({0})=P({3})=1/2 the tosses are not independent (S11). Adaptedness must be checked separately for each process; independence and Markov properties depend on the probability, which the definition of a filtration does not involve. Sampled events do not prove inclusionMKO assumption a2: finitely sampled events do not establish inclusion of σ-algebras. For the sequence Q, the events ∅ and Ω lie in both σ(Q_0) and σ(Q_1); sampling only these would wrongly suggest inclusion. The complete block-refinement check (the lemma of S03) is the certificate. - σ(Q_0) and σ(Q_1) are σ-algebras on the same Ω, so (σ(Q_0),σ(Q_1)) is a filtration → reject — {0,1}∈σ(Q_0) but it is not in σ(Q_1) (S08). - (F_t) is a filtration, so the second toss Y_1 is F_1-measurable → reject — Y_1 takes the values 1 and 0 on the block {0,1} (S10). - (F_t) is a filtration, so the two tosses are independent → reject — With P({0})=P({3})=1/2, P(both heads)=1/2≠1/4 (S11). - ∅ and Ω both belong to σ(Q_1), so σ(Q_0)⊆σ(Q_1) → reject — Inclusion must hold for every event of σ(Q_0); {0,1} fails. - Rewriting P_1 as (b,b,a,a) gives a different partition and a different F_1 → reject — Labels only indicate block equivalence; the blocks are still {0,1} and {2,3} (S01). ## Result and limitations For partitions of the same finite Ω, the later partition refines the earlier one exactly when the σ-algebras are nested. The 2 blocks of P_1 lie in Ω and the 4 singletons of P_2 lie in blocks of P_1, so F_0⊆F_1⊆F_2 and (F_t) is a filtration; the Q_1-block {0,2} lies in no Q_0-block, {0,1}∈σ(Q_0)∖σ(Q_1), and Q is not a filtration. The first toss X_1 is F_1-measurable, the second toss Y_1 is not; under P({0})=P({3})=1/2 the two tosses are not independent. A filtration expresses information nesting only. - This guide does not claim that (F_t) is the natural filtration of any process, and it does not treat martingales (the MKO's next step, to be added together with conditional expectation). ## Verification and source binding 5 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: e6820be99eb83c1217b02247f1bc0e38f7ba1bd24ea85ba09fd8e6937818f6c0 - original source SHA-256: ab8a8b045d8752cb59b7afd124424df8d7210731678c8341756298606f15afcf - Lean: NOT_RUN · independent AI: NOT_MEASURED [Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-finite-filtration-01.json)