Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Markov Chain Monte Carlo · Primary Chapter 4
Non-Reversible MCMC
Stable source-facing chapter environment inside the shared Samplinglib reader.
scaffoldsource mapFull source closure not claimed
Planned route
Source → theorem map → reusable Lean nodes
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.
Preserving a law is weaker than being reversible.
\[\pi P=\pi\quad\not\Rightarrow\quad \pi(dx)P(x,dy)=\pi(dy)P(y,dx)\]
Keep invariance independent of detailed balance. Lifting changes the state, and a marginal target must be proved by projection. Ordinary position-space HMC with the usual symmetrization can be reversible; Hamiltonian dynamics alone is not a blanket nonreversibility certificate. Acceleration depends on an explicit comparator and cost.
ASTIS orientation, not a verbatim source theorem or Lean closure.
Primary source anchors
- §4.1 · The Benefits of Non-Reversibility printed 106 / PDF 112
- §4.2 · Hamiltonian Monte Carlo Revisited printed 109 / PDF 115
- §4.3 · Lifting Schemes for MCMC printed 112 / PDF 118
- §4.3.1 · Non-Reversible HMC printed 112 / PDF 118
- §4.3.2 · Gustafson’s Algorithm and Multidimensional Generalisations printed 113 / PDF 119
- §4.4 · Improving Non-reversibility: Delayed Rejection printed 119 / PDF 125
- §4.4.1 · The Discrete Bouncy Particle Sampler printed 121 / PDF 127
- §4.5 · Chapter Notes printed 124 / PDF 130
Attached extended material
E7
Lifting, bouncy dynamics and PDMP limits
Attached to primary Chapter 4. Changing the state and clock connects deterministic proposals and event-driven samplers, but not via an unconditional equivalence.
All chapters and extensions · Method and target intersections