Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Markov Chain Monte Carlo · Primary Chapter 6
Assessing and Improving 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
Upstream alignment
Search shared kernel/measure, finite-state, calculus, covariance and geometry APIs; source overlap does not certify direct Lean compatibility.
Frontier Cells
Only genuinely missing mathematical edges become theorem-sized tasks.
Graph placement
Dependencies, consumers, cross-library bridges, and reusable shared interfaces.
Sampling error, estimator variance and diagnostics are distinct.
\[\sigma_f^2=\operatorname{Var}_\pi(f)+2\sum_{k\ge1}\operatorname{Cov}_\pi(f(X_0),f(X_k))\]
The covariance series needs stationary sampling and summability; a CLT needs its own assumptions. Diagnostics are not automatic finite-sample certificates. Distinguish Monte Carlo iterations n, data count N and dimension d. Share IPM/transport and covariance tools without treating dependent samples as IID.
ASTIS orientation, not a verbatim source theorem or Lean closure.
Primary source anchors
- §6.1 · Diagnostics for MCMC printed 192 / PDF 198
- §6.1.1 · Convergence Diagnostics printed 193 / PDF 199
- §6.1.2 · Bias Diagnostics printed 194 / PDF 200
- §6.1.3 · Improved Bias Diagnostics via the Kernel Trick printed 197 / PDF 203
- §6.2 · Convergence Bounds for MCMC printed 200 / PDF 206
- §6.2.1 · Bounds on Integral Probability Metrics printed 200 / PDF 206
- §6.2.2 · Choice of Auxiliary Markov Process printed 203 / PDF 209
- §6.2.3 · Kernel Stein Discrepancy printed 205 / PDF 211
- §6.2.4 · Convergence Control printed 210 / PDF 216
- §6.2.5 · Stochastic Gradient Stein Discrepancy printed 216 / PDF 222
- §6.3 · Optimal Weights for MCMC printed 218 / PDF 224
- §6.4 · Optimal Thinning for MCMC printed 223 / PDF 229
- §6.5 · Chapter Notes printed 224 / PDF 230
Attached extended material
E8
Run length, diagnostics and quantitative guarantees
Attached to primary Chapter 6. Separate a useful diagnostic from a theorem that controls a stated error.
E9
Coupling for unbiased MCMC estimates
Attached to primary Chapter 6. Use coupling not just to bound mixing, but to construct an unbiased expectation estimator.
E10
Control variates and expectation-preserving corrections
Attached to primary Chapter 6. Reuse zero-mean identities while keeping a fitted correction distinct from a target-preserving transition.
All chapters and extensions · Method and target intersections