Documentation

TauCeti.Probability.Exchangeability.MarkovExchangeable

Markov exchangeability #

A process X : ℕ → Ω → α on a countable state space is Markov exchangeable — Diaconis and Freedman's partial exchangeability — when two finite paths that start at the same state and make the same number of transitions from each state to each state are equally likely:

u 0 = v 0  →  transitionCount u = transitionCount v  →  prefixLaw μ X (n + 1) {u} =
  prefixLaw μ X (n + 1) {v}

This is the symmetry that a Markov chain has and an exchangeable process has, and it is the hypothesis of the Diaconis–Freedman representation theorem, which says that a recurrent Markov exchangeable process is a mixture of Markov chains. This file sets up the notion and its two sources.

Markov exchangeability is a genuine weakening of exchangeability. Exchangeability asks for invariance under all rearrangements of a finite path, whereas Markov exchangeability asks for it only between paths sharing a start and a transition-count matrix; the latter class of paths is strictly smaller, because a rearrangement generally destroys the transition counts. That the implication Exchangeable → MarkovExchangeable nevertheless holds is a conservation law for words: the transition counts and the first letter already determine the occurrence counts, hence the rearrangement class (TauCeti.exists_perm_comp_of_transitionCount_eq). That the implication is strict is witnessed by the deterministic 3-cycle, in TauCeti/Probability/Exchangeability/ThreeCycle.lean.

Main definitions #

Main results #

References #

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

source
def TauCeti.Probability.MarkovExchangeable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : ℕ → Ω → α) :
Prop

Markov exchangeability, Diaconis and Freedman's partial exchangeability: a measurable process has equally likely finite paths whenever they have the same starting state and the same transition counts. The countability and measurable-singleton conjuncts restrict this singleton-mass formulation to discrete state spaces, where it is non-vacuous and determines the finite-path laws.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.Probability.MarkovExchangeable.intro {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (h : ∀ (n : ℕ) (u v : Fin (n + 1) → α), u 0 = v 0 → (∀ (a b : α), transitionCount u a b = transitionCount v a b) → (prefixLaw μ X (n + 1)) {u} = (prefixLaw μ X (n + 1)) {v}) :
    MarkovExchangeable μ X

    Constructor from discrete-state instances, coordinatewise a.e. measurability, and invariance under paths with equal transition counts.

    source
    theorem TauCeti.Probability.MarkovExchangeable.countable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : MarkovExchangeable μ X) :
    Countable α

    The state space of a Markov exchangeable process is countable.

    source
    theorem TauCeti.Probability.MarkovExchangeable.measurableSingletonClass {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : MarkovExchangeable μ X) :
    MeasurableSingletonClass α

    Singletons in the state space of a Markov exchangeable process are measurable.

    source
    theorem TauCeti.Probability.MarkovExchangeable.aemeasurable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : MarkovExchangeable μ X) (i : ℕ) :
    AEMeasurable (X i) μ

    Every coordinate of a Markov exchangeable process is a.e. measurable.

    source
    theorem TauCeti.Probability.MarkovExchangeable.prefixLaw_singleton_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : MarkovExchangeable μ X) (n : ℕ) (u v : Fin (n + 1) → α) (h0 : u 0 = v 0) (hcount : ∀ (a b : α), transitionCount u a b = transitionCount v a b) :
    (prefixLaw μ X (n + 1)) {u} = (prefixLaw μ X (n + 1)) {v}

    Paths with the same starting state and transition counts have the same probability under a Markov exchangeable process.

    source
    theorem TauCeti.Probability.MarkovExchangeable.prefixLaw_apply_eq_of_equiv {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : MarkovExchangeable μ X) (n : ℕ) {s t : Set (Fin (n + 1) → α)} (e : ↑s ≃ ↑t) (h0 : ∀ (w : ↑s), ↑(e w) 0 = ↑w 0) (hcount : ∀ (w : ↑s) (a b : α), transitionCount (↑(e w)) a b = transitionCount (↑w) a b) :
    (prefixLaw μ X (n + 1)) s = (prefixLaw μ X (n + 1)) t

    A bijection pairing Markov-equivalent paths preserves prefix-law mass. More precisely, an equivalence between two sets of finite paths preserves their mass when it pairs paths with the same initial state and directed transition counts.

    This is the form used by finite last-exit reconstruction: the reconstruction gives an equivalence between two collections of admissible prefixes, rather than a permutation of every finite path.

    source
    theorem TauCeti.Probability.MarkovExchangeable.prefixLaw_map_perm_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : MarkovExchangeable μ X) (n : ℕ) (e : Equiv.Perm (Fin (n + 1) → α)) (h0 : ∀ (w : Fin (n + 1) → α), e w 0 = w 0) (hcount : ∀ (w : Fin (n + 1) → α) (a b : α), transitionCount (e w) a b = transitionCount w a b) :
    MeasureTheory.Measure.map (⇑e) (prefixLaw μ X (n + 1)) = prefixLaw μ X (n + 1)

    A transition-count-preserving permutation preserves a Markov-exchangeable prefix law. The permutation may rearrange finite paths in any way, provided it preserves their initial state and every directed transition count. This is the setwise form of Markov exchangeability used when a deterministic reconstruction permutes all paths in a finite Markov-exchangeability class.

    source
    @[simp]
    theorem TauCeti.Probability.markovExchangeable_iff {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} :
    MarkovExchangeable μ X ↔ (∀ (i : ℕ), AEMeasurable (X i) μ) ∧ ∀ (n : ℕ) (u v : Fin (n + 1) → α), u 0 = v 0 → (∀ (a b : α), transitionCount u a b = transitionCount v a b) → (prefixLaw μ X (n + 1)) {u} = (prefixLaw μ X (n + 1)) {v}

    Simp normal form for MarkovExchangeable.

    source
    theorem TauCeti.Probability.markovExchangeable_iff_prefixLaw_map_perm_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} :
    MarkovExchangeable μ X ↔ (∀ (i : ℕ), AEMeasurable (X i) μ) ∧ ∀ (n : ℕ) (e : Equiv.Perm (Fin (n + 1) → α)), (∀ (w : Fin (n + 1) → α), e w 0 = w 0) → (∀ (w : Fin (n + 1) → α) (a b : α), transitionCount (e w) a b = transitionCount w a b) → MeasureTheory.Measure.map (⇑e) (prefixLaw μ X (n + 1)) = prefixLaw μ X (n + 1)

    Permutation-invariance characterization of Markov exchangeability. A measurable process is Markov exchangeable exactly when each finite prefix law is invariant under every permutation of path words that preserves the initial state and every directed transition count.

    This is stronger as an interface than equality of singleton masses: it transports arbitrary events at once. Conversely, swapping any two words in one Markov-exchangeability class recovers the defining singleton equality.

    source
    theorem TauCeti.Probability.Exchangeable.markovExchangeable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : Exchangeable μ X) (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) :
    MarkovExchangeable μ X

    An exchangeable process is Markov exchangeable. Two paths with a common start and common transition counts are rearrangements of each other, so exchangeability already equates them.

    source
    theorem TauCeti.Probability.markovExchangeable_of_prefixLaw_singleton_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (p₀ : α → ENNReal) (p : α → α → ENNReal) (h : ∀ (n : ℕ) (w : Fin (n + 1) → α), (prefixLaw μ X (n + 1)) {w} = p₀ (w 0) * ∏ i : Fin n, p (w i.castSucc) (w i.succ)) :
    MarkovExchangeable μ X

    A Markov chain is Markov exchangeable. The hypothesis is the defining product form of the finite-dimensional laws of a Markov chain: an initial weight p₀ at the starting state times the transition weights p along the path. Only the product form matters, not that p is a probability kernel.

    source
    theorem TauCeti.Probability.markovExchangeable_pathLaw_iff {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) :
    (MarkovExchangeable (pathLaw μ X) fun (n : ℕ) (x : ℕ → α) => x n) ↔ MarkovExchangeable μ X

    The process-level and path-law formulations of Markov exchangeability agree.