A recurrent Markov exchangeable process whose successor array is not row exchangeable

The Diaconis–Freedman representation of a Markov exchangeable process passes through its successor array TauCeti.Probability.successorProcess, whose (a, k)-entry is the state reached right after the k-th visit to a. The change of variables back from a row exchangeable array to a mixture of Markov chains is TauCeti.Probability.mixedMarkovChain_of_rowExchangeable, and one array it accepts is that successor array. This file shows that recurrence and Markov exchangeability do not make the successor array row exchangeable, and exhibits an obstruction to it; that is why the Diaconis–Freedman representation TauCeti.Probability.MarkovExchangeable.mixedMarkovChain passes through the visited successor array TauCeti.Probability.visitedSuccessorProcess instead, whose unvisited rows are constant.

The obstruction is not the reordering of genuine transitions but the junk rows. A state the process never visits has no genuine successors, so every one of its visit times is Nat.nth's junk index 0; the whole row is therefore read off at time zero, every entry being x 1, and by TauCeti.successorArray_eq_successorArray_zero_of_forall_ne it is constant and equal to the cell (x 0, 0). Every successor array therefore satisfies the tie

successorArray x a k = successorArray x (x 0) 0    (a never visited)

whereas a permutation of the row x 0 moves the right-hand side while leaving the left-hand side where it is. TauCeti.Probability.Recurrent constrains only the states a process does visit, so it does not exclude this.

To turn that into a counterexample take the three-letter alphabet Fin 3 and let spareStateProcess be the sequence of coordinates of a fair coin sequence in the two letters 0 and 1; the letter 2 is spare and is almost surely never taken. Being i.i.d. the process is exchangeable (spareStateProcess_exchangeable), hence Markov exchangeable (spareStateProcess_markovExchangeable) and recurrent (spareStateProcess_recurrent). Yet swapping the first two entries of the row of the letter 0 — a permutation family of finite support — changes the law of its successor array (spareStateProcess_not_rowExchangeable_successorProcess), because the swap breaks the tie above on the event that the path begins 0, 0, 1, 1 and never takes the spare letter. That event has probability 16⁻¹, the probability of the opening alone, because avoiding the spare letter is almost sure.

Only one of the two cells the tie involves is one the consumer of the array reads: TauCeti.eqOn_iff_successorArray_visitCell describes a finite path event through the cells a reference path designates, and those lie in visited rows, so the spare row's cell (2, 0) is never among them, while the cell (x 0, 0) it is tied to is a genuine successor cell.

Main results

• TauCeti.Probability.spareStateProcess_exchangeable, TauCeti.Probability.spareStateProcess_markovExchangeable and TauCeti.Probability.spareStateProcess_recurrent — the example satisfies the Diaconis–Freedman hypotheses.
• TauCeti.Probability.spareStateProcess_not_rowExchangeable_successorProcess — its successor array is nevertheless not row exchangeable.

References

• P. Diaconis and D. Freedman, "de Finetti's theorem for Markov chains", Annals of Probability 8 (1980), 115–130.

noncomputable def TauCeti.Probability.spareStateLaw : MeasureTheory.Measure (Fin 3)

The fair-coin law on the three-letter alphabet Fin 3: the uniform law of the two letters 0 and 1, giving no mass to the spare letter 2.

Equations

• TauCeti.Probability.spareStateLaw = (PMF.uniformOfFinset {0, 1} TauCeti.Probability.spareStateLaw._proof_2✝).toMeasure

instance TauCeti.Probability.instIsProbabilityMeasureFinOfNatNatSpareStateLaw : MeasureTheory.IsProbabilityMeasure spareStateLaw

@[simp]

theorem TauCeti.Probability.spareStateLaw_singleton_two : spareStateLaw {2} = 0

The spare letter is null.

@[simp]

theorem TauCeti.Probability.spareStateLaw_singleton_of_ne_two {a : Fin 3} (ha : a ≠ 2) : spareStateLaw {a} = 2⁻¹

Each of the two letters the process uses carries mass 2⁻¹.

noncomputable def TauCeti.Probability.spareStateMeasure : MeasureTheory.Measure (ℕ → Fin 3)

The law of the example: fair-coin i.i.d. sequences in the alphabet Fin 3.

Equations

• TauCeti.Probability.spareStateMeasure = MeasureTheory.Measure.infinitePi fun (x : ℕ) => TauCeti.Probability.spareStateLaw

instance TauCeti.Probability.instIsProbabilityMeasureForallNatFinOfNatSpareStateMeasure : MeasureTheory.IsProbabilityMeasure spareStateMeasure

@[reducible, inline]

abbrev TauCeti.Probability.spareStateProcess : ℕ → (ℕ → Fin 3) → Fin 3

The example's process: the coordinates of a fair-coin sequence in the alphabet Fin 3.

Equations

• TauCeti.Probability.spareStateProcess n x = x n

theorem TauCeti.Probability.measurable_spareStateProcess (n : ℕ) : Measurable (spareStateProcess n)

Each coordinate of the example is measurable.

theorem TauCeti.Probability.spareStateMeasure_map_spareStateProcess (n : ℕ) : MeasureTheory.Measure.map (spareStateProcess n) spareStateMeasure = spareStateLaw

Each coordinate of the example has the fair-coin law.

theorem TauCeti.Probability.spareStateProcess_iIndepFun : ProbabilityTheory.iIndepFun spareStateProcess spareStateMeasure

The coordinates of the example are independent.

theorem TauCeti.Probability.spareStateProcess_identDistrib (n : ℕ) : ProbabilityTheory.IdentDistrib (spareStateProcess n) (spareStateProcess 0) spareStateMeasure spareStateMeasure

Every coordinate of the example is identically distributed with its zeroth coordinate.

theorem TauCeti.Probability.spareStateProcess_exchangeable : Exchangeable spareStateMeasure spareStateProcess

The example is exchangeable, being i.i.d.

theorem TauCeti.Probability.spareStateProcess_markovExchangeable : MarkovExchangeable spareStateMeasure spareStateProcess

The example is Markov exchangeable, the first Diaconis–Freedman hypothesis.

theorem TauCeti.Probability.spareStateProcess_recurrent : Recurrent spareStateMeasure spareStateProcess

The example is recurrent, the second Diaconis–Freedman hypothesis. Recurrence constrains only the letters the process takes, and says nothing about the spare letter 2.

theorem TauCeti.Probability.spareStateProcess_not_rowExchangeable_successorProcess : ¬RowExchangeable spareStateMeasure (successorProcess spareStateProcess)

The successor array of a recurrent Markov exchangeable process need not be row exchangeable. Row exchangeability would move the head of the row of 0 while leaving the spare row where it is, and the two are tied by TauCeti.successorArray_eq_successorArray_zero_of_forall_ne. On the paths that open 0, 0, 1, 1 and never take the spare letter — an event of probability 16⁻¹, since avoiding the spare letter is almost sure — the tie is broken, so the reindexed array does not almost surely satisfy an identity the original array almost surely satisfies.

Together with spareStateProcess_markovExchangeable and spareStateProcess_recurrent this shows that the row-exchangeability input of TauCeti.Probability.mixedMarkovChain_of_rowExchangeable cannot be obtained for the plain successor array from recurrence and Markov exchangeability alone.