row
plain-language theorem explainer
The row function extracts the i-th row of the transition matrix P from a MarkovKernel as a map from states to probabilities. Analysts working on Dobrushin coefficients or Markov chain contractions cite this accessor to isolate individual distributions. It is realized as a direct field projection with a simp attribute.
Claim. Let $K$ be a Markov kernel on a finite set $ι$. Then row$(K,i)$ denotes the function $j ↦ K.P(i,j)$, where $K.P$ is the transition matrix.
background
MarkovKernel is a structure on a finite type $ι$ consisting of a matrix $P:ι→ι→ℝ$ together with proofs that all entries are nonnegative and that each row sums to one. This minimal interface supports overlap computations that quantify similarity between rows. The row definition supplies direct access to any single row of $P$ for use in downstream overlap and contraction arguments.
proof idea
One-line definition that projects onto the P field of the MarkovKernel structure and curries the result to a function of the second index.
why it matters
The definition is referenced by 27 downstream declarations, including nine_is_D_sq establishing $9=D^2$ and normal-form aggregation lemmas. It supplies the basic row extractor required by the Dobrushin overlap construction, which in turn supports contraction estimates aligned with the Recognition Composition Law and the derivation of spatial dimension $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.