The coupling kernel

For probability vectors p and q on a finite set, under the kernel C_{p,q} of eq. (5) of the paper, an index is drawn from q and replaced, if it equals the current index i, by a forced move from i with respect to the probabilities proportional to p j * q j: C_{p,q}(i, ·) = q + q i * (F_{p ⊙ q}(i, ·) - δ_i), where p ⊙ q is the entrywise product, which is p * q in Lean.

The main results are the three parts of Lemma 2 of the paper: p i * C_{p,q}(i, i') = q i' * C_{q,p}(i', i), C_{p,q}(i, i') ≥ q i' for i ≠ i', and ⟨φ, C_{p,q} φ⟩_p ≤ p(φ) q(φ). The identity C_{p,p} = F_p for two indices (Section 4.3) is also proved.

noncomputable def CSMC.coupling {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p q : ι → ℝ) : Matrix ι ι ℝ

The coupling kernel C_{p,q} of eq. (5): C_{p,q}(i, i') = q i' + q i * (F_{p ⊙ q}(i, i') - δ_i(i')).

Equations

• CSMC.coupling p q = Matrix.of fun (i i' : ι) => q i' + q i * (CSMC.forcedU (p * q) i i' - 1 i i')

theorem CSMC.coupling_diag {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p q : ι → ℝ) (i : ι) : coupling p q i i = q i * forcedU (p * q) i i

The diagonal of the coupling kernel: C_{p,q}(i, i) = q i * F_{p ⊙ q}(i, i).

theorem CSMC.coupling_apply_of_ne {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p q : ι → ℝ) {i i' : ι} (hii' : i ≠ i') : coupling p q i i' = q i' + q i * forcedU (p * q) i i'

Off the diagonal, C_{p,q}(i, i') = q i' + q i * F_{p ⊙ q}(i, i').

theorem CSMC.coupling_mem_rowStochastic {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p q : ι → ℝ} (hp : IsProbVector p) (hq : IsProbVector q) : coupling p q ∈ Matrix.rowStochastic ℝ ι

The coupling kernel is a Markov kernel.

theorem CSMC.coupling_symm {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p q : ι → ℝ} (hp : IsProbVector p) (hq : IsProbVector q) (i i' : ι) : p i * coupling p q i i' = q i' * coupling q p i' i

First part of Lemma 2: p i * C_{p,q}(i, i') = q i' * C_{q,p}(i', i).

theorem CSMC.le_coupling {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p q : ι → ℝ} (hp : IsProbVector p) (hq : IsProbVector q) {i i' : ι} (hii' : i ≠ i') : q i' ≤ coupling p q i i'

Second part of Lemma 2: C_{p,q}(i, i') ≥ q i' for i ≠ i'.

theorem CSMC.dirForm_coupling_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p q : ι → ℝ} (hp : IsProbVector p) (hq : IsProbVector q) (φ : ι → ℝ) : dirForm p (coupling p q) φ ≤ expect p φ * expect q φ

Third part of Lemma 2: ⟨φ, C_{p,q} φ⟩_p ≤ p(φ) q(φ).

theorem CSMC.coupling_self_fin_two {p : Fin 2 → ℝ} (hp : IsProbVector p) : coupling p p = forced p

With two indices, C_{p,p} = F_p for every probability vector p (Section 4.3).