55noncomputable def markovOfMatrix (A : Matrix ι ι ℝ) 56 (hrow : ∀ i, ∑ j, A i j = 1) (hnn : ∀ i j, 0 ≤ A i j) : Dobrushin.MarkovKernel ι :=
proof body
Definition body.
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−β. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.