Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Markov Chain Monte Carlo · Extended E5 · attached to Chapter 2
Convex-body MCMC: Hit-and-Run
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?
The same continuous state space can support a geometric random walk rather than a Langevin proposal.
Primary §2.1 kernel construction; Vempala §6; cross-link Chewi constrained-sampling topics.
\[X_{k+1}\mid(X_k,u)\sim\operatorname{Unif}(K\cap(X_k+\mathbb Ru))\]
Proposed proof / reuse route
- Require a full-dimensional convex body with finite positive volume.
- Build a measurable random-direction/chord conditional kernel.
- Prove target invariance and required reversibility.
- Use isoperimetry/conductance with the source start and oracle model.
Truth boundary
Uniform on a convex body is log-concave with extended potential, but not a smooth unconstrained potential. Boundary, rounding, warm start and chord-oracle costs remain explicit. Historical survey bounds are not claimed to be current best bounds.
Planned consumers: mcmc, log-concave-sampling, optimisation. Planned sharing is not a compiled dependency or a priority claim.
Sources and exact scope
Geometric Random Walks: A Survey ↗
Santosh Vempala · author manuscript
§§2–4 foundations and isoperimetry; §6 Mixing of Hit-and-Run (PDF pp.25–26); historical claims are edition-scoped
public author manuscript; byte pin required before theorem use