Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Markov Chain Monte Carlo · Extended E10 · attached to Chapter 6
Control variates and expectation-preserving corrections
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?
Reuse zero-mean identities while keeping a fitted correction distinct from a target-preserving transition.
Primary §§1.1.4,3.3.1,6.3; MCMC control-variates chapter.
\[\pi(f-c)=\pi(f)\quad\text{when }\pi(c)=0\]
Proposed proof / reuse route
- Audit integrability and a genuine zero-mean identity.
- Compare stationary asymptotic variance, not just pointwise variance.
- Check training and evaluation dependence.
- Preserve any boundary terms in generator/Stein identities.
Truth boundary
Variance reduction is not automatically guaranteed by a zero mean. A fitted correction can introduce bias; a formal generator identity requires its domain and integration-by-parts assumptions.
Planned consumers: mcmc, optimisation, statistical-optimal-transport. Planned sharing is not a compiled dependency or a priority claim.
Sources and exact scope
Control Variates for MCMC ↗
Leah South, Matthew Sutton · 2402.07349v1
Control variates and zero-mean identities; estimator validity and learning bias must be checked
version-pinned; theorem-level audit pending