module module

`IndisputableMonolith.YM.Dobrushin`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

declarations in this module (9)

structure MarkovKernel L12
def row L17
def overlap L20
lemma overlap_nonneg L22
lemma overlap_le_one L30
def TVContractionMarkov L39
theorem tv_contraction_from_overlap_lb L41
def markovOfMatrix L55
theorem tv_contract_of_uniform_overlap L62