A stationary process that is not exchangeable: the deterministic 3-cycle #
This file discharges a worked example of the Exchangeability roadmap
(TauCetiRoadmap/Exchangeability/README.md, "Worked examples"):
A stationary non-reversible finite-state Markov chain — for instance the deterministic 3-cycle with uniform stationary law — is shift-invariant but not exchangeable, since the law of
(X₀, X₁)differs from that of(X₁, X₀). This keeps stationarity, shift-invariance, and exchangeability distinct.
Take the base space Ω = ZMod 3 with its uniform probability law threeCycleMeasure = ProbabilityTheory.uniformOn Set.univ, and the deterministic rotation process threeCycle n ω = ω + n. Starting from a uniform state and stepping by the 3-cycle, the process is stationary:
its path law is invariant under the one-sided shift
(threeCycle_measurePreserving_shift), because shifting the sample path of ω gives the sample
path of ω + 1, and the uniform law is translation invariant.
It is a deterministic Markov chain, hence a mixture of Markov chains
(threeCycle_mixedMarkovChain) and so Markov exchangeable (threeCycle_markovExchangeable); since
it is not exchangeable, this is also the example showing that Exchangeable is strictly stronger
than MarkovExchangeable, and — through threeCycle_not_mixedIID — that MixedIID is strictly
stronger than MixedMarkovChain.
It is, however, neither exchangeable (threeCycle_not_exchangeable) nor contractable
(threeCycle_not_contractable): the pair (X₀, X₁) = (ω, ω + 1) lands in
{(0, 1), (1, 2), (2, 0)}, so swapping the two coordinates — or reading off the pair (X₀, X₂)
instead — produces a different two-dimensional law. This separates stationarity and
shift-invariance from the symmetry notions, as the roadmap example asks.
The example uses the Layer 0 API (Exchangeable, Contractable, pathLaw, blockLaw, shift)
together with the Layer 8 MarkovExchangeable / MixedMarkovChain interface and MixedIID, and
Mathlib's translation invariance of the counting measure on a group
(MeasureTheory.map_add_right_eq_self) and its MeasureTheory.diracProba; it needs no material
from cameronfreer/exchangeability.
The deterministic 3-cycle process on ZMod 3: from state ω, the n-th coordinate is the
n-fold rotation ω + n.
Equations
- TauCeti.Probability.threeCycle n ω = ω + ↑n
Instances For
The uniform probability law on ZMod 3, the stationary law of the 3-cycle. This is a def
(not an abbrev) so that the IsAddRightInvariant instance below keys on threeCycleMeasure
and stays scoped to this example, rather than leaking to the general uniformOn Set.univ.
Instances For
The stationary measure of the 3-cycle is the uniform law on ZMod 3.
The stationary law of the 3-cycle is a probability measure.
The uniform law on ZMod 3 is invariant under right addition, supplying the translation
invariance used in the shift-stationarity proof.
The uniform law gives mass 3⁻¹ to each singleton.
The 3-cycle is stationary. Its path law is preserved by the one-sided shift: shifting the
sample path of ω yields the sample path of ω + 1, and the uniform law is translation
invariant.
The 3-cycle is not contractable. The pair law (X₀, X₂) along the strictly increasing
selection 0 < 2 differs from the prefix pair law (X₀, X₁): on the rectangle {X₀ = 0, X₁ = 1}
the prefix law has mass 3⁻¹ while the spread law has mass 0.
The 3-cycle is not exchangeable. Its two-coordinate prefix law already fails the finite
exchangeability symmetry: the pair (X₀, X₁) = (ω, ω + 1) ranges over
{(0, 1), (1, 2), (2, 0)}, so the law of (X₀, X₁) differs from that of (X₁, X₀).
The 3-cycle has the finite-dimensional laws of a Markov chain. A path of length n + 1 is
possible only if every step advances the state by one, in which case it is determined by its
starting state and carries the uniform mass 3⁻¹.
The uniform initial law of the 3-cycle, bundled as a probability measure.
Equations
Instances For
The measure underlying the bundled initial law is threeCycleMeasure.
The bundled initial law gives mass 3⁻¹ to each singleton.
The deterministic transition matrix of the 3-cycle, sending the state a to the point mass at
its successor a + 1.
Equations
Instances For
The measure underlying the bundled deterministic step is the Dirac mass at the successor state.
The 3-cycle is a mixture of Markov chains, with named witnesses — degenerately, being a single Markov chain: the uniform initial law and the deterministic successor step reproduce its finite path laws.
The 3-cycle is a mixture of Markov chains. With threeCycle_not_mixedIID, this shows that
mixing over Markov chains is strictly more general than mixing over i.i.d. laws.
The 3-cycle is Markov exchangeable, being a mixture of Markov chains: its finite path
probabilities factor through the starting state and the transition counts. With
threeCycle_not_exchangeable, this separates MarkovExchangeable from Exchangeable.
The 3-cycle is not mixed i.i.d., since a mixed i.i.d. process is exchangeable and the 3-cycle is not.