Last-exit reconstruction of a finite path

This file proves the finite combinatorial lemma behind the successor-array proof of the Diaconis--Freedman theorem. Fix a finite prefix of a path and reorder the successor entries used by that prefix, separately within each row. If each reordering permutes the used part of its row among itself and fixes its last entry, following the reordered successor rows produces another prefix with the same endpoint and the same transition counts.

The fixed-last hypothesis is essential: it is the last-exit condition which prevents the reconstructed path from closing a proper subtrail before all prescribed successor entries have been used. It enters exactly once, in TauCeti.visitCount_pathOfReindexedSuccessors_lt_visitCount, where it rules out the maximal deficient index being skipped. The proof follows Lemma 1(b) of Fortini, Ladelli, Petris, and Regazzini, On mixtures of distributions of Markov chains, Stochastic Processes and their Applications 100 (2002), 147--165.

Main definitions

• TauCeti.LastExitAdmissible: packages the two hypotheses of finite last-exit reconstruction.
• TauCeti.pathOfReindexedSuccessors: the path rebuilt after reindexing each row of the successor array of the original path.

Main results

• TauCeti.lastExitAdmissible_of_support_lt_visitCount: deterministic support criterion for last-exit admissibility.
• TauCeti.visitCount_pathOfReindexedSuccessors_lt_visitCount: the last-exit lemma — the reconstruction only ever consumes successor entries that the original prefix consumes too.
• TauCeti.successorArray_pathOfReindexedSuccessors_of_lt_visitCount: the entries it consumes are the prescribed reindexed ones.
• TauCeti.visitCount_pathOfReindexedSuccessors, TauCeti.pathOfReindexedSuccessors_eq and TauCeti.transitionCount_pathOfReindexedSuccessors: the last-exit reconstruction has the same visit counts, the same endpoint, and the same transition counts as the original prefix.
• TauCeti.LastExitAdmissible.symm_pathOfReindexedSuccessors and TauCeti.pathOfReindexedSuccessors_symm_apply_apply: inverse row reindexing is admissible and recovers the original finite prefix.

References

• S. Fortini, L. Ladelli, G. Petris, and E. Regazzini, "On mixtures of distributions of Markov chains", Stochastic Processes and their Applications 100 (2002), 147--165, Lemma 1(b).
• P. Diaconis and D. Freedman, "de Finetti's theorem for Markov chains", Annals of Probability 8 (1980), 115--130.
• Roadmap: TauCetiRoadmap/Exchangeability/README.md, Layer 8, "Markov exchangeability".

def TauCeti.LastExitAdmissible {α : Type u_1} (π : α → Equiv.Perm ℕ) (x : ℕ → α) (m : ℕ) : Prop

A family of successor-row permutations is last-exit admissible for the prefix of x before time m when it preserves every used row prefix and fixes the final used position in each nonempty row.

These are exactly the two hypotheses needed by finite last-exit reconstruction: the first keeps every reindexed successor entry inside the finite prefix, and the second prevents reconstruction from closing a proper subtrail before all prescribed entries have been consumed.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.lastExitAdmissible_iff {α : Type u_1} {π : α → Equiv.Perm ℕ} {x : ℕ → α} {m : ℕ} : LastExitAdmissible π x m ↔ (∀ (a : α), ∀ k < visitCount x a m, (π a) k < visitCount x a m) ∧ ∀ (a : α), 0 < visitCount x a m → (π a) (visitCount x a m - 1) = visitCount x a m - 1

The two conditions defining last-exit admissibility.

theorem TauCeti.LastExitAdmissible.maps_lt_visitCount {α : Type u_1} {π : α → Equiv.Perm ℕ} {x : ℕ → α} {m : ℕ} (h : LastExitAdmissible π x m) {a : α} {k : ℕ} (hk : k < visitCount x a m) : (π a) k < visitCount x a m

A last-exit-admissible permutation keeps every used row index inside the used prefix.

theorem TauCeti.LastExitAdmissible.apply_visitCount_sub_one {α : Type u_1} {π : α → Equiv.Perm ℕ} {x : ℕ → α} {m : ℕ} (h : LastExitAdmissible π x m) {a : α} (ha : 0 < visitCount x a m) : (π a) (visitCount x a m - 1) = visitCount x a m - 1

A last-exit-admissible permutation fixes the last used index of every nonempty row.

theorem TauCeti.lastExitAdmissible_of_support_lt_visitCount {α : Type u_1} {π : α → Equiv.Perm ℕ} {x : ℕ → α} {m : ℕ} (h : ∀ (a : α), 0 < visitCount x a m → ∀ (k : ℕ), (π a) k ≠ k → k + 1 < visitCount x a m) : LastExitAdmissible π x m

If every moved position lies strictly below the last used position of its row, then the row permutations are last-exit admissible.

noncomputable def TauCeti.pathOfReindexedSuccessors {α : Type u_1} (π : α → Equiv.Perm ℕ) (x : ℕ → α) : ℕ → α

Rebuild x after reindexing the entries in each row of its successor array by π.

Equations

• TauCeti.pathOfReindexedSuccessors π x = TauCeti.pathOfSuccessors (x 0) fun (a : α) (k : ℕ) => TauCeti.successorArray x a ((π a) k)

theorem TauCeti.pathOfReindexedSuccessors_def {α : Type u_1} (π : α → Equiv.Perm ℕ) (x : ℕ → α) : pathOfReindexedSuccessors π x = pathOfSuccessors (x 0) fun (a : α) (k : ℕ) => successorArray x a ((π a) k)

The defining equation for reconstruction from reindexed successor rows.

@[simp]

theorem TauCeti.pathOfReindexedSuccessors_zero {α : Type u_1} (π : α → Equiv.Perm ℕ) (x : ℕ → α) : pathOfReindexedSuccessors π x 0 = x 0

A rebuilt path starts where the original does.

@[simp]

theorem TauCeti.pathOfReindexedSuccessors_succ {α : Type u_1} (π : α → Equiv.Perm ℕ) (x : ℕ → α) (n : ℕ) : pathOfReindexedSuccessors π x (n + 1) = successorArray x (pathOfReindexedSuccessors π x n) ((π (pathOfReindexedSuccessors π x n)) (visitCount (pathOfReindexedSuccessors π x) (pathOfReindexedSuccessors π x n) n))

The recursion equation for a path rebuilt from reindexed successor rows.

@[simp]

theorem TauCeti.pathOfReindexedSuccessors_one {α : Type u_1} (x : ℕ → α) : pathOfReindexedSuccessors 1 x = x

Reindexing every successor row by the identity leaves the path unchanged.

theorem TauCeti.successorArray_pathOfReindexedSuccessors_of_lt_visitCount {α : Type u_1} (π : α → Equiv.Perm ℕ) (x : ℕ → α) (a : α) {k n : ℕ} (hk : k < visitCount (pathOfReindexedSuccessors π x) a n) : successorArray (pathOfReindexedSuccessors π x) a k = successorArray x a ((π a) k)

Every successor entry consumed by a reindexed reconstruction is the corresponding reindexed entry of the original successor array.

theorem TauCeti.visitCount_pathOfReindexedSuccessors_lt_visitCount {α : Type u_1} (π : α → Equiv.Perm ℕ) (x : ℕ → α) (m : ℕ) (h : LastExitAdmissible π x m) (i : ℕ) : i < m → visitCount (pathOfReindexedSuccessors π x) (pathOfReindexedSuccessors π x i) i < visitCount x (pathOfReindexedSuccessors π x i) m

The last-exit lemma. Under a last-exit reindexing, every step of the reconstruction consumes a successor entry that the original prefix consumes too: at each time i < m the reconstruction has visited its current state strictly fewer times than the original prefix visits it before m.

This is Lemma 1(b) of Fortini, Ladelli, Petris, and Regazzini.

theorem TauCeti.visitCount_pathOfReindexedSuccessors {α : Type u_1} (π : α → Equiv.Perm ℕ) (x : ℕ → α) (m : ℕ) (h : LastExitAdmissible π x m) (a : α) : visitCount (pathOfReindexedSuccessors π x) a m = visitCount x a m

A last-exit reindexing uses each prescribed successor row exactly as often as the original finite prefix.

theorem TauCeti.pathOfReindexedSuccessors_eq {α : Type u_1} (π : α → Equiv.Perm ℕ) (x : ℕ → α) (m : ℕ) (h : LastExitAdmissible π x m) : pathOfReindexedSuccessors π x m = x m

A finite path reconstructed after last-exit reindexing has the same endpoint as the original prefix.

theorem TauCeti.transitionCount_pathOfReindexedSuccessors {α : Type u_1} (π : α → Equiv.Perm ℕ) (x : ℕ → α) (m : ℕ) (h : LastExitAdmissible π x m) (a b : α) : transitionCount (fun (i : Fin (m + 1)) => pathOfReindexedSuccessors π x ↑i) a b = transitionCount (fun (i : Fin (m + 1)) => x ↑i) a b

A finite path reconstructed after last-exit reindexing has the same transition counts as the original prefix.

theorem TauCeti.LastExitAdmissible.symm_pathOfReindexedSuccessors {α : Type u_1} {π : α → Equiv.Perm ℕ} {x : ℕ → α} {m : ℕ} (h : LastExitAdmissible π x m) : LastExitAdmissible (fun (a : α) => Equiv.symm (π a)) (pathOfReindexedSuccessors π x) m

The inverse row permutations are last-exit admissible for the reconstructed prefix. This allows the reconstructed path to be reindexed in reverse through the same finite horizon.

theorem TauCeti.pathOfReindexedSuccessors_symm_apply_apply {α : Type u_1} {π : α → Equiv.Perm ℕ} {x : ℕ → α} {m : ℕ} (h : LastExitAdmissible π x m) {i : ℕ} (hi : i ≤ m) : pathOfReindexedSuccessors (fun (a : α) => Equiv.symm (π a)) (pathOfReindexedSuccessors π x) i = x i

Reindexing a finite prefix by inverse row permutations recovers the prefix. If π is last-exit admissible through time m, then reconstructing from the π-reindexed successor rows and subsequently from the π⁻¹-reindexed rows returns x i for every i ≤ m.

The conclusion is deliberately restricted to the admissible finite horizon: unused successor entries are unconstrained, so the two infinite reconstructions need not agree after m.