Kolmogorov's criterion for reversibility

StructureStochastic matrix#✓fully proved

For a natural number \(M\), a stochastic matrix of size \(M + 1\) is a square matrix \(P = (P_{ij})\) indexed by the states \(\{0, 1, \dots, M\}\), with real entries \(P_{ij} \ge 0\) for all states \(i, j\), whose rows sum to \(1\): \(\sum_j P_{ij} = 1\) for every \(i\). It is the transition matrix of a Markov chain on these \(M + 1\) states.

structure StochasticMatrix (M : ℕ) where
  prob : Fin (M + 1) → Fin (M + 1) → ℝ
  nonneg : ∀ i j, 0 ≤ prob i j
  row_sum : ∀ i, ∑ j, prob i j = 1

Used by 78

Used byDetailed balance of the Jukes–Cantor chain · Jukes–Cantor transition matrix as a stochastic matrix · Chapman–Kolmogorov equation for the Jukes–Cantor chain · Moran process as a stochastic matrix · Fixation probability of the chain · Loss probability of the chain · Almost-sure absorption of the Wright–Fisher chain · Finite Wright–Fisher chain is absorbed almost surely · Fixation probability of a Wright–Fisher chain · Loss probability of a Wright–Fisher chain · Fixation probability of the finite Wright–Fisher chain · Loss probability of an allele in the finite Wright–Fisher chain · Geometric decay of heterozygosity under Wright–Fisher drift · Multi-step martingale property of the Wright–Fisher allele count · One-step decay of heterozygosity under Wright–Fisher drift · One-step martingale property of the Wright–Fisher allele count · Limiting fixation probability of a Wright–Fisher chain · Neutral Wright–Fisher transition matrix · Entries of the Wright–Fisher matrix · Wright–Fisher rows are binomial laws · Fixation of an allele is absorbing in the Wright–Fisher chain · Loss of an allele is absorbing in the Wright–Fisher chain · Canonical Markov law started from a point starts there almost surely · Canonical Markov law satisfies the finite Markov chain specification · Powers of an ergodic chain are eventually all positive · Pairwise positive powers of an ergodic chain · Identity Markov chain · Ergodic finite Markov chain · Ergodicity is primitivity of the transition matrix · The uniform Markov chain is ergodic · Additivity of recursive matrix powers · Recursive matrix power agrees with the matrix power · First recursive power of a stochastic matrix · Later powers of a positive stochastic matrix power stay positive · Recursive powers of a stochastic matrix power · Powers of a stochastic matrix are stochastic · Power of a stochastic matrix · Powers of an ergodic Markov chain are ergodic · Transition probabilities of the identity chain · Transition probabilities of the uniform chain · Underlying matrix of a stochastic matrix · Underlying matrix of a stochastic matrix power · Uniform Markov chain on finitely many states · Bridge: finite-state Markov chains satisfy the general one-step Markov property · Transition kernel of a stochastic matrix · Transition kernel of a stochastic matrix evaluated on a set · Finite-state Markov chain with a given transition matrix · One-step forward equation · Finite Markov chains satisfy the general Markov property · Cycle weight · Detailed balance for cycle weights · Cycle weights along a positive transition · Path independence of cycle weight · Detailed balance · Detailed balance implies stationarity · Detailed balance distributions of irreducible chains are positive · Irreducible chains have positive paths · Paths from positive matrix powers · Irreducible stochastic matrix · Reversible stochastic matrix · Stationary distribution · Kolmogorov's cycle condition · Kolmogorov's cycle theorem, necessity half · Kolmogorov's cycle theorem, sufficiency · Forward path product · Joining positive paths · Path products are nonnegative · Positive path products have positive steps · Ratio product along a path · Ratio product of joined paths · First step of the ratio product · The ratio product around a loop is one · The ratio product is nonnegative · The ratio product as a finite product · Positive paths have positive ratio product · Ratio product after appending a state · Matrix powers of a stochastic matrix · Powers of a stochastic matrix are nonnegative

DefinitionMatrix powers of a stochastic matrix#✓fully proved

For a stochastic matrix \(P\) on the finite state space \(\{0, 1, \dots, M\}\) and \(n \in \mathbb{N}\), the \(n\)-th matrix power \(P^n\) is defined by \(P^0 = I\), the identity matrix, and \((P^{n+1})_{ij} = \sum_k P(i, k) (P^n)_{kj}\). The entry \((P^n)_{ij}\) is the probability of moving from state \(i\) to state \(j\) in exactly \(n\) steps.

def matPow (P : StochasticMatrix M) : ℕ → (Fin (M + 1) → Fin (M + 1) → ℝ)
  | 0 => fun i j => if i = j then 1 else 0
  | n + 1 => fun i j => ∑ k, P.prob i k * P.matPow n k j

Uses 1 · Used by 29

Statement usesStochastic matrix

Used byChapman–Kolmogorov equation for the Jukes–Cantor chain · Fixation probability of the chain · Loss probability of the chain · Almost-sure absorption of the Wright–Fisher chain · Loss probability of a Wright–Fisher chain · Geometric decay of heterozygosity under Wright–Fisher drift · Multi-step martingale property of the Wright–Fisher allele count · Interior Wright–Fisher states vanish in the limit · Fixation probability in the Wright–Fisher chain · Limiting loss probability of the Wright–Fisher transition matrix · Limiting fixation probability of a Wright–Fisher chain · Powers of an ergodic chain are eventually all positive · Pairwise positive powers of an ergodic chain · The uniform Markov chain is ergodic · Additivity of recursive matrix powers · Recursive matrix power agrees with the matrix power · Powers of the identity chain are the identity matrix · First recursive power of a stochastic matrix · Later powers of a positive stochastic matrix power stay positive · Recursive powers of a stochastic matrix power · Powers of a stochastic matrix are stochastic · The identity Markov chain is not ergodic · Power of a stochastic matrix · Powers of an ergodic Markov chain are ergodic · Detailed balance distributions of irreducible chains are positive · Irreducible chains have positive paths · Paths from positive matrix powers · Irreducible stochastic matrix · Powers of a stochastic matrix are nonnegative

DefinitionIrreducible stochastic matrix#✓fully proved

Let \(P\) be a stochastic matrix on the finite state space \(\{0, 1, \dots, M\}\) and write \(P^n\) for its \(n\)-th matrix power. Then \(P\) is irreducible if for all states \(i\) and \(j\) there is an \(n \ge 1\) with \((P^n)_{ij} > 0\); that is, every state can be reached from every state, itself included, in a positive number of steps.

def IsIrreducible (P : StochasticMatrix M) : Prop :=
  ∀ i j : Fin (M + 1), ∃ n : ℕ, 0 < n ∧ 0 < P.matPow n i j

Uses 2 · Used by 8

Statement usesStochastic matrix · Matrix powers of a stochastic matrix

Used byCycle weight · Detailed balance for cycle weights · Cycle weights along a positive transition · Path independence of cycle weight · Detailed balance distributions of irreducible chains are positive · Irreducible chains have positive paths · Kolmogorov's cycle theorem, necessity half · Kolmogorov's cycle theorem, sufficiency

StructureProbability distribution on a finite state space#✓fully proved

A probability distribution on the finite state space \(\{0, 1, \dots, M\}\) is a function \(\pi\) from the states to \(\mathbb{R}\) with \(\pi(i) \ge 0\) for every state \(i\) and \(\sum_i \pi(i) = 1\).

structure Distribution (M : ℕ) where
  val : Fin (M + 1) → ℝ
  nonneg : ∀ i, 0 ≤ val i
  sum_one : ∑ i, val i = 1

Used by 8

Used byDetailed balance of the Jukes–Cantor chain · Detailed balance · Detailed balance implies stationarity · Detailed balance distributions of irreducible chains are positive · Reversible stochastic matrix · Stationary distribution · Kolmogorov's cycle theorem, necessity half · Kolmogorov's cycle theorem, sufficiency

DefinitionStationary distribution#✓fully proved

A probability distribution \(\pi\) on the finite state space \(\{0, 1, \dots, M\}\) is stationary for a stochastic matrix \(P\) on the same states if \(\pi P = \pi\), that is, \(\sum_i \pi(i) P(i, j) = \pi(j)\) for every state \(j\).

def IsStationary (P : StochasticMatrix M) (π : Distribution M) : Prop :=
  ∀ j, ∑ i, π.val i * P.prob i j = π.val j

Uses 2 · Used by 4

Statement usesStochastic matrix · Probability distribution on a finite state space

Used byDetailed balance implies stationarity · Reversible stochastic matrix · Kolmogorov's cycle theorem, necessity half · Kolmogorov's cycle theorem, sufficiency

DefinitionDetailed balance#✓fully proved

A probability distribution \(\pi\) and a stochastic matrix \(P\) on the finite state space \(\{0, 1, \dots, M\}\) satisfy the detailed balance (reversibility) equations when \(\pi(i) P(i, j) = \pi(j) P(j, i)\) for all states \(i\) and \(j\).

def DetailedBalance (P : StochasticMatrix M) (π : Distribution M) : Prop :=
  ∀ i j : Fin (M + 1), π.val i * P.prob i j = π.val j * P.prob j i

Uses 2 · Used by 6

Statement usesStochastic matrix · Probability distribution on a finite state space

Used byDetailed balance of the Jukes–Cantor chain · Detailed balance implies stationarity · Detailed balance distributions of irreducible chains are positive · Reversible stochastic matrix · Kolmogorov's cycle theorem, necessity half · Kolmogorov's cycle theorem, sufficiency

DefinitionReversible stochastic matrix#✓fully proved

A stochastic matrix \(P\) on the finite state space \(\{0, 1, \dots, M\}\) is reversible if there is a probability distribution \(\pi\) on the states that is stationary for \(P\) and satisfies the detailed balance equations \(\pi(i) P(i, j) = \pi(j) P(j, i)\) for all states \(i, j\).

def IsReversible (P : StochasticMatrix M) : Prop :=
  ∃ π : Distribution M, P.IsStationary π ∧ P.DetailedBalance π

Uses 4 · Used by 2

Statement usesStochastic matrix · Detailed balance · Probability distribution on a finite state space · Stationary distribution

Used byKolmogorov's cycle theorem, necessity half · Kolmogorov's cycle theorem, sufficiency

StructureKolmogorov's cycle condition#✓fully proved

A stochastic matrix \(P\) on the finite state space \(\{0, 1, \dots, M\}\) satisfies Kolmogorov's cycle condition when (1) for all states \(x, y\), \(P(x, y) > 0\) implies \(P(y, x) > 0\); and (2) for every \(n \ge 0\) and every loop of states \(x_0, x_1, \dots, x_n\) with \(x_n = x_0\) and \(\prod_{i=0}^{n-1} P(x_{i+1}, x_i) > 0\), we have \(\prod_{i=0}^{n-1} P(x_i, x_{i+1}) = \prod_{i=0}^{n-1} P(x_{i+1}, x_i)\).

structure KolmogorovCycleCondition (P : StochasticMatrix M) : Prop where
  symm_support : ∀ x y : Fin (M + 1), P.prob x y > 0 → P.prob y x > 0
  cycle_prod : ∀ (n : ℕ) (c : Fin (n + 1) → Fin (M + 1)), c 0 = c (Fin.last n) →
    (∏ i : Fin n, P.prob (c i.succ) (c i.castSucc)) > 0 →
    (∏ i : Fin n, P.prob (c i.castSucc) (c i.succ)) =
      (∏ i : Fin n, P.prob (c i.succ) (c i.castSucc))

Uses 1 · Used by 6

Statement usesStochastic matrix

Used byDetailed balance for cycle weights · Cycle weights along a positive transition · Path independence of cycle weight · Kolmogorov's cycle theorem, necessity half · Kolmogorov's cycle theorem, sufficiency · The ratio product around a loop is one

TheoremDetailed balance implies stationarity#✓fully proved

Let \(P\) be a stochastic matrix on the finite state space \(\{0, 1, \dots, M\}\) and let \(\pi\) be a probability distribution on the same states. If \(\pi\) and \(P\) satisfy the detailed balance equations \(\pi(i) P(i, j) = \pi(j) P(j, i)\) for all states \(i, j\), then \(\pi\) is stationary for \(P\): \(\sum_i \pi(i) P(i, j) = \pi(j)\) for every state \(j\).

theorem detailedBalance_isStationary (P : StochasticMatrix M) (π : Distribution M)
    (hdb : P.DetailedBalance π) : P.IsStationary π

Uses 4 · Used by 1

Statement usesStochastic matrix · Detailed balance · Probability distribution on a finite state space · Stationary distribution

Used byKolmogorov's cycle theorem, sufficiency

LemmaPowers of a stochastic matrix are nonnegative#✓fully proved

Every entry of every power of a stochastic matrix is nonnegative.

lemma matPow_nonneg (P : StochasticMatrix M) : ∀ (n : ℕ) (i j : Fin (M + 1)),
    0 ≤ P.matPow n i j

Uses 2 · Used by 9

Statement usesStochastic matrix · Matrix powers of a stochastic matrix

Used byFixation probability of the chain · Loss probability of the chain · Almost-sure absorption of the Wright–Fisher chain · Loss probability of a Wright–Fisher chain · Interior Wright–Fisher states vanish in the limit · Limiting fixation probability of a Wright–Fisher chain · Later powers of a positive stochastic matrix power stay positive · Power of a stochastic matrix · Detailed balance distributions of irreducible chains are positive

TheoremDetailed balance distributions of irreducible chains are positive#✓fully proved

Let \(P\) be an irreducible stochastic matrix on the finite state space \(\{0, 1, \dots, M\}\). If a probability distribution \(\pi\) satisfies the detailed balance equations \(\pi(i) P(i, j) = \pi(j) P(j, i)\) for all states \(i, j\), then \(\pi(i) > 0\) for every state \(i\).

theorem distribution_pos_of_irreducible_detailedBalance
    (P : StochasticMatrix M) (π : Distribution M)
    (hirr : P.IsIrreducible) (hdb : P.DetailedBalance π) :
    ∀ i, 0 < π.val i

Uses 6 · Used by 1

Statement usesStochastic matrix · Detailed balance · Probability distribution on a finite state space · Irreducible stochastic matrix

Proof usesMatrix powers of a stochastic matrix · Powers of a stochastic matrix are nonnegative

Used byKolmogorov's cycle theorem, necessity half

TheoremKolmogorov's cycle theorem, necessity half#✓fully proved

Let \(P\) be an irreducible stochastic matrix on the finite state space \(\{0, 1, \dots, M\}\). If \(P\) is reversible, that is, some probability distribution \(\pi\) is stationary for \(P\) and satisfies the detailed balance equations \(\pi(i) P(i, j) = \pi(j) P(j, i)\) for all states \(i, j\), then \(P\) satisfies Kolmogorov's cycle condition: (1) for all states \(x, y\), \(P(x, y) > 0\) implies \(P(y, x) > 0\); and (2) for every \(n \ge 0\) and every loop of states \(x_0, x_1, \dots, x_n\) with \(x_n = x_0\) and \(\prod_{i=0}^{n-1} P(x_{i+1}, x_i) > 0\), we have \(\prod_{i=0}^{n-1} P(x_i, x_{i+1}) = \prod_{i=0}^{n-1} P(x_{i+1}, x_i)\).

theorem kolmogorov_cycle_necessity {M : ℕ} (P : StochasticMatrix M)
    (hirr : P.IsIrreducible) (hrev : P.IsReversible) :
    P.KolmogorovCycleCondition

Uses 8

Statement usesStochastic matrix · Irreducible stochastic matrix · Reversible stochastic matrix · Kolmogorov's cycle condition

Proof usesDetailed balance · Probability distribution on a finite state space · Stationary distribution · Detailed balance distributions of irreducible chains are positive

DefinitionForward path product#✓fully proved

For a stochastic matrix \(P\) and a path of states \(x_0, x_1, \dots, x_k\), the path product is the real number \(\prod_{i=0}^{k-1} P(x_i, x_{i+1})\), the product of the forward transition probabilities along the path. For the empty path and for a path consisting of a single state it is \(1\).

def listPathProduct (P : StochasticMatrix M) : List (Fin (M + 1)) → ℝ
  | [] => 1
  | [_] => 1
  | a :: b :: rest => P.prob a b * listPathProduct P (b :: rest)

Uses 1 · Used by 10

Statement usesStochastic matrix

Used byCycle weight · Cycle weights along a positive transition · Path independence of cycle weight · Irreducible chains have positive paths · Paths from positive matrix powers · Kolmogorov's cycle theorem, sufficiency · Joining positive paths · Path products are nonnegative · Positive path products have positive steps · Positive paths have positive ratio product

LemmaPath products are nonnegative#✓fully proved

Let \(P\) be a stochastic matrix on the states \(\{0, \dots, M\}\). For every path (finite list of states), the product of the forward transition probabilities \(P(x, y)\) over consecutive states \(x, y\) along the path is nonnegative.

lemma listPathProduct_nonneg (P : StochasticMatrix M) (path : List (Fin (M + 1))) :
    0 ≤ listPathProduct P path

Uses 2 · Used by 3

Statement usesStochastic matrix · Forward path product

Used byJoining positive paths · Positive path products have positive steps · Positive paths have positive ratio product

DefinitionRatio product along a path#✓fully proved

For a stochastic matrix \(P\) and a path of states \(x_0, x_1, \dots, x_k\), the ratio product is the real number \(\prod_{i=0}^{k-1} \frac{P(x_i, x_{i+1})}{P(x_{i+1}, x_i)}\), where a quotient with denominator \(0\) is taken to be \(0\). For the empty path and for a path consisting of a single state it is \(1\).

This is the quantity that defines the "cycle weight" used to construct a reversible measure from Kolmogorov's cycle condition.

noncomputable def listRatioProduct (P : StochasticMatrix M) : List (Fin (M + 1)) → ℝ
  | [] => 1
  | [_] => 1
  | a :: b :: rest => (P.prob a b / P.prob b a) * listRatioProduct P (b :: rest)

Uses 1 · Used by 10

Statement usesStochastic matrix

Used byCycle weight · Cycle weights along a positive transition · Path independence of cycle weight · Ratio product of joined paths · First step of the ratio product · The ratio product around a loop is one · The ratio product is nonnegative · The ratio product as a finite product · Positive paths have positive ratio product · Ratio product after appending a state

LemmaThe ratio product is nonnegative#✓fully proved

For a stochastic matrix \(P\), the ratio product along every path of states is nonnegative.

lemma listRatioProduct_nonneg (P : StochasticMatrix M) (path : List (Fin (M + 1))) :
    0 ≤ listRatioProduct P path

Uses 2 · Used by 1

Statement usesStochastic matrix · Ratio product along a path

Used byKolmogorov's cycle theorem, sufficiency

LemmaPositive paths have positive ratio product#✓fully proved

Let \(P\) be a stochastic matrix such that \(P(x, y) > 0\) implies \(P(y, x) > 0\) for all states \(x\) and \(y\). If the forward path product along a path of states is positive, then the ratio product along that path is positive.

lemma listRatioProduct_pos_of_listPathProduct_pos (P : StochasticMatrix M)
    (hsymm : ∀ x y : Fin (M + 1), P.prob x y > 0 → P.prob y x > 0)
    (path : List (Fin (M + 1))) (h : 0 < listPathProduct P path) :
    0 < listRatioProduct P path

Uses 4 · Used by 2

Statement usesStochastic matrix · Forward path product · Ratio product along a path

Proof usesPath products are nonnegative

Used byPath independence of cycle weight · Kolmogorov's cycle theorem, sufficiency

LemmaPaths from positive matrix powers#✓fully proved

Let \(P\) be a stochastic matrix on the states \(\{0, \dots, M\}\). If \(n > 0\) and the \((i, j)\) entry of the \(n\)-th matrix power \(P^n\) is positive, then there is a path from \(i\) to \(j\) (a finite list of states starting at \(i\) and ending at \(j\)) along which the product of the transition probabilities \(P(x, y)\) over consecutive states \(x, y\) is positive.

lemma exists_path_of_matPow_pos (P : StochasticMatrix M) :
    ∀ (n : ℕ) (i j : Fin (M + 1)), 0 < n → 0 < P.matPow n i j →
    ∃ path : List (Fin (M + 1)),
      path.head? = some i ∧ path.getLast? = some j ∧ 0 < listPathProduct P path

Uses 3 · Used by 1

Statement usesStochastic matrix · Forward path product · Matrix powers of a stochastic matrix

Used byIrreducible chains have positive paths

TheoremIrreducible chains have positive paths#✓fully proved

Let \(P\) be an irreducible stochastic matrix on the states \(\{0, \dots, M\}\). For any two states \(i, j\) there is a path from \(i\) to \(j\) (a finite list of states starting at \(i\) and ending at \(j\)) along which the product of the transition probabilities \(P(x, y)\) over consecutive states \(x, y\) is strictly positive.

theorem IsIrreducible.exists_path {P : StochasticMatrix M} (hirr : P.IsIrreducible)
    (i j : Fin (M + 1)) :
    ∃ path : List (Fin (M + 1)),
      path.head? = some i ∧ path.getLast? = some j ∧ 0 < listPathProduct P path

Uses 5 · Used by 4

Statement usesStochastic matrix · Irreducible stochastic matrix · Forward path product

Proof usesPaths from positive matrix powers · Matrix powers of a stochastic matrix

Used byCycle weight · Cycle weights along a positive transition · Path independence of cycle weight · Kolmogorov's cycle theorem, sufficiency

LemmaFirst step of the ratio product#✓fully proved

Let \(P\) be a stochastic matrix, \(n\) a natural number and \(c_0, c_1, \dots, c_{n+1}\) states. Then the ratio product along \(c_0, c_1, \dots, c_{n+1}\) equals \(\frac{P(c_0, c_1)}{P(c_1, c_0)}\) times the ratio product along \(c_1, \dots, c_{n+1}\), where a quotient with denominator \(0\) is taken to be \(0\).

lemma listRatioProduct_cons_ofFn (P : StochasticMatrix M) (n : ℕ)
    (c : Fin (n + 2) → Fin (M + 1)) :
    listRatioProduct P (c 0 :: List.ofFn (fun i : Fin (n + 1) => c i.succ)) =
    (P.prob (c 0) (c 1) / P.prob (c 1) (c 0)) *
    listRatioProduct P (List.ofFn (fun i : Fin (n + 1) => c i.succ))

Uses 2 · Used by 1

Statement usesStochastic matrix · Ratio product along a path

Used byThe ratio product as a finite product

LemmaThe ratio product as a finite product#✓fully proved

Let \(P\) be a stochastic matrix, \(n\) a natural number and \(c_0, c_1, \dots, c_n\) states. Then the ratio product along \(c_0, c_1, \dots, c_n\) equals \(\prod_{i=0}^{n-1} \frac{P(c_i, c_{i+1})}{P(c_{i+1}, c_i)}\), where a quotient with denominator \(0\) is taken to be \(0\).

lemma listRatioProduct_ofFn (P : StochasticMatrix M) :
    ∀ (n : ℕ) (c : Fin (n + 1) → Fin (M + 1)),
    listRatioProduct P (List.ofFn c) =
    ∏ i : Fin n, (P.prob (c i.castSucc) (c i.succ) /
                   P.prob (c i.succ) (c i.castSucc) : ℝ)

Uses 3 · Used by 1

Statement usesStochastic matrix · Ratio product along a path

Proof usesFirst step of the ratio product

Used byThe ratio product around a loop is one

LemmaThe ratio product around a loop is one#✓fully proved

Let \(P\) be a stochastic matrix satisfying Kolmogorov's cycle condition, and let \(x_0, x_1, \dots, x_n\) be a path of states with \(n \ge 1\) and \(x_0 = x_n\) such that \(P(x_{i+1}, x_i) > 0\) for every \(i < n\). Then the ratio product along \(x_0, x_1, \dots, x_n\) equals \(1\).

lemma listRatioProduct_cycle_eq_one (P : StochasticMatrix M)
    (hcycle : P.KolmogorovCycleCondition)
    (path : List (Fin (M + 1))) (hlen : 2 ≤ path.length) (hne : path ≠ [])
    (hloop : path.head hne = path.getLast hne)
    (hpos : ∀ i : Fin (path.length - 1),
      0 < P.prob (path.get ⟨i + 1, by omega⟩) (path.get ⟨i, by omega⟩)) :
    listRatioProduct P path = 1

Uses 4 · Used by 1

Statement usesStochastic matrix · Kolmogorov's cycle condition · Ratio product along a path

Proof usesThe ratio product as a finite product

Used byPath independence of cycle weight

DefinitionCycle weight#✓fully proved

Let \(P\) be an irreducible stochastic matrix on the states \(\{0, \dots, M\}\) and fix a reference state \(i_0\). The cycle weight of a state \(j\) relative to \(i_0\) is the product of the ratios \(P(x, y) / P(y, x)\) over consecutive states \(x, y\) along a path (a finite list of states) from \(i_0\) to \(j\) whose product of transition probabilities \(P(x, y)\) over consecutive states is positive, where a ratio with \(P(y, x) = 0\) counts as \(0\); such a path exists by irreducibility, and one is fixed by choice.

For chains satisfying Kolmogorov's cycle condition this value does not depend on the chosen path, and the weights give a reversible measure.

noncomputable def cycleWeight (P : StochasticMatrix M) (hirr : P.IsIrreducible)
    (i₀ : Fin (M + 1)) (j : Fin (M + 1)) : ℝ :=
  listRatioProduct P (Classical.choose (hirr.exists_path i₀ j))

Uses 5 · Used by 3

Statement usesStochastic matrix · Irreducible stochastic matrix · Irreducible chains have positive paths · Forward path product · Ratio product along a path

Used byDetailed balance for cycle weights · Cycle weights along a positive transition · Kolmogorov's cycle theorem, sufficiency

LemmaRatio product of joined paths#✓fully proved

Let \(P\) be a stochastic matrix and let \(x_0, \dots, x_k\) and \(y_0, \dots, y_l\) be paths of states with \(x_k = y_0\). Then the ratio product along the joined path \(x_0, \dots, x_k, y_1, \dots, y_l\) equals the ratio product along \(x_0, \dots, x_k\) times the ratio product along \(y_0, \dots, y_l\).

lemma listRatioProduct_append (P : StochasticMatrix M) :
    ∀ (l1 l2 : List (Fin (M + 1))) (hne1 : l1 ≠ []) (hne2 : l2 ≠ []),
    l1.getLast hne1 = l2.head hne2 →
    listRatioProduct P (l1 ++ l2.tail) =
      listRatioProduct P l1 * listRatioProduct P l2

Uses 2 · Used by 1

Statement usesStochastic matrix · Ratio product along a path

Used byPath independence of cycle weight

LemmaPositive path products have positive steps#✓fully proved

Let \(P\) be a stochastic matrix on the states \(\{0, \dots, M\}\), and let \(l\) be a path (a finite list of states) whose \(i\)-th state, counting from \(0\), is \(l_i\). If the product of the transition probabilities \(P(x, y)\) over consecutive states \(x, y\) along \(l\) is positive, then \(P(l_i, l_{i+1}) > 0\) for every \(i\) such that \(i + 1\) is less than the length of \(l\).

lemma listPathProduct_pos_implies_transitions (P : StochasticMatrix M)
    (l : List (Fin (M + 1))) (hpos : 0 < listPathProduct P l)
    (i : ℕ) (hi : i + 1 < l.length) :
    0 < P.prob (l.get ⟨i, by omega⟩) (l.get ⟨i + 1, hi⟩)

Uses 3 · Used by 1

Statement usesStochastic matrix · Forward path product

Proof usesPath products are nonnegative

Used byPath independence of cycle weight

LemmaJoining positive paths#✓fully proved

Let \(P\) be a stochastic matrix on the states \(\{0, \dots, M\}\), and let \(l_1, l_2\) be nonempty paths (finite lists of states) such that the last state of \(l_1\) is the first state of \(l_2\). If the products of the transition probabilities \(P(x, y)\) over consecutive states \(x, y\) along \(l_1\) and along \(l_2\) are both positive, then so is the product along the path that follows \(l_1\) and then \(l_2\) with its first state removed.

lemma listPathProduct_append_pos (P : StochasticMatrix M)
    (l1 l2 : List (Fin (M + 1))) (hne1 : l1 ≠ []) (hne2 : l2 ≠ [])
    (hjoin : l1.getLast hne1 = l2.head hne2)
    (h1 : 0 < listPathProduct P l1) (h2 : 0 < listPathProduct P l2) :
    0 < listPathProduct P (l1 ++ l2.tail)

Uses 3 · Used by 2

Statement usesStochastic matrix · Forward path product

Proof usesPath products are nonnegative

Used byCycle weights along a positive transition · Path independence of cycle weight

TheoremPath independence of cycle weight#✓fully proved

Let \(P\) be an irreducible stochastic matrix on the states \(\{0, \dots, M\}\) satisfying Kolmogorov's cycle condition, and let \(i_0, j\) be states. If two paths (finite lists of states) both start at \(i_0\), end at \(j\), and have positive product of the transition probabilities \(P(x, y)\) over consecutive states \(x, y\), then the products of the ratios \(P(x, y) / P(y, x)\) over consecutive states \(x, y\) along the two paths are equal.

This is the key step that makes the cycle weight well-defined and ultimately produces a reversible measure.

theorem cycleWeight_path_independent (P : StochasticMatrix M)
    (hcycle : P.KolmogorovCycleCondition) (hirr : P.IsIrreducible) (i₀ j : Fin (M + 1))
    (path1 path2 : List (Fin (M + 1)))
    (h1 : path1.head? = some i₀) (h1' : path1.getLast? = some j)
    (h2 : path2.head? = some i₀) (h2' : path2.getLast? = some j)
    (hp1 : 0 < listPathProduct P path1) (hp2 : 0 < listPathProduct P path2) :
    listRatioProduct P path1 = listRatioProduct P path2

Uses 11 · Used by 1

Statement usesStochastic matrix · Irreducible stochastic matrix · Kolmogorov's cycle condition · Forward path product · Ratio product along a path

Proof usesIrreducible chains have positive paths · Joining positive paths · Positive path products have positive steps · Ratio product of joined paths · The ratio product around a loop is one · Positive paths have positive ratio product

Used byCycle weights along a positive transition

LemmaRatio product after appending a state#✓fully proved

Let \(P\) be a stochastic matrix, \(x_0, \dots, x_k\) a path of states and \(j\) a state. Then the ratio product along \(x_0, \dots, x_k, j\) equals the ratio product along \(x_0, \dots, x_k\) times \(\frac{P(x_k, j)}{P(j, x_k)}\), where a quotient with denominator \(0\) is taken to be \(0\).

lemma listRatioProduct_snoc (P : StochasticMatrix M) :
    ∀ (path : List (Fin (M + 1))) (j : Fin (M + 1)) (hne : path ≠ []),
    listRatioProduct P (path ++ [j]) =
      listRatioProduct P path *
        (P.prob (path.getLast hne) j /
          P.prob j (path.getLast hne))

Uses 2 · Used by 1

Statement usesStochastic matrix · Ratio product along a path

Used byCycle weights along a positive transition

LemmaCycle weights along a positive transition#✓fully proved

Let \(P\) be an irreducible stochastic matrix on the states \(\{0, \dots, M\}\) satisfying Kolmogorov's cycle condition, fix a reference state \(i_0\), and write \(w(j)\) for the cycle weight of a state \(j\) relative to \(i_0\). If \(i, j\) are states with \(P(i, j) > 0\), then \(w(i) \cdot P(i, j) / P(j, i) = w(j)\).

lemma cycleWeight_extend (P : StochasticMatrix M)
    (hcycle : P.KolmogorovCycleCondition) (hirr : P.IsIrreducible)
    (i₀ i j : Fin (M + 1)) (hPij : 0 < P.prob i j) :
    cycleWeight P hirr i₀ i *
      (P.prob i j / P.prob j i) =
      cycleWeight P hirr i₀ j

Uses 10 · Used by 1

Statement usesStochastic matrix · Irreducible stochastic matrix · Kolmogorov's cycle condition · Cycle weight

Proof usesIrreducible chains have positive paths · Path independence of cycle weight · Forward path product · Joining positive paths · Ratio product along a path · Ratio product after appending a state

Used byDetailed balance for cycle weights

TheoremDetailed balance for cycle weights#✓fully proved

Let \(P\) be an irreducible stochastic matrix on the states \(\{0, \dots, M\}\) satisfying Kolmogorov's cycle condition, fix a reference state \(i_0\), and write \(w(j)\) for the cycle weight of a state \(j\) relative to \(i_0\). Then for all states \(i, j\) we have \(w(i) \cdot P(i, j) = w(j) \cdot P(j, i)\).

theorem cycleWeight_detailed_balance (P : StochasticMatrix M)
    (hcycle : P.KolmogorovCycleCondition) (hirr : P.IsIrreducible)
    (i₀ i j : Fin (M + 1)) :
    cycleWeight P hirr i₀ i * P.prob i j =
    cycleWeight P hirr i₀ j * P.prob j i

Uses 5 · Used by 1

Statement usesStochastic matrix · Irreducible stochastic matrix · Kolmogorov's cycle condition · Cycle weight

Proof usesCycle weights along a positive transition

Used byKolmogorov's cycle theorem, sufficiency

TheoremKolmogorov's cycle theorem, sufficiency#✓fully proved

For an irreducible finite Markov chain satisfying the cycle condition, there exists a reversible measure: a distribution satisfying the detailed balance equations (and hence stationary).

theorem kolmogorov_cycle_sufficiency {M : ℕ} (P : StochasticMatrix M)
    (hirr : P.IsIrreducible) (hcycle : P.KolmogorovCycleCondition) :
    P.IsReversible

Uses 14

Statement usesStochastic matrix · Irreducible stochastic matrix · Reversible stochastic matrix · Kolmogorov's cycle condition

Proof usesDetailed balance · Probability distribution on a finite state space · Irreducible chains have positive paths · Stationary distribution · Cycle weight · Detailed balance for cycle weights · Detailed balance implies stationarity · Forward path product · The ratio product is nonnegative · Positive paths have positive ratio product

31 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.