Expectations and quadratic forms on a finite index set

The expectation p(φ) = ∑ i, p i * φ i and the quadratic form ⟨φ, K φ⟩_p = ∑ i, ∑ j, p i * K i j * φ i * φ j of Section 2.2 of the paper are defined for weights p : ι → ℝ on a finite type ι, a function φ : ι → ℝ, and a matrix K. When K is a Markov kernel which leaves p invariant, ⟨φ, K φ⟩_p - p(φ) ^ 2 is the lag-one autocovariance of φ for the Markov chain with kernel K started from p.

Probability vectors, the reversibility of a matrix with respect to a vector, and the Gibbs kernel K(i, ·) = p are also defined. A Markov kernel on ι is a matrix in Matrix.rowStochastic ℝ ι, with K i j the probability of moving from i to j.

def CSMC.expect {ι : Type u_1} [Fintype ι] (p φ : ι → ℝ) : ℝ

The expectation p(φ) = ∑ i, p i * φ i of φ with respect to the weights p (Section 2.2).

Equations

• CSMC.expect p φ = ∑ i : ι, p i * φ i

def CSMC.dirForm {ι : Type u_1} [Fintype ι] (p : ι → ℝ) (K : Matrix ι ι ℝ) (φ : ι → ℝ) : ℝ

The quadratic form ⟨φ, K φ⟩_p = ∑ i, ∑ j, p i * K i j * φ i * φ j (Section 2.2).

Equations

• CSMC.dirForm p K φ = ∑ i : ι, ∑ j : ι, p i * K i j * φ i * φ j

theorem CSMC.expect_add {ι : Type u_1} [Fintype ι] (p φ ψ : ι → ℝ) : expect p (φ + ψ) = expect p φ + expect p ψ

The expectation is additive in the function.

def CSMC.IsProbVector {ι : Type u_1} [Fintype ι] (p : ι → ℝ) : Prop

p is a probability vector: its entries are nonnegative and sum to one.

Equations

• CSMC.IsProbVector p = ((∀ (i : ι), 0 ≤ p i) ∧ ∑ i : ι, p i = 1)

def CSMC.IsReversible {ι : Type u_1} (p : ι → ℝ) (K : Matrix ι ι ℝ) : Prop

The matrix K is reversible with respect to p: p i * K i j = p j * K j i for all i and j.

Equations

• CSMC.IsReversible p K = ∀ (i j : ι), p i * K i j = p j * K j i

def CSMC.gibbs {ι : Type u_1} (p : ι → ℝ) : Matrix ι ι ℝ

The Gibbs kernel K(i, ·) = p, under which the new index is drawn from p without regard for the current index i (Section 2.2).

Equations

• CSMC.gibbs p = Matrix.of fun (x j : ι) => p j

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

The entries of a probability vector are at most one.

theorem CSMC.IsProbVector.sum_erase {ι : Type u_1} [Fintype ι] {p : ι → ℝ} [DecidableEq ι] (hp : IsProbVector p) (i : ι) : ∑ k ∈ Finset.univ.erase i, p k = 1 - p i

The entries of a probability vector other than p i sum to 1 - p i.

theorem CSMC.IsProbVector.eq_zero_of_eq_one {ι : Type u_1} [Fintype ι] {p : ι → ℝ} (hp : IsProbVector p) {i j : ι} (hi : p i = 1) (hji : j ≠ i) : p j = 0

If an entry of a probability vector is one, the other entries are zero.

theorem CSMC.sum_pos_of_ne_zero {ι : Type u_1} [Fintype ι] {u : ι → ℝ} (hu : ∀ (i : ι), 0 ≤ u i) (h : u ≠ 0) : 0 < ∑ k : ι, u k

A nonnegative vector which is not zero has a positive sum.

theorem CSMC.isProbVector_div_sum {ι : Type u_1} [Fintype ι] {u : ι → ℝ} (hu : ∀ (i : ι), 0 ≤ u i) (h : u ≠ 0) : IsProbVector fun (i : ι) => u i / ∑ k : ι, u k

A nonnegative vector which is not zero, divided by its sum, is a probability vector.