MarkovKernel

formal source

   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