Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
Markov Chain Monte Carlo · Primary Chapter 5

Continuous-Time 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

01

Source audit

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

02

Upstream alignment

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

03

Frontier Cells

Only genuinely missing mathematical edges become theorem-sized tasks.

04

Graph placement

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

Primary v1 · printed p.126 / PDF p.132 ↗

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

A continuous-time method need not be a diffusion.

\[Lf(z)=b(z)\cdot\nabla f(z)+\lambda(z)\!\int\!(f(z\prime)-f(z))Q(z,dz\prime)\]

PDMPs combine deterministic flows and jumps. Audit event rates, simulation, non-explosion, generator domains and invariant integration. An infinitesimal balance identity does not by itself construct an invariant Markov semigroup. Continuous time and continuous state are independent axes.

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

Primary source anchors

  1. §5.1 · Continuous-Time MCMC as the Limit of Non-Reversible MCMC printed 126 / PDF 132
  2. §5.2 · Piecewise Deterministic Markov Processes printed 129 / PDF 135
  3. §5.2.1 · What is a PDMP? printed 129 / PDF 135
  4. §5.2.2 · Simulating PDMPs printed 130 / PDF 136
  5. §5.2.3 · The Generator and Invariant Distribution of a PDMP printed 134 / PDF 140
  6. §5.2.4 · The Limiting Process of Section 5.1 as a PDMP printed 136 / PDF 142
  7. §5.3 · Continuous-time MCMC via PDMPs printed 139 / PDF 145
  8. §5.3.1 · Different Samplers printed 140 / PDF 146
  9. §5.3.2 · Use of PDMP Output printed 154 / PDF 160
  10. §5.3.3 · Comparison of Samplers printed 155 / PDF 161
  11. §5.4 · Efficient Simulation of PDMP Samplers printed 159 / PDF 165
  12. §5.4.1 · Simulating PDMPs printed 159 / PDF 165
  13. §5.4.2 · Exploiting Model Sparsity printed 165 / PDF 171
  14. §5.4.3 · Data Subsampling Ideas printed 168 / PDF 174
  15. §5.5 · Extensions printed 175 / PDF 181
  16. §5.5.1 · Discontinuous Target Distribution printed 176 / PDF 182
  17. §5.5.2 · Reversible Jump PDMP Samplers printed 179 / PDF 185
  18. §5.5.3 · More General Velocity Models printed 184 / PDF 190
  19. §5.6 · Chapter Notes printed 191 / PDF 197

Attached extended material

Use the related Chapters 4–5 extensions through the index.

All chapters and extensions · Method and target intersections