overlap_le_one
plain-language theorem explainer
Overlap between any two rows of a Markov kernel is at most 1. Researchers deriving Dobrushin contraction coefficients for total variation distance on finite state spaces would cite this bound to control mixing rates. The argument is a direct comparison: each pointwise min is bounded by one row entry, the resulting sums are compared, and the row-sum normalization finishes the inequality.
Claim. Let $K$ be a Markov kernel on a finite set with transition probabilities $P$. Define the overlap as $o(K,i,i') = sum_j min(P(i,j),P(i',j))$. Then $o(K,i,i') leq 1$.
background
MarkovKernel is the minimal structure carrying a nonnegative matrix $P: iota to iota to mathbb{R}$ whose rows each sum to 1. The overlap function is defined directly as the sum of the pointwise minima of any two rows. The lemma sits inside the Dobrushin module, which assembles elementary estimates on these kernels before deriving contraction statements.
proof idea
The term proof first invokes min_le_left to obtain min(P(i,j),P(i',j)) leq P(i,j) for each j. It then applies Finset.sum_le_sum to lift the pointwise bound to the full sum. Finally simpa substitutes the definition of overlap and the rowSum_one hypothesis to reach the desired inequality.
why it matters
The bound supplies the upper end of the interval [0,1] in which overlap lives, a prerequisite for any later lower-bound argument that produces a contraction factor beta in (0,1]. It is the elementary counterpart to the overlap definition and is invoked whenever total-variation contraction is extracted from a uniform overlap lower bound inside the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.