def StochasticMatrix.matPow {M : ℕ} (P : StochasticMatrix M) : ℕ → Fin (M + 1) → Fin (M + 1) → ℝ

The n-th matrix power of a stochastic transition matrix P. Entry (i,j) represents the probability of moving from state i to state j in exactly n steps.

def StochasticMatrix.IsIrreducible {M : ℕ} (P : StochasticMatrix M) : Prop

A stochastic matrix P is irreducible if for every pair of states i, j there is some positive number of steps n such that P^n i j > 0; i.e., every state is reachable from every other state in finitely many steps.

structure StochasticMatrix.Distribution (M : ℕ) : Type

A probability distribution on the finite state space Fin (M + 1): a function val : Fin (M + 1) → ℝ whose values are nonnegative and sum to 1.

• val : Fin (M + 1) → ℝ
• nonneg (i : Fin (M + 1)) : 0 ≤ self.val i
• sum_one : ∑ i : Fin (M + 1), self.val i = 1

def StochasticMatrix.IsStationary {M : ℕ} (P : StochasticMatrix M) (π : Distribution M) : Prop

A distribution π is stationary for the transition matrix P if π P = π, i.e., ∑ᵢ π(i) P(i, j) = π(j) for every state j.

def StochasticMatrix.DetailedBalance {M : ℕ} (P : StochasticMatrix M) (π : Distribution M) : Prop

The detailed balance (reversibility) equations between P and π: π(i) P(i,j) = π(j) P(j,i) for all states i, j.

def StochasticMatrix.IsReversible {M : ℕ} (P : StochasticMatrix M) : Prop

A transition matrix P is reversible if there exists a distribution π that is both stationary and satisfies the detailed balance equations with P.

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

If π satisfies detailed balance with P, then π is stationary for P. Detailed balance is a strictly stronger condition than stationarity.

def StochasticMatrix.pathProduct {M : ℕ} (P : StochasticMatrix M) : List (Fin (M + 1)) → ℝ

The product of transition probabilities along a path: for a list of states [x₀, x₁, …, x_k], returns ∏ᵢ P(xᵢ, xᵢ₊₁). Empty and singleton lists give 1.

structure StochasticMatrix.KolmogorovCycleCondition {M : ℕ} (P : StochasticMatrix M) : Prop

Kolmogorov's cycle condition on a stochastic matrix P: (1) symm_support: P(x, y) > 0 implies P(y, x) > 0; and (2) cycle_prod: for any loop x₀, x₁, …, xₙ = x₀ whose reverse path has positive probability, the product of forward transition probabilities along the loop equals the product of backward transition probabilities. This is the necessary and sufficient condition for the existence of a reversible measure for an irreducible chain.

• 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)

theorem StochasticMatrix.matPow_nonneg {M : ℕ} (P : StochasticMatrix M) (n : ℕ) (i j : Fin (M + 1)) : 0 ≤ P.matPow n i j

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

theorem StochasticMatrix.distribution_pos_of_irreducible_detailedBalance {M : ℕ} (P : StochasticMatrix M) (π : Distribution M) (hirr : P.IsIrreducible) (hdb : P.DetailedBalance π) (i : Fin (M + 1)) : 0 < π.val i

For an irreducible chain P, any distribution π satisfying detailed balance must assign strictly positive mass to every state.

theorem StochasticMatrix.prod_castSucc_eq_prod_succ {n M : ℕ} (f : Fin (M + 1) → ℝ) (c : Fin (n + 1) → Fin (M + 1)) (hcycle : c 0 = c (Fin.last n)) : ∏ i : Fin n, f (c i.castSucc) = ∏ i : Fin n, f (c i.succ)

Helper lemma: along a loop c : Fin (n + 1) → Fin (M + 1) with c 0 = c (Fin.last n), the product ∏ i, f (c (i.castSucc)) equals the shifted product ∏ i, f (c (i.succ)). This is a telescoping/cyclic rearrangement of products.

noncomputable def StochasticMatrix.listPathProduct {M : ℕ} (P : StochasticMatrix M) : List (Fin (M + 1)) → NNReal

NNReal-valued version of pathProduct: the product of forward transition probabilities along the path, packaged as a nonnegative real.

noncomputable def StochasticMatrix.listRatioProduct {M : ℕ} (P : StochasticMatrix M) : List (Fin (M + 1)) → NNReal

The product of ratios P(xᵢ, xᵢ₊₁) / P(xᵢ₊₁, xᵢ) along a path. This is the quantity that defines the "cycle weight" used to construct a reversible measure from Kolmogorov's cycle condition.

theorem StochasticMatrix.listRatioProduct_pos_of_listPathProduct_pos {M : ℕ} (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 < P.listPathProduct path) : 0 < P.listRatioProduct path

If the forward listPathProduct along a path is positive and the transition probabilities have symmetric support, then the corresponding listRatioProduct is also positive.

theorem StochasticMatrix.exists_path_of_matPow_pos {M : ℕ} (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 < P.listPathProduct path

If P.matPow n i j > 0, then there is an actual path from i to j (a list of states starting at i and ending at j) along which the product of transition probabilities is positive.

theorem StochasticMatrix.IsIrreducible.exists_path {M : ℕ} {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 < P.listPathProduct path

For an irreducible chain, between any two states i, j there exists a finite path from i to j along which the product of transition probabilities is strictly positive.

theorem StochasticMatrix.IsIrreducible.exists_path_ratio {M : ℕ} {P : StochasticMatrix M} (hirr : P.IsIrreducible) (hsymm : ∀ (x y : Fin (M + 1)), P.prob x y > 0 → P.prob y x > 0) (i j : Fin (M + 1)) : ∃ (path : List (Fin (M + 1))), path.head? = some i ∧ path.getLast? = some j ∧ 0 < P.listRatioProduct path

Variant of IsIrreducible.exists_path: under symmetric support, there also exists a path from i to j along which the listRatioProduct is positive.

theorem StochasticMatrix.listRatioProduct_cons_ofFn {M : ℕ} (P : StochasticMatrix M) (n : ℕ) (c : Fin (n + 2) → Fin (M + 1)) : P.listRatioProduct (c 0 :: List.ofFn fun (i : Fin (n + 1)) => c i.succ) = ⟨P.prob (c 0) (c 1), ⋯⟩ / ⟨P.prob (c 1) (c 0), ⋯⟩ * P.listRatioProduct (List.ofFn fun (i : Fin (n + 1)) => c i.succ)

Unfolding of listRatioProduct on a list of the form c 0 :: List.ofFn (c ∘ Fin.succ).

theorem StochasticMatrix.listRatioProduct_ofFn {M : ℕ} (P : StochasticMatrix M) (n : ℕ) (c : Fin (n + 1) → Fin (M + 1)) : P.listRatioProduct (List.ofFn c) = ∏ i : Fin n, ⟨P.prob (c i.castSucc) (c i.succ), ⋯⟩ / ⟨P.prob (c i.succ) (c i.castSucc), ⋯⟩

listRatioProduct along List.ofFn c is the finite product of ratios P(c iₖ, c iₖ₊₁) / P(c iₖ₊₁, c iₖ) indexed by i : Fin n.

theorem StochasticMatrix.listRatioProduct_cycle_eq_one {M : ℕ} (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, ⋯⟩) (path.get ⟨↑i, ⋯⟩)) : P.listRatioProduct path = 1

Under Kolmogorov's cycle condition, the ratio product along any closed loop (a path whose first and last elements coincide and whose reverse edges all have positive probability) is equal to 1.

noncomputable def StochasticMatrix.cycleWeight {M : ℕ} (P : StochasticMatrix M) (hirr : P.IsIrreducible) (i₀ j : Fin (M + 1)) : NNReal

The cycle weight of state j relative to a reference state i₀: defined as the listRatioProduct along some (classically chosen) positive-probability path from i₀ to j. For chains satisfying Kolmogorov's cycle condition this value is path-independent (cycleWeight_path_independent) and yields the unique-up-to-scaling reversible measure.

theorem StochasticMatrix.listRatioProduct_append {M : ℕ} (P : StochasticMatrix M) (l1 l2 : List (Fin (M + 1))) (hne1 : l1 ≠ []) (hne2 : l2 ≠ []) : l1.getLast hne1 = l2.head hne2 → P.listRatioProduct (l1 ++ l2.tail) = P.listRatioProduct l1 * P.listRatioProduct l2

listRatioProduct is multiplicative when concatenating two paths that share an endpoint: joining l1 with l2.tail (so the join point isn't duplicated) gives the product of the ratio products of l1 and l2.

theorem StochasticMatrix.listPathProduct_pos_implies_transitions {M : ℕ} (P : StochasticMatrix M) (l : List (Fin (M + 1))) (hpos : 0 < P.listPathProduct l) (i : ℕ) (hi : i + 1 < l.length) : 0 < P.prob (l.get ⟨i, ⋯⟩) (l.get ⟨i + 1, hi⟩)

If the path product along a list l is positive, then every consecutive transition probability P(l[i], l[i+1]) along l is positive.

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

If two paths l1, l2 each have positive path product and share an endpoint, then their join l1 ++ l2.tail also has positive path product.

theorem StochasticMatrix.cycleWeight_path_independent {M : ℕ} (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 < P.listPathProduct path1) (hp2 : 0 < P.listPathProduct path2) : P.listRatioProduct path1 = P.listRatioProduct path2

Path independence of cycle weight. Under Kolmogorov's cycle condition, any two positive-probability paths from i₀ to j yield the same listRatioProduct. This is the key step that makes cycleWeight well-defined and ultimately produces a reversible measure.

theorem StochasticMatrix.listRatioProduct_snoc {M : ℕ} (P : StochasticMatrix M) (path : List (Fin (M + 1))) (j : Fin (M + 1)) (hne : path ≠ []) : P.listRatioProduct (path ++ [j]) = P.listRatioProduct path * (⟨P.prob (path.getLast hne) j, ⋯⟩ / ⟨P.prob j (path.getLast hne), ⋯⟩)

Recursion for listRatioProduct when appending a single state j at the end of a nonempty path: the new ratio product equals the old one times the ratio for the new edge.

theorem StochasticMatrix.cycleWeight_extend {M : ℕ} (P : StochasticMatrix M) (hcycle : P.KolmogorovCycleCondition) (hirr : P.IsIrreducible) (i₀ i j : Fin (M + 1)) (hPij : 0 < P.prob i j) : P.cycleWeight hirr i₀ i * (⟨P.prob i j, ⋯⟩ / ⟨P.prob j i, ⋯⟩) = P.cycleWeight hirr i₀ j

Extending the path by one positive-probability transition i → j multiplies the cycle weight by P(i,j) / P(j,i). Equivalently, cycleWeight i₀ j = cycleWeight i₀ i · P(i,j)/P(j,i) whenever P(i,j) > 0.

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

The cycle weights satisfy the detailed balance equations with P: cycleWeight(i) · P(i,j) = cycleWeight(j) · P(j,i) for all states i, j.

theorem StochasticMatrix.kolmogorov_cycle_theorem {M : ℕ} (P : StochasticMatrix M) (hirr : P.IsIrreducible) : P.IsReversible ↔ P.KolmogorovCycleCondition

Kolmogorov's cycle theorem. For an irreducible finite Markov chain with transition matrix P, there exists a reversible measure (i.e., P.IsReversible) if and only if P satisfies the Kolmogorov cycle condition: (1) P(x,y) > 0 implies P(y,x) > 0; and (2) for any loop x₀, x₁, …, xₙ with ∏ P(xᵢ, xᵢ₋₁) > 0, we have ∏ (P(xᵢ₋₁, xᵢ) / P(xᵢ, xᵢ₋₁)) = 1.