Markov chain Monte Carlo

DefinitionMarkov kernel of a transition rule#✓fully proved

Let \(\alpha\) be a finite state space with a measurable structure in which singletons are measurable. A transition rule \(P\) assigning to each \(x \in \alpha\) a probability distribution \(P(x, \cdot)\) on \(\alpha\) gives the Markov kernel on \(\alpha\) that sends \(x\) to \(P(x, \cdot)\) viewed as a probability measure, so a set \(B\) gets mass \(\sum_{y \in B} P(x, y)\).

noncomputable def pmfKernel (P : α → PMF α) : Kernel α α :=
  Kernel.ofFunOfCountable fun x ↦ (P x).toMeasure

Used by 12

Used bySystematic-scan Gibbs sampler · First step of a Gibbs sweep · Gibbs sweep matrix is stochastic · Positivity of Gibbs sweep transition probabilities · Gibbs sampling leaves the target stationary · A full Gibbs sweep leaves the target stationary · The target is stationary for Metropolis–Hastings · Detailed balance implies invariance · Gibbs updates are reversible · The Metropolis–Hastings kernel is reversible · Detailed balance implies reversibility · Target is stationary for the Gibbs sweep matrix

TheoremDetailed balance implies reversibility#✓fully proved

Let \(\alpha\) be a finite state space with a measurable structure in which singletons are measurable, \(\pi\) a probability distribution on \(\alpha\) and \(P\) a transition rule assigning to each \(x \in \alpha\) a probability distribution \(P(x, \cdot)\) on \(\alpha\). If \(\pi(x) P(x, y) = \pi(y) P(y, x)\) for all \(x, y \in \alpha\), then the Markov kernel \(\kappa\) of \(P\) is reversible with respect to \(\pi\), viewed as a measure: for all measurable sets \(A\) and \(B\), \(\int_A \kappa(x, B) \, d\pi(x) = \int_B \kappa(x, A) \, d\pi(x)\).

theorem isReversible_pmfKernel {π : PMF α} {P : α → PMF α}
    (h : ∀ x y, π x * P x y = π y * P y x) : (pmfKernel P).IsReversible π.toMeasure

Uses 1 · Used by 3

Statement usesMarkov kernel of a transition rule

Used byDetailed balance implies invariance · Gibbs updates are reversible · The Metropolis–Hastings kernel is reversible

TheoremDetailed balance implies invariance#✓fully proved

Let \(\alpha\) be a finite state space with a measurable structure in which singletons are measurable, \(\pi\) a probability distribution on \(\alpha\) and \(P\) a transition rule assigning to each \(x \in \alpha\) a probability distribution \(P(x, \cdot)\) on \(\alpha\). If \(\pi(x) P(x, y) = \pi(y) P(y, x)\) for all \(x, y \in \alpha\), then \(\pi\), viewed as a measure, is invariant for the Markov kernel \(\kappa\) of \(P\): for every measurable set \(B\), \(\int \kappa(x, B) \, d\pi(x) = \pi(B)\).

theorem invariant_pmfKernel {π : PMF α} {P : α → PMF α} (h : ∀ x y, π x * P x y = π y * P y x) :
    (pmfKernel P).Invariant π.toMeasure

Uses 2 · Used by 2

Statement usesMarkov kernel of a transition rule

Proof usesDetailed balance implies reversibility

Used byGibbs sampling leaves the target stationary · The target is stationary for Metropolis–Hastings

TheoremDetailed balance gives a stationary distribution#✓fully proved

Let \(\alpha\) be a finite set, \(\pi\) a probability distribution on \(\alpha\) and \(P\) a transition rule assigning to each \(x \in \alpha\) a probability distribution \(P(x, \cdot)\) on \(\alpha\). If \(\pi(x) P(x, y) = \pi(y) P(y, x)\) for all \(x, y \in \alpha\), then one step of \(P\) started from \(\pi\) is again distributed as \(\pi\): for every \(y \in \alpha\), \(\sum_{x \in \alpha} \pi(x) P(x, y) = \pi(y)\).

theorem bind_eq_of_detailedBalance [Finite α] {π : PMF α} {P : α → PMF α}
    (h : ∀ x y, π x * P x y = π y * P y x) : π.bind P = π

Used by 1

Used byTarget is stationary for the Metropolis–Hastings matrix

DefinitionMetropolis–Hastings acceptance probability#✓fully proved

For a probability distribution \(\pi\) on \(\alpha\) and a proposal \(Q\) assigning to each \(x \in \alpha\) a probability distribution \(Q(x, \cdot)\) on \(\alpha\), the acceptance probability of a move from \(x\) to \(y\) is \(a(x, y) = \min\bigl(1, \pi(y) Q(y, x) / (\pi(x) Q(x, y))\bigr)\), computed in \([0, \infty]\) with \(c / 0 = \infty\) for \(c \ne 0\) and \(0 / 0 = 0\).

noncomputable def mhAccept (π : PMF α) (Q : α → PMF α) (x y : α) : ℝ≥0∞ :=
  min 1 (π y * Q y x / (π x * Q x y))

Used by 3

Used byPrimitivity of the Metropolis–Hastings matrix · Detailed balance for Metropolis–Hastings · Metropolis–Hastings step

DefinitionMetropolis–Hastings step#✓fully proved

For a probability distribution \(\pi\) on \(\alpha\) (the target) and a proposal \(Q\) assigning to each \(x \in \alpha\) a probability distribution \(Q(x, \cdot)\) on \(\alpha\), one Metropolis–Hastings step from \(x\) is the distribution of the following move: draw \(y\) from \(Q(x, \cdot)\), then move to \(y\) with the Metropolis–Hastings acceptance probability \(a(x, y)\), and otherwise stay at \(x\).

noncomputable def mhStep (π : PMF α) (Q : α → PMF α) (x : α) : PMF α :=
  (Q x).bind fun y ↦ (coin (mhAccept π Q x y) (min_le_left _ _)).map fun b ↦ cond b y x

Uses 2 · Used by 7

Statement usesBiased coin · Metropolis–Hastings acceptance probability

Used byThe target is stationary for Metropolis–Hastings · Primitivity of the Metropolis–Hastings matrix · The Metropolis–Hastings kernel is reversible · Detailed balance for Metropolis–Hastings · Metropolis–Hastings transition matrix · Metropolis–Hastings matrix is stochastic · Target is stationary for the Metropolis–Hastings matrix

TheoremDetailed balance for Metropolis–Hastings#✓fully proved

Let \(\pi\) be a probability distribution on a type \(\alpha\), \(Q\) a proposal assigning to each \(x \in \alpha\) a probability distribution \(Q(x, \cdot)\) on \(\alpha\), and \(P(x, y)\) the probability that one Metropolis–Hastings step for target \(\pi\) and proposal \(Q\) moves from \(x\) to \(y\). Then \(\pi(x) P(x, y) = \pi(y) P(y, x)\) for all \(x, y \in \alpha\).

For \(x \ne y\) both sides equal \(\min(\pi(x) Q(x, y), \pi(y) Q(y, x))\); no positivity or symmetry assumption on \(\pi\) or \(Q\) is needed.

theorem mh_detailedBalance (π : PMF α) (Q : α → PMF α) (x y : α) :
    π x * mhStep π Q x y = π y * mhStep π Q y x

Uses 3 · Used by 3

Statement usesMetropolis–Hastings step

Proof usesBiased coin · Metropolis–Hastings acceptance probability

Used byThe target is stationary for Metropolis–Hastings · The Metropolis–Hastings kernel is reversible · Target is stationary for the Metropolis–Hastings matrix

TheoremThe Metropolis–Hastings kernel is reversible#✓fully proved

Let \(\alpha\) be a finite state space with a measurable structure in which singletons are measurable, \(\pi\) a probability distribution on \(\alpha\) and \(Q\) a proposal assigning to each \(x \in \alpha\) a probability distribution \(Q(x, \cdot)\) on \(\alpha\). Then the Markov kernel \(\kappa\) of the Metropolis–Hastings step for target \(\pi\) and proposal \(Q\) is reversible with respect to \(\pi\), viewed as a measure: for all measurable sets \(A\) and \(B\), \(\int_A \kappa(x, B) \, d\pi(x) = \int_B \kappa(x, A) \, d\pi(x)\).

theorem isReversible_mhKernel (π : PMF α) (Q : α → PMF α) :
    (pmfKernel (mhStep π Q)).IsReversible π.toMeasure

Uses 4

Statement usesMetropolis–Hastings step · Markov kernel of a transition rule

Proof usesDetailed balance implies reversibility · Detailed balance for Metropolis–Hastings

TheoremThe target is stationary for Metropolis–Hastings#✓fully proved

Let \(\alpha\) be a finite state space with a measurable structure in which singletons are measurable, \(\pi\) a probability distribution on \(\alpha\) and \(Q\) a proposal assigning to each \(x \in \alpha\) a probability distribution \(Q(x, \cdot)\) on \(\alpha\). Then \(\pi\), viewed as a measure, is invariant for the Markov kernel \(\kappa\) of the Metropolis–Hastings step for target \(\pi\) and proposal \(Q\): for every measurable set \(B\), \(\int \kappa(x, B) \, d\pi(x) = \pi(B)\).

No positivity or symmetry assumption on \(\pi\) or \(Q\) is needed.

theorem invariant_mhKernel (π : PMF α) (Q : α → PMF α) :
    (pmfKernel (mhStep π Q)).Invariant π.toMeasure

Uses 4

Statement usesMetropolis–Hastings step · Markov kernel of a transition rule

Proof usesDetailed balance implies invariance · Detailed balance for Metropolis–Hastings

DefinitionNormalizer of the conditional law#✓fully proved

Let \(\pi\) be a probability distribution on the configurations \(x : \iota \to S\), with \(\iota\) and \(S\) finite. For a coordinate \(i \in \iota\) and a configuration \(x\), the normalizer is \(Z_i(x) = \sum_{s \in S} \pi(x[i \mapsto s]) \in [0, \infty]\), where \(x[i \mapsto s]\) is \(x\) with coordinate \(i\) set to \(s\). It normalizes the conditional law of coordinate \(i\) given the other coordinates of \(x\).

noncomputable def condNorm (π : PMF (ι → S)) (i : ι) (x : ι → S) : ℝ≥0∞ :=
  ∑ s, π (update x i s)

Used by 3

Used byConditional law of a coordinate · Detailed balance for a Gibbs update · Positivity of Gibbs sweep transition probabilities

DefinitionConditional law of a coordinate#✓fully proved

Let \(\pi\) be a probability distribution on the configurations \(x : \iota \to S\), with \(\iota\) and \(S\) finite, such that \(\pi(x) \neq 0\) for every \(x\). For a coordinate \(i \in \iota\) and a configuration \(x\), the conditional law of coordinate \(i\) given the others is the probability distribution on \(S\) that gives \(s \in S\) the mass \(\pi(x[i \mapsto s]) / Z_i(x)\), where \(x[i \mapsto s]\) is \(x\) with coordinate \(i\) set to \(s\) and \(Z_i(x) = \sum_{t \in S} \pi(x[i \mapsto t])\). In the usual notation this is \(\pi(x_i = s \mid x_{-i})\), where \(x_i\) is coordinate \(i\) of \(x\) and \(x_{-i}\) is the family of its other coordinates.

noncomputable def condLaw (π : PMF (ι → S)) (hπ : ∀ x, π x ≠ 0) (i : ι) (x : ι → S) : PMF S :=
  PMF.ofFintype (fun s ↦ π (update x i s) / condNorm π i x) (by
    simp_rw [div_eq_mul_inv]
    rw [← Finset.sum_mul]
    exact ENNReal.mul_inv_cancel (ne_bot_of_le_ne_bot (hπ x) (le_condNorm π i x))
      (condNorm_ne_top π i x))

Uses 1 · Used by 3

Statement usesNormalizer of the conditional law

Used byDetailed balance for a Gibbs update · Gibbs update · Positivity of Gibbs sweep transition probabilities

DefinitionGibbs update#✓fully proved

Let \(\pi\) be a probability distribution on the configurations \(x : \iota \to S\), with \(\iota\) and \(S\) finite, such that \(\pi(x) \neq 0\) for every \(x\). The Gibbs update of coordinate \(i \in \iota\) from \(x\) is the probability distribution of \(x[i \mapsto s]\), the configuration \(x\) with coordinate \(i\) set to \(s\), where \(s\) is drawn from the conditional law of coordinate \(i\) given the other coordinates of \(x\).

noncomputable def gibbsStep (π : PMF (ι → S)) (hπ : ∀ x, π x ≠ 0) (i : ι) (x : ι → S) :
    PMF (ι → S) :=
  (condLaw π hπ i x).map (update x i)

Uses 1 · Used by 9

Statement usesConditional law of a coordinate

Used byDetailed balance for a Gibbs update · Systematic-scan Gibbs sampler · First step of a Gibbs sweep · Gibbs sweep matrix is stochastic · Positivity of Gibbs sweep transition probabilities · Gibbs sampling leaves the target stationary · A full Gibbs sweep leaves the target stationary · Gibbs updates are reversible · Target is stationary for the Gibbs sweep matrix

TheoremSymmetry of differing in one coordinate#✓fully proved

For functions \(x, y : \iota \to S\) and a coordinate \(i \in \iota\), if setting coordinate \(i\) of \(x\) to \(y(i)\) gives \(y\), then setting coordinate \(i\) of \(y\) to \(x(i)\) gives \(x\).

theorem update_eq_comm {i : ι} {x y : ι → S} (h : update x i (y i) = y) :
    update y i (x i) = x

Used by 1

Used byDetailed balance for a Gibbs update

TheoremDetailed balance for a Gibbs update#✓fully proved

Let \(\pi\) be a probability distribution on the configurations \(x : \iota \to S\), with \(\iota\) and \(S\) finite, such that \(\pi(x) \neq 0\) for every \(x\), and for a coordinate \(i\) let \(P_i(x, y)\) be the probability that the Gibbs update of coordinate \(i\) moves \(x\) to \(y\). Then \(\pi(x) P_i(x, y) = \pi(y) P_i(y, x)\) for all configurations \(x\) and \(y\).

When \(x\) and \(y\) differ at most in coordinate \(i\), both sides equal \(\pi(x) \pi(y) / Z\) for the same normalizer \(Z\); otherwise both sides are \(0\).

theorem gibbs_detailedBalance [Finite ι] (π : PMF (ι → S)) (hπ : ∀ x, π x ≠ 0) (i : ι)
    (x y : ι → S) : π x * gibbsStep π hπ i x y = π y * gibbsStep π hπ i y x

Uses 4 · Used by 2

Statement usesGibbs update

Proof usesConditional law of a coordinate · Normalizer of the conditional law · Symmetry of differing in one coordinate

Used byGibbs sampling leaves the target stationary · Gibbs updates are reversible

TheoremGibbs updates are reversible#✓fully proved

Let \(\pi\) be a probability distribution on the configurations \(x : \iota \to S\), with \(\iota\) and \(S\) finite, such that \(\pi(x) \neq 0\) for every \(x\). For every coordinate \(i\), the Markov kernel \(K\) of the Gibbs update of coordinate \(i\) is reversible with respect to \(\pi\): for all measurable sets \(A\) and \(B\) of configurations, \(\int_A K(x, B) \, d\pi(x) = \int_B K(x, A) \, d\pi(x)\).

theorem isReversible_gibbsKernel (π : PMF (ι → S)) (hπ : ∀ x, π x ≠ 0) (i : ι) :
    (pmfKernel (gibbsStep π hπ i)).IsReversible π.toMeasure

Uses 4

Statement usesGibbs update · Markov kernel of a transition rule

Proof usesDetailed balance for a Gibbs update · Detailed balance implies reversibility

TheoremGibbs sampling leaves the target stationary#✓fully proved

Let \(\pi\) be a probability distribution on the configurations \(x : \iota \to S\), with \(\iota\) and \(S\) finite, such that \(\pi(x) \neq 0\) for every \(x\). For every coordinate \(i\), \(\pi\) is an invariant measure of the Markov kernel of the Gibbs update of coordinate \(i\): if \(x\) is drawn from \(\pi\) and coordinate \(i\) is resampled from its conditional law given the other coordinates, the result is again distributed as \(\pi\).

theorem invariant_gibbsKernel (π : PMF (ι → S)) (hπ : ∀ x, π x ≠ 0) (i : ι) :
    (pmfKernel (gibbsStep π hπ i)).Invariant π.toMeasure

Uses 4 · Used by 1

Statement usesGibbs update · Markov kernel of a transition rule

Proof usesDetailed balance for a Gibbs update · Detailed balance implies invariance

Used byA full Gibbs sweep leaves the target stationary

DefinitionSystematic-scan Gibbs sampler#✓fully proved

Let \(\pi\) be a probability distribution on the configurations \(x : \iota \to S\), with \(\iota\) and \(S\) finite, such that \(\pi(x) \neq 0\) for every \(x\). For a list \(l = (i_1, \dots, i_n)\) of coordinates, the systematic-scan Gibbs sampler is the Markov kernel on configurations that applies the Gibbs updates of the coordinates \(i_1, i_2, \dots, i_n\) in this order; for the empty list it is the identity kernel.

noncomputable def gibbsSweep (π : PMF (ι → S)) (hπ : ∀ x, π x ≠ 0) :
    List ι → Kernel (ι → S) (ι → S)
  | [] => Kernel.id
  | i :: l => gibbsSweep π hπ l ∘ₖ pmfKernel (gibbsStep π hπ i)

Uses 2 · Used by 6

Statement usesGibbs update · Markov kernel of a transition rule

Used byFirst step of a Gibbs sweep · Transition matrix of the systematic-scan Gibbs sweep · Gibbs sweep matrix is stochastic · Positivity of Gibbs sweep transition probabilities · A full Gibbs sweep leaves the target stationary · Target is stationary for the Gibbs sweep matrix

TheoremFirst step of a Gibbs sweep#✓fully proved

Let \(\pi\) be a probability distribution on the configurations \(x : \iota \to S\), with \(\iota\) and \(S\) finite, such that \(\pi(x) \neq 0\) for every \(x\). For a list \(l\) of coordinates let \(K_l\) be the systematic-scan Gibbs sampler for \(l\), and for a coordinate \(i\) let \(P_i\) be the Markov kernel of the Gibbs update of coordinate \(i\). Then for every configuration \(x\), the law \(K_{(i, l)}(x)\) of the sampler for the list \((i, l)\) obtained by putting \(i\) in front of \(l\) is the mixture \(\int K_l(y) \, P_i(x, dy)\): first coordinate \(i\) is updated, then the sweep \(l\) runs from the result.

theorem gibbsSweep_cons_apply (π : PMF (ι → S)) (hπ : ∀ x, π x ≠ 0) (i : ι) (l : List ι)
    (x : ι → S) :
    gibbsSweep π hπ (i :: l) x = (pmfKernel (gibbsStep π hπ i) x).bind (gibbsSweep π hπ l)

Uses 3 · Used by 1

Statement usesGibbs update · Systematic-scan Gibbs sampler · Markov kernel of a transition rule

Used byPositivity of Gibbs sweep transition probabilities

TheoremA full Gibbs sweep leaves the target stationary#✓fully proved

Let \(\pi\) be a probability distribution on the configurations \(x : \iota \to S\), with \(\iota\) and \(S\) finite, such that \(\pi(x) \neq 0\) for every \(x\). For every finite list \(l\) of coordinates, in any order and possibly with repetitions, \(\pi\) is an invariant measure of the systematic-scan Gibbs sampler that updates the coordinates in the order of \(l\).

theorem invariant_gibbsSweep (π : PMF (ι → S)) (hπ : ∀ x, π x ≠ 0) (l : List ι) :
    (gibbsSweep π hπ l).Invariant π.toMeasure

Uses 4 · Used by 1

Statement usesSystematic-scan Gibbs sampler

Proof usesGibbs update · Gibbs sampling leaves the target stationary · Markov kernel of a transition rule

Used byTarget is stationary for the Gibbs sweep matrix

TheoremProbabilities of a finite law sum to one#✓fully proved

The probabilities of a law on a finite type, as reals, sum to 1.

theorem sum_toReal_pmf {β : Type*} [Fintype β] (π : PMF β) : ∑ y, (π y).toReal = 1

Used by 3

Used byThe systematic-scan Gibbs sampler converges to its target · The Metropolis–Hastings chain converges to its target · Metropolis–Hastings matrix is stochastic

DefinitionMetropolis–Hastings transition matrix#✓fully proved

The transition matrix P(x, y) = mhStep π Q x y of the Metropolis–Hastings chain, as a real matrix.

noncomputable def mhMatrix (π : PMF α) (Q : α → PMF α) : Matrix α α ℝ :=
  Matrix.of fun x y => (mhStep π Q x y).toReal

Uses 1 · Used by 4

Statement usesMetropolis–Hastings step

Used byThe Metropolis–Hastings chain converges to its target · Primitivity of the Metropolis–Hastings matrix · Metropolis–Hastings matrix is stochastic · Target is stationary for the Metropolis–Hastings matrix

TheoremMetropolis–Hastings matrix is stochastic#✓fully proved

The Metropolis–Hastings matrix is stochastic.

theorem mhMatrix_mem_rowStochastic (π : PMF α) (Q : α → PMF α) :
    mhMatrix π Q ∈ rowStochastic ℝ α

Uses 3 · Used by 1

Statement usesMetropolis–Hastings transition matrix

Proof usesMetropolis–Hastings step · Probabilities of a finite law sum to one

Used byThe Metropolis–Hastings chain converges to its target

TheoremTarget is stationary for the Metropolis–Hastings matrix#✓fully proved

The target is stationary for the Metropolis–Hastings matrix.

theorem vecMul_mhMatrix (π : PMF α) (Q : α → PMF α) :
    (fun x => (π x).toReal) ᵥ* mhMatrix π Q = fun x => (π x).toReal

Uses 4 · Used by 1

Statement usesMetropolis–Hastings transition matrix

Proof usesDetailed balance gives a stationary distribution · Metropolis–Hastings step · Detailed balance for Metropolis–Hastings

Used byThe Metropolis–Hastings chain converges to its target

TheoremPrimitivity of the Metropolis–Hastings matrix#✓fully proved

For a target with full support and a proposal with primitive transition matrix and symmetric support, the Metropolis–Hastings matrix is primitive.

theorem isPrimitive_mhMatrix {π : PMF α} (hπ : ∀ x, π x ≠ 0) {Q : α → PMF α}
    (hQs : ∀ x y, Q x y ≠ 0 → Q y x ≠ 0)
    (hQp : (Matrix.of fun x y => (Q x y).toReal).IsPrimitive) :
    (mhMatrix π Q).IsPrimitive

Uses 4 · Used by 1

Statement usesMetropolis–Hastings transition matrix

Proof usesBiased coin · Metropolis–Hastings acceptance probability · Metropolis–Hastings step

Used byThe Metropolis–Hastings chain converges to its target

TheoremThe Metropolis–Hastings chain converges to its target#✓fully proved

Under the hypotheses of isPrimitive_mhMatrix, there are C and 0 ≤ ρ < 1 with d_TV(Pⁿ(x, ·), π) ≤ C ρⁿ for every start x.

theorem exists_tvDist_mhMatrix_pow_le {π : PMF α} (hπ : ∀ x, π x ≠ 0) {Q : α → PMF α}
    (hQs : ∀ x y, Q x y ≠ 0 → Q y x ≠ 0)
    (hQp : (Matrix.of fun x y => (Q x y).toReal).IsPrimitive) :
    ∃ C ρ : ℝ, 0 ≤ ρ ∧ ρ < 1 ∧ ∀ (n : ℕ) (x : α),
      tvDist (fun y => (mhMatrix π Q ^ n) x y) (fun y => (π y).toReal) ≤ C * ρ ^ n

Uses 7

Statement usesMetropolis–Hastings transition matrix · Total variation distance of functions on a finite set

Proof usesPrimitivity of the Metropolis–Hastings matrix · Metropolis–Hastings matrix is stochastic · Probabilities of a finite law sum to one · Target is stationary for the Metropolis–Hastings matrix · The convergence theorem

DefinitionTransition matrix of the systematic-scan Gibbs sweep#✓fully proved

The transition matrix P(x, y) = gibbsSweep π hπ l x {y} of the systematic-scan Gibbs sweep along l, as a real matrix.

noncomputable def gibbsSweepMatrix (π : PMF (ι → S)) (hπ : ∀ x, π x ≠ 0) (l : List ι) :
    Matrix (ι → S) (ι → S) ℝ :=
  Matrix.of fun x y => (gibbsSweep π hπ l x {y}).toReal

Uses 1 · Used by 4

Statement usesSystematic-scan Gibbs sampler

Used byThe systematic-scan Gibbs sampler converges to its target · Gibbs sweep matrix is stochastic · Positivity of Gibbs sweep transition probabilities · Target is stationary for the Gibbs sweep matrix

TheoremGibbs sweep matrix is stochastic#✓fully proved

The Gibbs sweep matrix is stochastic.

theorem gibbsSweepMatrix_mem_rowStochastic (π : PMF (ι → S)) (hπ : ∀ x, π x ≠ 0) (l : List ι) :
    gibbsSweepMatrix π hπ l ∈ rowStochastic ℝ (ι → S)

Uses 4 · Used by 1

Statement usesTransition matrix of the systematic-scan Gibbs sweep

Proof usesGibbs update · Systematic-scan Gibbs sampler · Markov kernel of a transition rule

Used byThe systematic-scan Gibbs sampler converges to its target

TheoremTarget is stationary for the Gibbs sweep matrix#✓fully proved

The target is stationary for the Gibbs sweep matrix.

theorem vecMul_gibbsSweepMatrix (π : PMF (ι → S)) (hπ : ∀ x, π x ≠ 0) (l : List ι) :
    (fun x => (π x).toReal) ᵥ* gibbsSweepMatrix π hπ l = fun x => (π x).toReal

Uses 5 · Used by 1

Statement usesTransition matrix of the systematic-scan Gibbs sweep

Proof usesGibbs update · Systematic-scan Gibbs sampler · A full Gibbs sweep leaves the target stationary · Markov kernel of a transition rule

Used byThe systematic-scan Gibbs sampler converges to its target

TheoremPositivity of Gibbs sweep transition probabilities#✓fully proved

If the sweep visits every coordinate, every transition probability of the sweep is positive.

theorem gibbsSweepMatrix_pos (π : PMF (ι → S)) (hπ : ∀ x, π x ≠ 0) {l : List ι}
    (hl : ∀ i, i ∈ l) (x y : ι → S) : 0 < gibbsSweepMatrix π hπ l x y

Uses 7 · Used by 1

Statement usesTransition matrix of the systematic-scan Gibbs sweep

Proof usesConditional law of a coordinate · Normalizer of the conditional law · Gibbs update · Systematic-scan Gibbs sampler · First step of a Gibbs sweep · Markov kernel of a transition rule

Used byThe systematic-scan Gibbs sampler converges to its target

TheoremThe systematic-scan Gibbs sampler converges to its target#✓fully proved

If the sweep visits every coordinate, there are C and 0 ≤ ρ < 1 with d_TV(Pⁿ(x, ·), π) ≤ C ρⁿ for every start x.

theorem exists_tvDist_gibbsSweepMatrix_pow_le (π : PMF (ι → S)) (hπ : ∀ x, π x ≠ 0)
    {l : List ι} (hl : ∀ i, i ∈ l) :
    ∃ C ρ : ℝ, 0 ≤ ρ ∧ ρ < 1 ∧ ∀ (n : ℕ) (x : ι → S),
      tvDist (fun y => (gibbsSweepMatrix π hπ l ^ n) x y) (fun y => (π y).toReal) ≤
        C * ρ ^ n

Uses 7

Statement usesTransition matrix of the systematic-scan Gibbs sweep · Total variation distance of functions on a finite set

Proof usesGibbs sweep matrix is stochastic · Positivity of Gibbs sweep transition probabilities · Probabilities of a finite law sum to one · Target is stationary for the Gibbs sweep matrix · The convergence theorem

30 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.