Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Markov Chain Monte Carlo · Extended E3 · attached to Chapter 2
Optimal scaling beyond product targets
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?
Separate a high-dimensional optimization criterion from finite-dimensional convergence.
Primary §2.1.3; Yang–Roberts–Rosenthal §§2–3 (PDF pp.4–16); RR §6.
\[\operatorname{ESJD}=\mathbb E[\|X_{k+1}-X_k\|^2]\]
Proposed proof / reuse route
- Fix the sequence of target laws and proposal scaling.
- Audit ESJD and acceptance-limit assumptions.
- Check stronger conditions needed for a diffusion limit.
- Translate time scaling and cost only through a separate argument.
Truth boundary
The 0.234 acceptance limit is not a universal tuning theorem. A weak diffusion limit is not by itself a nonasymptotic mixing bound; correlated targets still need the exact source conditions.
Planned consumers: mcmc, log-concave-sampling, optimisation. Planned sharing is not a compiled dependency or a priority claim.
Sources and exact scope
Optimal Scaling of Random-Walk Metropolis Algorithms on General Target Distributions ↗
Jun Yang, Gareth O. Roberts, Jeffrey S. Rosenthal · 1904.12157v3
§§2–3: optimal ESJD and diffusion limits; assumptions differ between results
version-and-sha256-pinned
General state space Markov chains and MCMC algorithms ↗
Gareth O. Roberts, Jeffrey S. Rosenthal · math/0404033v4
§2 construction; §§3–4 convergence/drift/coupling; §5 CLT; §6 scaling. Probability Surveys 1 (2004), 20–71; arXiv v4 (2007).
version-and-sha256-pinned