Finite filtration: checking information nesting by partition refinement, and separating it from adaptedness and independence

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

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\}\}

F_t=\sigma(P_t)

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

P'\preceq P

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

P_1\ \text{vs}\ P_0

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

P_2\ \text{vs}\ P_1

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

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}

A=\{0,1,2\}

A\in F_2,\ A\notin F_1

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)

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

X_1\ F_1\text{-measurable}

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

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

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)

\text{S06, S08, S10, S11}

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

Substeps and lemmas

P'\preceq P,\ B\in P

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

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

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

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 filtration

The 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 property

The 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 inclusion

MKO 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)