markovOfMatrix
plain-language theorem explainer
markovOfMatrix converts an explicit row-stochastic non-negative matrix into the MarkovKernel record required for overlap and total-variation calculations. Researchers deriving Dobrushin contraction bounds for finite Markov chains cite the construction when they start from a concrete transition matrix rather than an abstract kernel. The definition is a direct record constructor that copies the matrix entries and attaches the supplied row-sum and non-negativity hypotheses.
Claim. Let $A$ be an $ι×ι$ matrix with real entries such that each row sums to 1 and every entry is non-negative. Then $A$ determines a Markov kernel $P$ on the finite set $ι$ by the rule $P(i,j):=A(i,j)$.
background
MarkovKernel is the minimal structure needed for overlap computations inside the Dobrushin module. It consists of a transition map $P:ι→ι→ℝ$ together with proofs that all entries are non-negative and that every row sums to one. The present definition supplies a concrete instance of this structure directly from an ordinary matrix. The surrounding module imports establish the basic overlap and total-variation machinery that will be applied to any kernel built this way.
proof idea
The definition is a one-line wrapper that applies the MarkovKernel constructor, supplying the matrix entries as the transition map $P$ and using the hypotheses hrow and hnn directly as the rowSum_one and nonneg fields.
why it matters
This definition supplies the concrete Markov kernels required by tv_contract_of_uniform_overlap, which produces the total-variation contraction factor $1-β$ whenever row overlaps are bounded below by $β$. In the Recognition Science setting it provides the interface between explicit transition matrices and the abstract contraction machinery used for mixing-time estimates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.