Comparison of quadratic forms

For a Markov kernel K which maps the probability vector p to q, that is, ∑ i, p i * K i j = q j for every j, the difference ⟨φ, K φ⟩_p - p(φ) q(φ) is a sum over pairs of indices of p i * (K i j - q j) times -(φ i - φ j) ^ 2 / 2. If K i j ≥ q j for i ≠ j, the difference is therefore nonpositive. The third parts of Lemmas 1 and 2 of the paper follow in this way from their second parts.

Lemma 3 of Tierney (1998) is also proved for finite index sets: of two Markov kernels which are reversible with respect to p, the one with the larger off-diagonal entries has the smaller quadratic form.

theorem CSMC.sum_sum_mul_sub_sq {ι : Type u_1} [Fintype ι] (c : ι → ι → ℝ) (φ : ι → ℝ) : ∑ i : ι, ∑ j : ι, c i j * (φ i - φ j) ^ 2 = ∑ i : ι, (∑ j : ι, c i j) * φ i ^ 2 + ∑ j : ι, (∑ i : ι, c i j) * φ j ^ 2 - 2 * ∑ i : ι, ∑ j : ι, c i j * φ i * φ j

For coefficients c i j, the sum ∑ i, ∑ j, c i j * (φ i - φ j) ^ 2 is ∑ i, (∑ j, c i j) * φ i ^ 2 + ∑ j, (∑ i, c i j) * φ j ^ 2 - 2 * ∑ i, ∑ j, c i j * φ i * φ j.

theorem CSMC.dirForm_sub_expect_mul_expect {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p q : ι → ℝ} {K : Matrix ι ι ℝ} (hp : IsProbVector p) (hK : K ∈ Matrix.rowStochastic ℝ ι) (hpK : ∀ (j : ι), ∑ i : ι, p i * K i j = q j) (φ : ι → ℝ) : dirForm p K φ - expect p φ * expect q φ = (-∑ i : ι, ∑ j : ι, p i * (K i j - q j) * (φ i - φ j) ^ 2) / 2

If K is a Markov kernel and ∑ i, p i * K i j = q j for every j, then ⟨φ, K φ⟩_p - p(φ) q(φ) = -(∑ i, ∑ j, p i * (K i j - q j) * (φ i - φ j) ^ 2) / 2.

theorem CSMC.dirForm_le_of_offDiag {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p q : ι → ℝ} {K : Matrix ι ι ℝ} (hp : IsProbVector p) (hK : K ∈ Matrix.rowStochastic ℝ ι) (hpK : ∀ (j : ι), ∑ i : ι, p i * K i j = q j) (hoff : ∀ (i j : ι), i ≠ j → q j ≤ K i j) (φ : ι → ℝ) : dirForm p K φ ≤ expect p φ * expect q φ

If K is a Markov kernel, ∑ i, p i * K i j = q j for every j, and K i j ≥ q j for i ≠ j, then ⟨φ, K φ⟩_p ≤ p(φ) q(φ).

theorem CSMC.dirForm_eq_of_isReversible {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ι → ℝ} {K : Matrix ι ι ℝ} (hK : K ∈ Matrix.rowStochastic ℝ ι) (hrev : IsReversible p K) (φ : ι → ℝ) : dirForm p K φ = ∑ i : ι, p i * φ i ^ 2 - (∑ i : ι, ∑ j : ι, p i * K i j * (φ i - φ j) ^ 2) / 2

For a Markov kernel K reversible with respect to p, ⟨φ, K φ⟩_p = ∑_i p_i φ(i) ^ 2 - (∑_{i, j} p_i K(i, j) (φ(i) - φ(j)) ^ 2) / 2.

theorem CSMC.tierney_lemma3 {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ι → ℝ} {K₁ K₂ : Matrix ι ι ℝ} (hp : ∀ (i : ι), 0 ≤ p i) (hK₁ : K₁ ∈ Matrix.rowStochastic ℝ ι) (hK₂ : K₂ ∈ Matrix.rowStochastic ℝ ι) (h₁ : IsReversible p K₁) (h₂ : IsReversible p K₂) (hoff : ∀ (i j : ι), i ≠ j → K₂ i j ≤ K₁ i j) (φ : ι → ℝ) : dirForm p K₁ φ ≤ dirForm p K₂ φ

Lemma 3 of Tierney (1998), for a finite index set: if the Markov kernels K₁ and K₂ are reversible with respect to p and K₂ i j ≤ K₁ i j for i ≠ j, then ⟨φ, K₁ φ⟩_p ≤ ⟨φ, K₂ φ⟩_p.

theorem CSMC.expect_sq_sub_dirForm_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ι → ℝ} {K : Matrix ι ι ℝ} (hp : IsProbVector p) (hK : K ∈ Matrix.rowStochastic ℝ ι) (hrev : IsReversible p K) (φ : ι → ℝ) : expect p φ ^ 2 - dirForm p K φ ≤ expect p (φ ^ 2) - expect p φ ^ 2

For a Markov kernel K reversible with respect to a probability vector p, p(φ) ^ 2 - ⟨φ, K φ⟩_p ≤ p(φ ^ 2) - p(φ) ^ 2: minus the lag-one autocovariance of φ is at most its variance.

theorem CSMC.le_one_of_mem_rowStochastic {ι : Type u_1} [Fintype ι] [DecidableEq ι] {K : Matrix ι ι ℝ} (hK : K ∈ Matrix.rowStochastic ℝ ι) (i j : ι) : K i j ≤ 1

The entries of a Markov kernel are at most one.

theorem CSMC.dirForm_indicator {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ι → ℝ) (K : Matrix ι ι ℝ) (i : ι) : (dirForm p K fun (k : ι) => if k = i then 1 else 0) = p i * K i i

The quadratic form at the indicator of {i} is ⟨1_{i}, K 1_{i}⟩_p = p i * K i i.

theorem CSMC.gibbs_isReversible {ι : Type u_1} (p : ι → ℝ) : IsReversible p (gibbs p)

The Gibbs kernel K(i, ·) = p is reversible with respect to p.

theorem CSMC.one_isReversible {ι : Type u_1} [DecidableEq ι] (p : ι → ℝ) : IsReversible p 1

The identity kernel is reversible with respect to every vector.

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

For a probability vector p, the Gibbs kernel K(i, ·) = p is a Markov kernel.

theorem CSMC.dirForm_gibbs {ι : Type u_1} [Fintype ι] (p q φ : ι → ℝ) : dirForm p (gibbs q) φ = expect p φ * expect q φ

For the Gibbs kernel K(i, ·) = q, ⟨φ, K φ⟩_p = p(φ) q(φ).

theorem CSMC.dirForm_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p φ : ι → ℝ) : dirForm p 1 φ = expect p (φ ^ 2)

For the identity kernel, ⟨φ, φ⟩_p = p(φ ^ 2).

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

For a probability vector p, p(φ) ^ 2 ≤ p(φ ^ 2): the variance of φ under p is nonnegative.

theorem CSMC.vecMul_apply_eq_expect {ι : Type u_1} [Fintype ι] (φ : ι → ℝ) (M : Matrix ι ι ℝ) (j : ι) : Matrix.vecMul φ M j = expect (fun (i : ι) => M i j) φ

(φ ᵥ* M) j = ∑_i M i j φ i is the expectation of φ with respect to the column M(·, j).