TVContractionMarkov
plain-language theorem explainer
TVContractionMarkov α asserts that the real number α lies in the half-open interval [0,1). Analysts deriving Dobrushin-type total variation bounds for Markov kernels cite this predicate when a uniform row overlap lower bound β ∈ (0,1] produces the contraction factor α = 1 - β. The declaration is a direct definition of the admissible contraction coefficients.
Claim. Let α ∈ ℝ. The predicate TVContractionMarkov(α) holds if and only if 0 ≤ α < 1. This interval condition serves as the certificate that α = 1 - β yields a total variation contraction whenever the minimal row overlap satisfies β ∈ (0,1].
background
The Dobrushin module works with Markov kernels represented as row-stochastic matrices on finite state spaces. The overlap function records the minimal agreement between any two rows, while row extracts the probability vectors. TVContractionMarkov isolates the numerical restriction on the contraction rate α that follows from a positive lower bound on these overlaps.
proof idea
This declaration is a definition that directly encodes the conjunction (0 ≤ α) ∧ (α < 1). No lemmas or tactics are invoked; the predicate is introduced solely to be instantiated by the two downstream theorems.
why it matters
The predicate is the target of tv_contraction_from_overlap_lb and tv_contract_of_uniform_overlap, which establish that any uniform overlap β ∈ (0,1] produces a valid TV contraction with factor 1 - β. It supplies the contraction certificate inside the YM.Dobrushin development, supporting mixing-time or uniqueness arguments that connect to the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.