Markov Chain Monte Carlo · Primary Chapter 2

Reversible MCMC and its Scaling

Stable source-facing chapter environment inside the shared Samplinglib reader.

scaffoldsource mapFull source closure not claimed

Planned route

Source → theorem map → reusable Lean nodes

Source audit

Definitions, theorems, assumptions, proof route, and exact anchors.

Upstream alignment

Search shared kernel/measure, finite-state, calculus, covariance and geometry APIs; source overlap does not certify direct Lean compatibility.

Frontier Cells

Only genuinely missing mathematical edges become theorem-sized tasks.

Graph placement

Dependencies, consumers, cross-library bridges, and reusable shared interfaces.

Primary v1 · printed p.42 / PDF p.48 ↗

This page establishes a stable source route and truth boundary; it does not claim a completed formalization.

Proposals, invariant kernels, and scaling are different obligations.

\pi(x)q(x,y)\alpha(x,y)=\min\{\pi(x)q(x,y),\pi(y)q(y,x)\}

First prove a correctly normalized Metropolis construction, including rejection mass, support and zero-denominator rules. Gibbs/heat-bath updates use a conditional-law adapter. Random-scan mixtures and deterministic-scan compositions have different reversibility properties. Scaling limits are asymptotic claims, not finite-dimensional guarantees.

ASTIS orientation, not a verbatim source theorem or Lean closure.

Primary source anchors

§2.1 · The Metropolis–Hastings Algorithm printed 43 / PDF 49
§2.1.1 · Component-wise updates and Gibbs moves printed 48 / PDF 54
§2.1.2 · The Metropolis–Hastings Independence Sampler printed 49 / PDF 55
§2.1.3 · The Random Walk Metropolis Algorithm printed 50 / PDF 56
§2.1.4 · The Metropolis-Adjusted Langevin Algorithm printed 53 / PDF 59
§2.2 · Hamiltonian Monte Carlo printed 57 / PDF 63
§2.3 · Chapter Notes printed 63 / PDF 69

Attached extended material

extended · outline