Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

ABC-MCMC and ABC-sequential Monte Carlo — Examples

1 · Prerequisites

2 · Summary

These finite and continuous examples calculate the augmented stationary target, show how a positive tolerance and a summary can differ from the exact-data posterior, derive an ABC-SMC mixture weight by hand, and exhibit vanishing acceptance and finite-particle collapse. Each calculation checks only its stated model and does not establish general accuracy or convergence.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedOpen item page →

ABC acceptance probability vanishes with the tolerance

Example

Let the parameter space be the singleton ${*}$ with its unit prior and let the simulator return $Y \sim Uniform [0, 1]$ , independently of the parameter. Use the independence proposal $Q = H$ , meaning that each proposal draws the singleton parameter and a fresh uniform datum. Take $S (y) = y$ , observation $s_{0} = \frac{1}{2}$ , and absolute distance. For $0 \leq ϵ \leq \frac{1}{2}$ , the tolerance event is $[\frac{1}{2} - ϵ, \frac{1}{2} + ϵ]$ ; for $ϵ > \frac{1}{2}$ it contains the full simulator support $[0, 1]$ . For positive tolerance use the explicit Metropolis–Hastings density representatives constructed below; acceptance at individual starting states can depend on this choice.

Verification

Given: A uniform simulator on $[0, 1]$ , the stated summary and observation, and a tolerance $ϵ \geq 0$ .

[F1] Augmented ABC tolerance target: the prior-predictive tolerance-event probability is $Z_{ϵ}$ , and the indicator target is defined only when $Z_{ϵ} > 0$ .

[F2] ABC Metropolis–Hastings on simulator-augmented states: a proposed augmented state is simulated and retained only according to the fixed-tolerance Metropolis–Hastings accepted-flow rule.

[F3] Metropolis–Hastings kernel: the generic procedure accepts with the density of the common symmetric part of the forward and transposed proposal flows relative to the forward flow and otherwise makes a self-transition. The procedure chooses measurable representatives $f = d μ / d (μ + μ^{T})$ and $g = d μ^{T} / d (μ + μ^{T})$ with $f + g = 1$ everywhere, and uses $α = \min {1, g / f}$ when $f > 0$ and $α = 1$ when $f = 0$ .

1.1F1givenalgebra

For $0 \leq ϵ \leq \frac{1}{2}$ , the tolerance interval has length $2 ϵ$ , so the singleton prior gives $Z_{ϵ} = 2 ϵ$ ; for $ϵ > \frac{1}{2}$ it covers all of $[0, 1]$ , so $Z_{ϵ} = 1$ .

2.1F1F2F3step 1.1algebra

Fix $ϵ > 0$ and write $h (x)$ for the tolerance indicator of the datum in the augmented state $x$ . Relative to $H (d x) H (d y)$ , the forward and transposed flows have densities $h (x) / Z_{ϵ}$ and $h (y) / Z_{ϵ}$ . Choose $f (x, y) = h (x) / (h (x) + h (y))$ and $g (x, y) = h (y) / (h (x) + h (y))$ when $h (x) + h (y) > 0$ , and $f = g = 1 / 2$ otherwise. These are measurable, sum to one everywhere, and multiplying them by the density $(h (x) + h (y)) / Z_{ϵ}$ of $μ + μ^{T}$ recovers the two flow densities; hence they are valid representatives for [F3].

3.1F1F2F3step 1.1step 2.1algebra∎

At every admissible current state $x$ , $h (x) = 1$ , so these representatives give $f (x, y) > 0$ , $g (x, y) / f (x, y) = h (y)$ and thus $α (x, y) = h (y)$ . Consequently the acceptance probability is $\int h (y) H (d y) = Z_{ϵ}$ , equal to $2 ϵ \to 0$ for $0 < ϵ \leq \frac{1}{2}$ and to $1$ for $ϵ > \frac{1}{2}$ . At $ϵ = 0$ , $Z_{0} = 0$ and [F1] assigns no target. The pointwise acceptance calculation uses the specified representatives, rather than arbitrary modifications on flow-null sets.

ExampleConstruction: AI-generatedVerification: AI-generatedOpen item page →

A positive-tolerance ABC-MH stationary law can differ from the exact-data posterior

Example

Let $Θ = {0, 1}$ have the uniform prior and let $Y = {0, 1, 2}$ . The simulator probabilities are $K (0, {0}) = \frac{1}{2}, K (0, {1}) = \frac{1}{2}, K (0, {2}) = 0,$ $K (1, {0}) = \frac{1}{4}, K (1, {1}) = \frac{1}{2}, K (1, {2}) = \frac{1}{4} .$ Take summary $S (0) = S (1) = 0$ , $S (2) = 1$ , observed summary $s_{0} = 0$ , distance $∣ s - s_{0} ∣$ , and positive tolerance $ϵ = \frac{1}{2}$ . Thus the accepted data set is ${0, 1}$ . Use the independence simulator proposal $Q ((θ, y), \cdot) = H (\cdot)$ , where $H = Π K$ is the prior-simulator law.

Verification

Given: The finite prior, simulator, summary, tolerance, and independence proposal specified in the Example.

[F1] Augmented ABC tolerance target: the augmented target is ${\tilde{Π}}_{ϵ} (C) = Z_{ϵ}^{- 1} \int_{C} 1_{A_{ϵ}} (y) H (d θ, d y)$ when $Z_{ϵ} > 0$ .

[F2] The augmented ABC target has the tolerance posterior as its parameter marginal: the parameter marginal of the augmented target is the tolerance-conditioned ABC law.

[F3] ABC Metropolis–Hastings on simulator-augmented states: ABC-MH applies the general Metropolis–Hastings accepted-flow construction to this target and the simulator-based proposal, keeping rejected proposals as self-transitions.

[F4] ABC Metropolis–Hastings preserves its augmented tolerance target: the resulting kernel is reversible with respect to and leaves invariant this fixed-tolerance target.

[F5] Metropolis–Hastings kernel: the general accepted-flow procedure uses the common part of the forward and transposed proposal flows and retains rejected proposals as self-transitions.

1.1F1givenalgebra

The accepted prior-simulator masses are $H (0, 0) = 1 / 4$ , $H (0, 1) = 1 / 4$ , $H (1, 0) = 1 / 8$ , and $H (1, 1) = 1 / 4$ , while $(1, 2)$ has mass $1 / 8$ outside the tolerance; hence $Z_{ϵ} = 7 / 8$ .

2.1F1F2step 1.1algebra

Dividing those four accepted masses by $7 / 8$ gives augmented masses $(2 / 7, 2 / 7, 1 / 7, 2 / 7)$ and, by [F2], parameter marginal $(4 / 7, 3 / 7)$ .

3.1F2step 2.1algebra

Given exact data $Y = 0$ , the prior-weighted likelihood masses are $1 / 4$ at $θ = 0$ and $1 / 8$ at $θ = 1$ , so the exact posterior is $(2 / 3, 1 / 3)$ , different from $(4 / 7, 3 / 7)$ because the tolerance summary merges $Y = 0$ with $Y = 1$ .

4.1F1F3F4F5step 1.1step 2.1algebra∎

For accepted current and proposed states, the forward flow is ${\tilde{Π}}_{ϵ} (d x) H (d y) = \frac{8}{7} H (d x) H (d y)$ , symmetric under swap, so [F5] accepts; for proposal $(1, 2)$ the transposed flow is zero and the proposal is rejected. Thus $P (x, B) = H (B \cap A_{ϵ}) + \frac{1}{8} 1_{B} (x) = \frac{7}{8} {\tilde{Π}}_{ϵ} (B) + \frac{1}{8} 1_{B} (x)$ for accepted $x$ , and integration gives ${\tilde{Π}}_{ϵ} P (B) = {\tilde{Π}}_{ϵ} (B)$ , verifying stationarity consistently with [F4].

ExampleConstruction: AI-generatedVerification: AI-generatedOpen item page →

A finite ABC-SMC tolerance schedule and its mixture weights

Example

Let $Θ = {0, 1}$ have the uniform prior and $Y = {0, 1, 2}$ . The simulator has $K (0, {0}) = K (0, {1}) = \frac{1}{2}$ and $K (0, {2}) = 0$ , while $K (1, {0}) = \frac{1}{4}$ , $K (1, {1}) = \frac{1}{2}$ , and $K (1, {2}) = \frac{1}{4}$ . Take $S (0) = S (1) = 0$ , $S (2) = 1$ , and $s_{0} = 0$ . Let $ϵ_{0} = \frac{3}{2}$ and $ϵ_{1} = \frac{1}{2}$ . At stage $0$ every simulated datum meets the tolerance. Condition on the possible stage-0 population $(θ_{1}, θ_{2}) = (0, 0)$ with weights $(\frac{1}{2}, \frac{1}{2})$ . At stage $1$ use a perturbation kernel with $Q_{1} (0, {0}) = \frac{99}{100}$ and $Q_{1} (0, {1}) = \frac{1}{100}$ , and set the same row from $θ = 1$ so $Q_{1}$ is fully specified.

Verification

Given: The model, tolerances, previous weighted population, and perturbation kernel specified in the Example.

[F1] Augmented ABC tolerance target: the tolerance target has unnormalized measure $Π (d θ) K (θ, d y) 1_{A_{ϵ}} (y)$ and normalizer $Z_{ϵ}$ .

[F2] Sequential ABC importance-resampling with tolerance populations: the proposal mixture is the weighted mixture of perturbation kernels, and the incremental weight is the tolerance indicator times $d Π / d ϕ_{t}^{N}$ .

[F3] Sequential ABC Radon–Nikodym weights target each tolerance law: under the mixture support condition, the conditional expected unnormalized weighted proposal law is $γ_{t} (d θ, d y) = Π (d θ) K (θ, d y) 1_{A_{ϵ_{t}}} (y)$ , whose total mass is $Z_{ϵ_{t}}$ . Dividing this measure by $Z_{ϵ_{t}}$ gives the current normalized tolerance target; this does not assert unbiasedness of a self-normalized finite-particle estimate.

1.1F1givenalgebra

At $ϵ_{0} = 3 / 2$ , all simulated summaries are accepted, so $Z_{ϵ_{0}} = 1$ ; at $ϵ_{1} = 1 / 2$ , acceptance probabilities are $1$ and $3 / 4$ at the two parameter values, giving $Z_{ϵ_{1}} = 7 / 8$ and target parameter masses $(4 / 7, 3 / 7)$ .

1.2F2givenalgebra

For the previous population $(0, 0)$ , $ϕ_{1}^{N} ({0}) = 99 / 100$ and $ϕ_{1}^{N} ({1}) = 1 / 100$ , so it dominates the uniform prior and the RN ratios are $r_{1}^{N} (0) = (1 / 2) / (99 / 100) = 50 / 99$ and $r_{1}^{N} (1) = (1 / 2) / (1 / 100) = 50$ .

2.1F1F2F3step 1.1step 1.2algebra∎

A proposal matches tolerance with probability $(99 / 100) \cdot 1 + (1 / 100) \cdot (3 / 4) = 399 / 400$ ; its expected weight contributions at $θ = 0, 1$ are $(99 / 100) (1) (50 / 99) = 1 / 2$ and $(1 / 100) (3 / 4) (50) = 3 / 8$ , totaling $7 / 8$ . Their ratio is $(4 / 7, 3 / 7)$ , the population target marginal by [F3]; these are normalized expected unnormalized weights, not a realized self-normalized finite-particle estimate.

ExampleConstruction: AI-generatedVerification: AI-generatedOpen item page →

Finite ABC-SMC particles can miss target support despite a valid mixture weight

Example

Let $Θ = {0, 1}$ have the uniform prior and $Y = {0, 1, 2}$ . The simulator has $K (0, {0}) = K (0, {1}) = \frac{1}{2}$ and $K (0, {2}) = 0$ , while $K (1, {0}) = \frac{1}{4}$ , $K (1, {1}) = \frac{1}{2}$ , and $K (1, {2}) = \frac{1}{4}$ . Take $S (0) = S (1) = 0$ , $S (2) = 1$ , $s_{0} = 0$ , and $ϵ_{1} = \frac{1}{2}$ . Let the previous two-particle population be $(0, 0)$ with equal weights and use the stage-1 kernel $Q_{1} (0, {0}) = \frac{99}{100}$ , $Q_{1} (0, {1}) = \frac{1}{100}$ , with the same row from $θ = 1$ . The proposal mixture has full prior support, and its Radon–Nikodym weights are finite.

Verification

Given: The stage-1 prior, simulator, tolerance event, proposal mixture, and particle count $N = 2$ specified in the Example.

[F1] Sequential ABC importance-resampling with tolerance populations: a candidate receives weight $1_{A_{ϵ_{1}}} (Y) d Π / d ϕ_{1}^{N} (θ)$ , and a zero-total-weight population is reported as degenerate.

[F2] Sequential ABC Radon–Nikodym weights target each tolerance law: the theorem does not claim that a finite self-normalized particle population represents all positive target mass.

1.1F1givenalgebra

The proposal masses are $ϕ_{1}^{N} ({0}) = 99 / 100$ and $ϕ_{1}^{N} ({1}) = 1 / 100$ , so the uniform prior is dominated and the finite RN weights are $r_{1}^{N} (0) = 50 / 99$ and $r_{1}^{N} (1) = 50$ . Tolerance acceptance is certain at $θ = 0$ and has probability $3 / 4$ at $θ = 1$ , so $Z_{ϵ_{1}} = 1 / 2 + (1 / 2) (3 / 4) = 7 / 8$ and the unnormalized target mass at $θ = 1$ is $3 / 8$ , giving normalized mass $3 / 7$ .

2.1F1step 1.1algebra

Each proposal has parameter $0$ with probability $99 / 100$ , independently conditional on the previous population, so both have parameter $0$ with probability $(99 / 100)^{2} = 9801 / 10000$ ; on this event both weights equal $50 / 99$ and the normalized empirical measure assigns zero mass to $θ = 1$ .

3.1F1F2step 1.1step 2.1algebra∎

Step 1.1 gives true target mass $3 / 7$ at $θ = 1$ , whereas the positive-probability event in step 2.1 has no empirical mass there; any resampled offspring also stay at $θ = 0$ . This illustrates the finite-particle caveat in [F2] despite valid support and weights.

ABC-MCMC and ABC-sequential Monte Carlo — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

ABC acceptance probability vanishes with the tolerance

Example

Verification

A positive-tolerance ABC-MH stationary law can differ from the exact-data posterior

Example

Verification

A finite ABC-SMC tolerance schedule and its mixture weights

Example

Verification

Finite ABC-SMC particles can miss target support despite a valid mixture weight

Example

Verification

Sources