Dobrushin coefficients

For a matrix B whose columns B(·|j) are probability vectors, as the backward-sampling probabilities B_s(i|j) = B s i j are, the Dobrushin coefficient is β = max_{j, j'} (1/2) ∑_i |B(i|j) - B(i|j')| (Section 4.2 of the paper), the maximal total-variation distance between two columns.

The results are the two bounds of Dobrushin (1956) which are used in the proof of Proposition 2. The coefficient of a product is at most the product of the coefficients. The coefficient is at most 1 - ε if B(i|j) ≥ ε w_i for a probability vector w.

noncomputable def CSMC.dobrushin {ι : Type u_1} [Fintype ι] (B : Matrix ι ι ℝ) : ℝ

The Dobrushin coefficient β = max_{j, j'} (1/2) ∑_i |B(i|j) - B(i|j')| of a matrix B with entries B i j = B(i|j) (Section 4.2).

Equations

• CSMC.dobrushin B = ⨆ (j : ι), ⨆ (j' : ι), (∑ i : ι, |B i j - B i j'|) / 2

theorem CSMC.dobrushin_nonneg {ι : Type u_1} [Fintype ι] (B : Matrix ι ι ℝ) : 0 ≤ dobrushin B

The Dobrushin coefficient is nonnegative.

theorem CSMC.le_dobrushin {ι : Type u_1} [Fintype ι] (B : Matrix ι ι ℝ) (k l : ι) : (∑ i : ι, |B i k - B i l|) / 2 ≤ dobrushin B

Half the total-variation distance between two columns of B is at most the Dobrushin coefficient of B.

theorem CSMC.sum_abs_mulVec_le {ι : Type u_1} [Fintype ι] (B : Matrix ι ι ℝ) {d : ι → ℝ} (hd : ∑ k : ι, d k = 0) : ∑ i : ι, |∑ k : ι, B i k * d k| ≤ dobrushin B * ∑ k : ι, |d k|

If the entries of d sum to zero, then ∑_i |∑_k B(i|k) d_k| ≤ β ∑_k |d_k|, where β is the Dobrushin coefficient of B.

theorem CSMC.dobrushin_mul_le {ι : Type u_1} [Fintype ι] (B : Matrix ι ι ℝ) {B' : Matrix ι ι ℝ} (hB' : ∀ (j : ι), IsProbVector fun (i : ι) => B' i j) : dobrushin (B * B') ≤ dobrushin B * dobrushin B'

The Dobrushin coefficient of a product of matrices is at most the product of their coefficients, when the columns of the second factor are probability vectors.

theorem CSMC.dobrushin_le_one {ι : Type u_1} [Fintype ι] {B : Matrix ι ι ℝ} (hB : ∀ (j : ι), IsProbVector fun (i : ι) => B i j) : dobrushin B ≤ 1

The Dobrushin coefficient of a matrix whose columns are probability vectors is at most one.

theorem CSMC.dobrushin_le_one_sub {ι : Type u_1} [Fintype ι] {B : Matrix ι ι ℝ} {w : ι → ℝ} {ε : ℝ} (hB : ∀ (j : ι), IsProbVector fun (i : ι) => B i j) (hw : IsProbVector w) (h : ∀ (i j : ι), ε * w i ≤ B i j) : dobrushin B ≤ 1 - ε

If B(i|j) ≥ ε w_i for all i and j, where w is a probability vector and the columns of B are probability vectors, then the Dobrushin coefficient of B is at most 1 - ε.