IndisputableMonolith.YM.Dobrushin

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace YM
   5namespace Dobrushin
   6
   7open scoped BigOperators
   8
   9variable {ι : Type} [Fintype ι]
  10
  11/-- Minimal Markov kernel interface for overlap computations. -/
  12structure MarkovKernel (ι : Type) [Fintype ι] where
  13  P : ι → ι → ℝ
  14  nonneg : ∀ i j, 0 ≤ P i j
  15  rowSum_one : ∀ i, ∑ j, P i j = 1
  16
  17@[simp] def row (K : MarkovKernel ι) (i : ι) : ι → ℝ := fun j => K.P i j
  18
  19/-- Row–row overlap `∑j min(P i j, P i' j)` in [0,1]. -/
  20def overlap (K : MarkovKernel ι) (i i' : ι) : ℝ := ∑ j, min (K.P i j) (K.P i' j)
  21
  22lemma overlap_nonneg (K : MarkovKernel ι) (i i' : ι) : 0 ≤ overlap K i i' := by
  23  classical
  24  have hterm : ∀ j : ι, 0 ≤ min (K.P i j) (K.P i' j) :=
  25    fun j => min_nonneg (K.nonneg i j) (K.nonneg i' j)
  26  have hsum : 0 ≤ ∑ j in Finset.univ, min (K.P i j) (K.P i' j) :=
  27    Finset.sum_nonneg (by intro j _; exact hterm j)
  28  simpa [overlap] using hsum
  29
  30lemma overlap_le_one (K : MarkovKernel ι) (i i' : ι) : overlap K i i' ≤ 1 := by
  31  classical
  32  have hpoint : ∀ j : ι, min (K.P i j) (K.P i' j) ≤ K.P i j :=
  33    fun j => min_le_left _ _
  34  have hsum : (∑ j in Finset.univ, min (K.P i j) (K.P i' j)) ≤ ∑ j in Finset.univ, K.P i j :=
  35    Finset.sum_le_sum (by intro j _; exact hpoint j)
  36  simpa [overlap, K.rowSum_one i] using hsum
  37
  38/-- TV contraction certificate from uniform overlap lower bound β ∈ (0,1]. -/
  39def TVContractionMarkov (α : ℝ) : Prop := (0 ≤ α) ∧ (α < 1)
  40
  41theorem tv_contraction_from_overlap_lb {β : ℝ}
  42    (hβpos : 0 < β) (hβle : β ≤ 1) : TVContractionMarkov (α := 1 - β) := by
  43  constructor <;> linarith
  44
  45end Dobrushin
  46end YM
  47
  48namespace YM
  49
  50open YM.Dobrushin
  51
  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
  70