Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Markov Chain Monte Carlo · Extended E6 · attached to Chapter 3
Perturbed kernels: approximation versus exact invariance
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
Use one canonical shared node where types match. Formal/source audit is still required.
Frontier Cells
Only genuinely missing mathematical edges become theorem-sized tasks.
Graph placement
Dependencies, consumers, cross-library bridges, and reusable shared interfaces.
ASTIS extended material, not a chapter of Fearnhead–Nemeth–Oates–Sherlock. No Lean closure asserted.
Why this extension?
A cheap transition may approximate an ideal chain while introducing a persistent target bias.
Primary §§3.1–3.3; pinned perturbations §19.2–§19.3.
\[d(\mu\widetilde P^n,\pi)\le d(\mu\widetilde P^n,\mu P^n)+d(\mu P^n,\pi)\]
Proposed proof / reuse route
- State the ideal and implemented kernels separately.
- Pin the discrepancy, initialization and local error.
- Prove stability/error propagation rather than assume it.
- Combine with the ideal mixing bound and report total work.
Truth boundary
Invariant-law bias need not vanish at a fixed step size. Small local error alone does not give a uniform-in-time bound. General-state drift norms and Wasserstein metrics require separate adapters.
Planned consumers: mcmc, log-concave-sampling, statistical-optimal-transport. Planned sharing is not a compiled dependency or a priority claim.
Sources and exact scope
Perturbations of Markov Chains ↗
Daniel Rudolf, Aaron Smith, Matias Quiroz · 2404.10251v1
§19.2 Basic Principles and §19.3 Survey of Mathematical Results in this pinned preprint; handbook chapter numbering may differ
version-pinned; theorem-level audit pending