Rejection sampling

DefinitionBiased coin#✓fully proved

For \(r \in [0, \infty]\) with \(r \le 1\), the biased coin with parameter \(r\) is the probability mass function on \(\{\mathrm{true}, \mathrm{false}\}\) that gives \(\mathrm{true}\) probability \(r\) and \(\mathrm{false}\) probability \(1 - r\).

noncomputable def coin (r : ℝ≥0∞) (hr : r ≤ 1) : PMF Bool :=
  PMF.ofFintype (fun b ↦ cond b r (1 - r)) (by
    rw [Fintype.sum_bool, Bool.cond_true, Bool.cond_false]
    exact add_tsub_cancel_of_le hr)

Used by 5

Used byPrimitivity of the Metropolis–Hastings matrix · Detailed balance for Metropolis–Hastings · Metropolis–Hastings step · One round of rejection sampling · Probability that a round proposes and accepts a given point

DefinitionAcceptance probability#✓fully proved

Given probability mass functions \(p\) and \(q\) on a type \(\alpha\), a constant \(M \in [0, \infty]\) and a point \(x \in \alpha\), the acceptance probability of the proposal \(x\) is \(p(x) / (M\,q(x))\), computed in \([0, \infty]\), where \(a / 0 = \infty\) for \(a \ne 0\) and \(0 / 0 = 0\).

noncomputable def acceptProb (p q : PMF α) (M : ℝ≥0∞) (x : α) : ℝ≥0∞ := p x / (M * q x)

Used by 2

Used byOne round of rejection sampling · Probability that a round proposes and accepts a given point

DefinitionOne round of rejection sampling#✓fully proved

Let \(p\) and \(q\) be probability mass functions on a type \(\alpha\) (the target and the proposal) and let \(M \in [0, \infty]\) be an envelope constant with \(p(x) \le M\,q(x)\) for all \(x \in \alpha\). One round of rejection sampling for target \(p\), proposal \(q\) and envelope \(M\) is the probability mass function on pairs \((x, b) \in \alpha \times \{\mathrm{true}, \mathrm{false}\}\) obtained by drawing \(x\) from \(q\) and then flipping a coin that lands \(b = \mathrm{true}\) ("accepted") with probability \(p(x) / (M\,q(x))\).

noncomputable def trial (p q : PMF α) (M : ℝ≥0∞) (hM : ∀ x, p x ≤ M * q x) : PMF (α × Bool) :=
  q.bind fun x ↦ (coin (acceptProb p q M x) (acceptProb_le_one hM x)).map (Prod.mk x)

Uses 2 · Used by 6

Statement usesAcceptance probability · Biased coin

Used byUniqueness for the first-step equation of rejection sampling · Probability that a round proposes and accepts a given point · Conditional on acceptance, the proposal has the target law · Rejection sampling outputs the target law · Probability that a round rejects · Probability that a round accepts

TheoremProbability that a round proposes and accepts a given point#✓fully proved

Let \(p\) and \(q\) be probability mass functions on \(\alpha\) and \(M \in [0, \infty]\) with \(p(y) \le M\,q(y)\) for all \(y \in \alpha\). For every \(x \in \alpha\), one round of rejection sampling for target \(p\), proposal \(q\) and envelope \(M\) yields the pair \((x, \mathrm{true})\), that is, proposes \(x\) and accepts it, with probability \(p(x) / M\).

theorem trial_apply_true {p q : PMF α} {M : ℝ≥0∞} (hM : ∀ x, p x ≤ M * q x) (x : α) :
    trial p q M hM (x, true) = p x / M

Uses 3 · Used by 4

Statement usesOne round of rejection sampling

Proof usesAcceptance probability · Biased coin

Used byUniqueness for the first-step equation of rejection sampling · Conditional on acceptance, the proposal has the target law · Rejection sampling outputs the target law · Probability that a round accepts

TheoremProbability that a round accepts#✓fully proved

Let \(p\) and \(q\) be probability mass functions on \(\alpha\) and \(M \in [0, \infty]\) with \(p(x) \le M\,q(x)\) for all \(x \in \alpha\). The sum over \(x \in \alpha\) of the probabilities that one round of rejection sampling for target \(p\), proposal \(q\) and envelope \(M\) yields \((x, \mathrm{true})\) equals \(M^{-1}\); that is, a round accepts with probability \(1 / M\).

theorem tsum_trial_true {p q : PMF α} {M : ℝ≥0∞} (hM : ∀ x, p x ≤ M * q x) :
    ∑' x, trial p q M hM (x, true) = M⁻¹

Uses 2 · Used by 2

Statement usesOne round of rejection sampling

Proof usesProbability that a round proposes and accepts a given point

Used byConditional on acceptance, the proposal has the target law · Probability that a round rejects

TheoremProbability that a round rejects#✓fully proved

Let \(p\) and \(q\) be probability mass functions on \(\alpha\) and \(M \in [0, \infty]\) with \(p(x) \le M\,q(x)\) for all \(x \in \alpha\). Let \(r\) be the sum over \(x \in \alpha\) of the probabilities that one round of rejection sampling for target \(p\), proposal \(q\) and envelope \(M\) yields \((x, \mathrm{false})\), that is, the probability that the round rejects. Then \(r + M^{-1} = 1\).

theorem tsum_trial_false_add {p q : PMF α} {M : ℝ≥0∞} (hM : ∀ x, p x ≤ M * q x) :
    ∑' x, trial p q M hM (x, false) + M⁻¹ = 1

Uses 2 · Used by 2

Statement usesOne round of rejection sampling

Proof usesProbability that a round accepts

Used byUniqueness for the first-step equation of rejection sampling · Rejection sampling outputs the target law

TheoremConditional on acceptance, the proposal has the target law#✓fully proved

Let \(p\) and \(q\) be probability mass functions on \(\alpha\) and \(M \in [0, \infty]\) with \(M \ne 0\), \(M \ne \infty\) and \(p(y) \le M\,q(y)\) for all \(y \in \alpha\). For one round of rejection sampling for target \(p\), proposal \(q\) and envelope \(M\), write \(P(x, \mathrm{accepted})\) for the probability that the round proposes \(x\) and accepts it, and \(P(\mathrm{accepted}) = \sum_{y \in \alpha} P(y, \mathrm{accepted})\). Then \(P(x, \mathrm{accepted}) / P(\mathrm{accepted}) = p(x)\) for every \(x \in \alpha\).

theorem trial_true_div_tsum {p q : PMF α} {M : ℝ≥0∞} (hM : ∀ x, p x ≤ M * q x) (hM0 : M ≠ 0)
    (hMt : M ≠ ∞) (x : α) :
    trial p q M hM (x, true) / ∑' y, trial p q M hM (y, true) = p x

Uses 3

Statement usesOne round of rejection sampling

Proof usesProbability that a round proposes and accepts a given point · Probability that a round accepts

TheoremRejection sampling outputs the target law#✓fully proved

Let \(p\) and \(q\) be probability mass functions on \(\alpha\) and \(M \in [0, \infty]\) with \(M \ne 0\), \(M \ne \infty\) and \(p(y) \le M\,q(y)\) for all \(y \in \alpha\). For one round of rejection sampling for target \(p\), proposal \(q\) and envelope \(M\), write \(P(x, \mathrm{accepted})\) for the probability that the round proposes \(x\) and accepts it, and \(r\) for the sum over \(y \in \alpha\) of the probabilities that it proposes \(y\) and rejects it. Then for every \(x \in \alpha\),

\[\sum_{k=0}^{\infty} r^k \, P(x, \mathrm{accepted}) = p(x).\]

Here \(r^k \, P(x, \mathrm{accepted})\) is the probability that repeating independent rounds until one accepts outputs \(x\) after exactly \(k\) rejections, so the output of that loop has law \(p\).

theorem tsum_rejections_mul_trial {p q : PMF α} {M : ℝ≥0∞} (hM : ∀ x, p x ≤ M * q x)
    (hM0 : M ≠ 0) (hMt : M ≠ ∞) (x : α) :
    ∑' k : ℕ, (∑' y, trial p q M hM (y, false)) ^ k * trial p q M hM (x, true) = p x

Uses 3

Statement usesOne round of rejection sampling

Proof usesProbability that a round proposes and accepts a given point · Probability that a round rejects

TheoremUniqueness for the first-step equation of rejection sampling#✓fully proved

Let \(p\) and \(q\) be probability mass functions on \(\alpha\) and \(M \in [0, \infty]\) with \(M \ne 0\), \(M \ne \infty\) and \(p(y) \le M\,q(y)\) for all \(y \in \alpha\). For one round of rejection sampling for target \(p\), proposal \(q\) and envelope \(M\), write \(P(x, \mathrm{accepted})\) for the probability that the round proposes \(x\) and accepts it, and \(r\) for the sum over \(y \in \alpha\) of the probabilities that it proposes \(y\) and rejects it. If \(f \colon \alpha \to [0, \infty]\) takes only finite values and satisfies \(f(x) = P(x, \mathrm{accepted}) + r \, f(x)\) for every \(x \in \alpha\), then \(f(x) = p(x)\) for every \(x \in \alpha\).

The law of the output of the loop that repeats independent rounds until one accepts satisfies this first-step equation, so this result identifies that law as \(p\).

theorem eq_of_firstStep {p q : PMF α} {M : ℝ≥0∞} (hM : ∀ x, p x ≤ M * q x) (hM0 : M ≠ 0)
    (hMt : M ≠ ∞) {out : α → ℝ≥0∞} (hfin : ∀ x, out x ≠ ∞)
    (hout : ∀ x, out x = trial p q M hM (x, true) + (∑' y, trial p q M hM (y, false)) * out x)
    (x : α) : out x = p x

Uses 3

Statement usesOne round of rejection sampling

Proof usesProbability that a round proposes and accepts a given point · Probability that a round rejects

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.