  52variable {ι : Type} [Fintype ι]
  53
  54/-- Turn a strictly positive row‑stochastic real matrix into a MarkovKernel. -/
  55noncomputable def markovOfMatrix (A : Matrix ι ι ℝ)
  56  (hrow : ∀ i, ∑ j, A i j = 1) (hnn : ∀ i j, 0 ≤ A i j) : Dobrushin.MarkovKernel ι :=
  57{ P := fun i j => A i j
  58, nonneg := hnn
  59, rowSum_one := hrow }
  60
  61/-- If all row‑row overlaps are uniformly ≥ β ∈ (0,1], we obtain a TV contraction with α = 1−β. -/
  62theorem tv_contract_of_uniform_overlap {β : ℝ}
  63    (hβpos : 0 < β) (hβle : β ≤ 1) :
  64    Dobrushin.TVContractionMarkov (α := 1 - β) := by
  65  -- special case of tv_contraction_from_overlap_lb applied to `markovOfMatrix A`
  66  exact Dobrushin.tv_contraction_from_overlap_lb hβpos hβle
  67
  68end YM
  69end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.