structure StochasticMatrix (M : ℕ) : Type

A StochasticMatrix M is an (M+1) × (M+1) row-stochastic matrix: entries prob i j are non-negative real numbers, and the rows sum to 1. This is the transition matrix of a Markov chain on the finite state space Fin (M + 1).

• prob : Fin (M + 1) → Fin (M + 1) → ℝ
• nonneg (i j : Fin (M + 1)) : 0 ≤ self.prob i j
• row_sum (i : Fin (M + 1)) : ∑ j : Fin (M + 1), self.prob i j = 1

structure IsFiniteMarkovChain {Ω : Type u_1} {m : MeasurableSpace Ω} {M : ℕ} (X : ℕ → Ω → Fin (M + 1)) (P : StochasticMatrix M) (ℱ : DiscreteFiltration Ω m) (μ : MeasureTheory.Measure Ω) : Prop

IsFiniteMarkovChain X P ℱ μ asserts that the sequence X : ℕ → Ω → Fin (M+1) is a Markov chain with transition matrix P, adapted to the discrete filtration ℱ, under the measure μ. Concretely: each X n is ℱ n-measurable, and the conditional probability that X (n+1) = j given ℱ n equals P.prob (X n) j, matching the Markov property P(X_{n+1} = j | X_n = i, ...) = P_{ij}.

• adapted (n : ℕ) : Measurable (X n)
• markov_prop (n : ℕ) (j : Fin (M + 1)) : μ[fun (ω : Ω) => if X (n + 1) ω = j then 1 else 0 | ↑ℱ n] =ᵐ[μ] fun (ω : Ω) => P.prob (X n ω) j