Documentation

TauCeti.Probability.Exchangeability.Excursion

Reordering the excursions of a Markov exchangeable path #

A finite path that starts at a state a₀ and returns to it splits at its visits to a₀ into excursions, and TauCeti.loopPathAt a₀ bs spells out the path traversing the excursions bs : List (List α) in the listed order. This file proves that a Markov exchangeable process gives the same mass to every ordering of one list of excursions:

bs ~ bs'  →  prefixLaw μ X (n + 1) {loopPathAt a₀ bs} = prefixLaw μ X (n + 1) {loopPathAt a₀ bs'}

Markov exchangeability says that the mass of a finite path depends only on its first state and its transition counts, and reordering excursions changes neither: every excursion is entered at a₀ and left back to a₀, so the transitions of the whole loop are those of its excursion loops, gathered in an order that a permutation of the excursions rearranges (TauCeti.transitionCount_loopPathAt_eq_of_perm).

Every finite path returning to its starting state arises this way (TauCeti.exists_loopPathAt), so the statement is a symmetry of all the finite-path masses of such a process, not of a special family of paths; TauCeti.Probability.MarkovExchangeable.exists_excursions_prefixLaw_eq packages the two together.

This is the finite-path symmetry that Diaconis and Freedman's representation theorem for Markov exchangeable processes rests on: a recurrent Markov exchangeable process returns to its initial state infinitely often, so its excursions from that state form a genuine sequence of random finite paths, and the identities below are that sequence's finite-dimensional exchangeability. The combinatorial excursion process and its reconstruction of a recurrent path segment are set up in TauCeti.Combinatorics.Enumerative.ExcursionProcess, and TauCeti.Probability.Exchangeability.Recurrence.Excursion adds the recurrence hypothesis at the process level to assemble the identities below into exchangeability of that process (TauCeti.Probability.MarkovExchangeable.exchangeable_excursionProcess) and to run de Finetti on it. Exhibiting the original process as a mixture of Markov chains (TauCeti.Probability.MixedMarkovChain, whose converse direction is TauCeti.Probability.MixedMarkovChainWith.markovExchangeable) is the remaining step.

Main results #

References #

No material is adapted from cameronfreer/exchangeability, which treats exchangeable rather than Markov exchangeable sequences.

source
theorem TauCeti.Probability.MarkovExchangeable.prefixLaw_loopPathAt_eq_of_perm {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : MarkovExchangeable μ X) (a₀ : α) {bs bs' : List (List α)} (hperm : bs.Perm bs') {n : ℕ} (hn : loopSteps bs = n) :
(prefixLaw μ X (n + 1)) {fun (i : Fin (n + 1)) => loopPathAt a₀ bs ↑i} = (prefixLaw μ X (n + 1)) {fun (i : Fin (n + 1)) => loopPathAt a₀ bs' ↑i}

Reordering the excursions of a loop does not change its mass under a Markov exchangeable process. The two paths start at the same state and have the same transition counts, which is exactly what Markov exchangeability sees.

source
theorem TauCeti.Probability.MarkovExchangeable.prefixLaw_singleton_eq_of_perm_excursions {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : MarkovExchangeable μ X) (a₀ : α) {n : ℕ} {u v : Fin (n + 1) → α} {bs bs' : List (List α)} (hperm : bs.Perm bs') (hn : loopSteps bs = n) (hu : ∀ (i : Fin (n + 1)), loopPathAt a₀ bs ↑i = u i) (hv : ∀ (i : Fin (n + 1)), loopPathAt a₀ bs' ↑i = v i) :
(prefixLaw μ X (n + 1)) {u} = (prefixLaw μ X (n + 1)) {v}

Two finite paths that traverse the same excursions in different orders are equally likely. The user-facing form of TauCeti.Probability.MarkovExchangeable.prefixLaw_loopPathAt_eq_of_perm: the hypotheses say that u and v both start at a₀ and run through the excursions bs, respectively bs', and TauCeti.exists_loopPathAt supplies such a list for every finite path that returns to its starting state.

source
theorem TauCeti.Probability.MarkovExchangeable.measure_setOf_loopPathAt_eq_of_perm {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : MarkovExchangeable μ X) (a₀ : α) {bs bs' : List (List α)} (hperm : bs.Perm bs') {n : ℕ} (hn : loopSteps bs = n) :
μ {ω : Ω | ∀ i ≤ n, X i ω = loopPathAt a₀ bs i} = μ {ω : Ω | ∀ i ≤ n, X i ω = loopPathAt a₀ bs' i}

Reordering the excursions of a loop does not change the probability that the process traverses it. The event-level form of TauCeti.Probability.MarkovExchangeable.prefixLaw_loopPathAt_eq_of_perm.

source
theorem TauCeti.Probability.MarkovExchangeable.exists_excursions_prefixLaw_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : MarkovExchangeable μ X) {n : ℕ} (w : Fin (n + 1) → α) (hw : w (Fin.last n) = w 0) :
∃ (bs : List (List α)), loopSteps bs = n ∧ (∀ e ∈ bs, w 0 ∉ e) ∧ (∀ (i : Fin (n + 1)), loopPathAt (w 0) bs ↑i = w i) ∧ ∀ (bs' : List (List α)), bs.Perm bs' → (prefixLaw μ X (n + 1)) {fun (i : Fin (n + 1)) => loopPathAt (w 0) bs' ↑i} = (prefixLaw μ X (n + 1)) {w}

The finite-path symmetry of a Markov exchangeable process. Every finite path w that returns to its starting state is the loop of a list of excursions, none of which visits that state, and every reordering of those excursions has the same mass as w itself.