The six selection rules

In Section 2.1 of the paper, six choices of the kernels K_T and K_{t,j,j'} of Algorithm 1 are defined in terms of the final weights W = W_T and the backward-sampling probabilities B_t(·|j). In the first five, K_{t,j,j'}(i, ·) = B_t(·|j') for j ≠ j':

• AT: K_T(i, ·) = W and K_{t,j,j}(i, ·) = δ_i (ancestral tracing);
• FM-AT: K_T = F_W and K_{t,j,j}(i, ·) = δ_i (forced move plus ancestral tracing);
• BS: K_T(i, ·) = W and K_{t,j,j}(i, ·) = B_t(·|j) (backward sampling);
• FM-BS: K_T = F_W and K_{t,j,j}(i, ·) = B_t(·|j) (forced move plus backward sampling);
• M-BS: K_T = F_W and K_{t,j,j} = F_{B_t(·|j)} (Metropolized backward sampling);
• CM-BS: K_T = F_W, K_{t,j,j} = F_{B_t(·|j)}, and K_{t,j,j'} = C_{B_t(·|j), B_t(·|j')} for j ≠ j' (coupled Metropolized backward sampling).

Each rule satisfies the hypotheses of Algorithm 1 (Section 3). Under BS and FM-BS, the excess D_{t,j,j'}(φ) is zero. Under M-BS and CM-BS, it is nonpositive, whereas, under AT, it is the variance of φ under B_t(·|j) if j = j' and zero otherwise (Section 4.1).

inductive CSMC.SelectionRule : Type

The six selection rules of Section 2.1.

• AT : SelectionRule

  Ancestral tracing.

• FMAT : SelectionRule

  Forced move plus ancestral tracing.

• BS : SelectionRule

  Backward sampling.

• FMBS : SelectionRule

  Forced move plus backward sampling.

• MBS : SelectionRule

  Metropolized backward sampling.

• CMBS : SelectionRule

  Coupled Metropolized backward sampling.

@[instance_reducible]

instance CSMC.instDecidableEqSelectionRule : DecidableEq SelectionRule

Equations

• CSMC.instDecidableEqSelectionRule x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

noncomputable def CSMC.SelectionRule.finalKernel {ι : Type u_1} [Fintype ι] [DecidableEq ι] (r : SelectionRule) (W : ι → ℝ) : Matrix ι ι ℝ

The kernel K_T of the rule, as a function of the final weights W: the Gibbs kernel for AT and BS, and the forced move F_W for the other rules.

Equations

• CSMC.SelectionRule.AT.finalKernel W = CSMC.gibbs W
• CSMC.SelectionRule.BS.finalKernel W = CSMC.gibbs W
• CSMC.SelectionRule.FMAT.finalKernel W = CSMC.forced W
• CSMC.SelectionRule.FMBS.finalKernel W = CSMC.forced W
• CSMC.SelectionRule.MBS.finalKernel W = CSMC.forced W
• CSMC.SelectionRule.CMBS.finalKernel W = CSMC.forced W

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

The kernel K_{t,j,j} of the rule, as a function of the probability vector p = B_t(·|j): the identity kernel for AT and FM-AT, the Gibbs kernel for BS and FM-BS, and the forced move F_p for M-BS and CM-BS.

Equations

• CSMC.SelectionRule.AT.diagKernel p = 1
• CSMC.SelectionRule.FMAT.diagKernel p = 1
• CSMC.SelectionRule.BS.diagKernel p = CSMC.gibbs p
• CSMC.SelectionRule.FMBS.diagKernel p = CSMC.gibbs p
• CSMC.SelectionRule.MBS.diagKernel p = CSMC.forced p
• CSMC.SelectionRule.CMBS.diagKernel p = CSMC.forced p

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

The kernel K_{t,j,j'}, j ≠ j', of the rule, as a function of p = B_t(·|j) and q = B_t(·|j'): the coupling kernel C_{p,q} for CM-BS, and the Gibbs kernel K(i, ·) = q for the other rules.

Equations

• CSMC.SelectionRule.CMBS.offDiagKernel p q = CSMC.coupling p q
• CSMC.SelectionRule.AT.offDiagKernel p q = CSMC.gibbs q
• CSMC.SelectionRule.FMAT.offDiagKernel p q = CSMC.gibbs q
• CSMC.SelectionRule.BS.offDiagKernel p q = CSMC.gibbs q
• CSMC.SelectionRule.FMBS.offDiagKernel p q = CSMC.gibbs q
• CSMC.SelectionRule.MBS.offDiagKernel p q = CSMC.gibbs q

noncomputable def CSMC.SelectionRule.kernels {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} (r : SelectionRule) (W : ι → ℝ) (B : Fin n → Matrix ι ι ℝ) : BackwardKernels ι n

The kernels of the rule, given the final weights W and the backward-sampling probabilities B.

Equations

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

theorem CSMC.SelectionRule.kernels_final {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} (r : SelectionRule) (W : ι → ℝ) (B : Fin n → Matrix ι ι ℝ) : (r.kernels W B).final = r.finalKernel W

The kernel K_T of the rule.

theorem CSMC.SelectionRule.kernels_step {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} (r : SelectionRule) (W : ι → ℝ) (B : Fin n → Matrix ι ι ℝ) (s : Fin n) (j j' : ι) : (r.kernels W B).step s j j' = if j = j' then r.diagKernel fun (i : ι) => B s i j else r.offDiagKernel (fun (i : ι) => B s i j) fun (i : ι) => B s i j'

The kernels K_{t,j,j'} of the rule.

theorem CSMC.SelectionRule.kernels_step_self {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} (r : SelectionRule) (W : ι → ℝ) (B : Fin n → Matrix ι ι ℝ) (s : Fin n) (j : ι) : (r.kernels W B).step s j j = r.diagKernel fun (i : ι) => B s i j

The kernel K_{t,j,j} of the rule is diagKernel at B_t(·|j).

theorem CSMC.SelectionRule.kernels_step_of_ne {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} {r : SelectionRule} (hr : r ≠ CMBS) (W : ι → ℝ) (B : Fin n → Matrix ι ι ℝ) (s : Fin n) {j j' : ι} (h : j ≠ j') : (r.kernels W B).step s j j' = gibbs fun (i : ι) => B s i j'

For j ≠ j' and the rules other than CM-BS, K_{t,j,j'}(i, ·) = B_t(·|j').

theorem CSMC.SelectionRule.kernels_step_eq_gibbs {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} {r : SelectionRule} (hr : r = BS ∨ r = FMBS) (W : ι → ℝ) (B : Fin n → Matrix ι ι ℝ) (s : Fin n) (j j' : ι) : (r.kernels W B).step s j j' = gibbs fun (i : ι) => B s i j'

For BS and FM-BS, K_{t,j,j'}(i, ·) = B_t(·|j') for all j and j'.

theorem CSMC.SelectionRule.diagKernel_mem_isReversible {ι : Type u_1} [Fintype ι] [DecidableEq ι] (r : SelectionRule) {p : ι → ℝ} (hp : IsProbVector p) : r.diagKernel p ∈ Matrix.rowStochastic ℝ ι ∧ IsReversible p (r.diagKernel p)

The kernel K_{t,j,j} of each rule is a Markov kernel reversible with respect to p = B_t(·|j).

theorem CSMC.SelectionRule.admissible {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} (r : SelectionRule) {W : ι → ℝ} {B : Fin n → Matrix ι ι ℝ} (hW : IsProbVector W) (hB : ∀ (s : Fin n) (j : ι), IsProbVector fun (i : ι) => B s i j) : Admissible W B (r.kernels W B)

Each of the six rules satisfies the hypotheses of Algorithm 1 (Section 3).

theorem CSMC.SelectionRule.excess_eq_zero {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} {r : SelectionRule} (hr : r = BS ∨ r = FMBS) (W : ι → ℝ) (B : Fin n → Matrix ι ι ℝ) (s : Fin n) (j j' : ι) (φ : ι → ℝ) : excess B (r.kernels W B) s j j' φ = 0

For BS and FM-BS, D_{t,j,j'}(φ) = 0 (Section 4.1).

theorem CSMC.SelectionRule.excess_AT {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} (W : ι → ℝ) (B : Fin n → Matrix ι ι ℝ) (s : Fin n) (j j' : ι) (φ : ι → ℝ) : excess B (AT.kernels W B) s j j' φ = if j = j' then expect (fun (i : ι) => B s i j) (φ ^ 2) - expect (fun (i : ι) => B s i j) φ ^ 2 else 0

For AT, D_{t,j,j'}(φ) is the variance of φ under B_t(·|j) if j = j' and zero otherwise (Section 4.1).

theorem CSMC.SelectionRule.excess_nonpos {ι : Type u_1} [Fintype ι] [DecidableEq ι] {n : ℕ} {r : SelectionRule} (hr : r = MBS ∨ r = CMBS) (W : ι → ℝ) {B : Fin n → Matrix ι ι ℝ} (hB : ∀ (s : Fin n) (j : ι), IsProbVector fun (i : ι) => B s i j) (s : Fin n) (j j' : ι) (φ : ι → ℝ) : excess B (r.kernels W B) s j j' φ ≤ 0

For M-BS and CM-BS, D_{t,j,j'}(φ) ≤ 0 (Section 4.1).