The forced move

For a probability vector p on a finite set, the forced move F_p of eq. (4) of the paper, the Metropolized Gibbs kernel of Liu (1996), proposes, from i with p i < 1, an index j ≠ i with probability p j / (1 - p i) and accepts it with probability min {1, (1 - p i) / (1 - p j)}, so that F_p(i, j) = p j / max {1 - p i, 1 - p j} for j ≠ i. If p i = 1, then F_p(i, ·) = δ_i.

For a nonnegative vector u, F_u is the forced move with respect to u normalized to sum to one if u ≠ 0, and the identity kernel if u = 0 (Section 2.3).

The main results are the three parts of Lemma 1 of the paper: F_p is reversible with respect to p, F_p(i, j) ≥ p j for i ≠ j, and ⟨φ, F_p φ⟩_p ≤ p(φ) ^ 2.

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

The forced move F_p of eq. (4): for j ≠ i, F_p(i, j) = p j / max {1 - p i, 1 - p j}, F_p(i, i) = 1 - ∑_{j ≠ i} F_p(i, j), and F_p(i, ·) = δ_i if p i = 1.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CSMC.forcedU {ι : Type u_1} [Fintype ι] [DecidableEq ι] (u : ι → ℝ) : Matrix ι ι ℝ

The forced move F_u with respect to a nonnegative vector u (Section 2.3): the forced move with respect to u / (u_1 + ⋯ + u_N) if u ≠ 0, and the identity kernel if u = 0.

Equations

• CSMC.forcedU u = if u = 0 then 1 else CSMC.forced fun (i : ι) => u i / ∑ k : ι, u k

theorem CSMC.forced_apply_of_eq_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ι → ℝ} {i : ι} (hi : p i = 1) (j : ι) : forced p i j = if i = j then 1 else 0

If p i = 1, then F_p(i, ·) = δ_i.

theorem CSMC.forced_apply_of_ne {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ι → ℝ} {i j : ι} (hi : p i ≠ 1) (hij : i ≠ j) : forced p i j = p j / max (1 - p i) (1 - p j)

For p i ≠ 1 and j ≠ i, F_p(i, j) = p j / max {1 - p i, 1 - p j}.

theorem CSMC.forced_apply_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ι → ℝ} {i : ι} (hi : p i ≠ 1) : forced p i i = 1 - ∑ k ∈ Finset.univ.erase i, p k / max (1 - p i) (1 - p k)

For p i ≠ 1, F_p(i, i) = 1 - ∑_{k ≠ i} p k / max {1 - p i, 1 - p k}.

theorem CSMC.le_forced {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ι → ℝ} (hp : IsProbVector p) {i j : ι} (hij : i ≠ j) : p j ≤ forced p i j

Second part of Lemma 1: F_p(i, j) ≥ p j for i ≠ j.

theorem CSMC.forced_mem_rowStochastic {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ι → ℝ} (hp : IsProbVector p) : forced p ∈ Matrix.rowStochastic ℝ ι

The forced move is a Markov kernel.

theorem CSMC.forced_isReversible {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ι → ℝ} (hp : IsProbVector p) : IsReversible p (forced p)

First part of Lemma 1: F_p is reversible with respect to p.

theorem CSMC.dirForm_forced_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ι → ℝ} (hp : IsProbVector p) (φ : ι → ℝ) : dirForm p (forced p) φ ≤ expect p φ ^ 2

Third part of Lemma 1: ⟨φ, F_p φ⟩_p ≤ p(φ) ^ 2.

theorem CSMC.forced_diag_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ι → ℝ} (hp : IsProbVector p) (i : ι) : forced p i i ≤ p i

Under the forced move, the current index is kept with probability at most that under the Gibbs kernel: F_p(i, i) ≤ p i.

theorem CSMC.forcedU_mem_rowStochastic {ι : Type u_1} [Fintype ι] [DecidableEq ι] {u : ι → ℝ} (hu : ∀ (i : ι), 0 ≤ u i) : forcedU u ∈ Matrix.rowStochastic ℝ ι

For a nonnegative vector u, F_u is a Markov kernel.

theorem CSMC.forcedU_isReversible {ι : Type u_1} [Fintype ι] [DecidableEq ι] {u : ι → ℝ} (hu : ∀ (i : ι), 0 ≤ u i) : IsReversible u (forcedU u)

For a nonnegative vector u, u i * F_u(i, j) = u j * F_u(j, i) for all i and j.

theorem CSMC.forced_fin_two_apply_of_ne {p : Fin 2 → ℝ} (hp : IsProbVector p) {i j : Fin 2} (hij : i ≠ j) : forced p i j = p j / max (p j) (p i)

For two indices i ≠ j and a probability vector p, F_p(i, j) = p j / max {p j, p i}.

theorem CSMC.forced_fin_two {p : Fin 2 → ℝ} (hp : IsProbVector p) (h0 : 0 < p 0) (h1 : 0 < p 1) : forced p 0 1 = min 1 (p 1 / p 0)

For N = 2 and p_1, p_2 > 0, F_p(1, 2) = min {1, p_2 / p_1} is the Metropolis acceptance probability (Section 2.2). The indices 1 and 2 of the paper are 0 and 1 in Lean.