Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
Markov Chain Monte Carlo · Primary Chapter 1

Background

Stable source-facing chapter environment inside the shared Samplinglib reader.

scaffoldsource mapFull source closure not claimed
Planned route

Source → theorem map → reusable Lean nodes

01

Source audit

Definitions, theorems, assumptions, proof route, and exact anchors.

02

Upstream alignment

Search shared kernel/measure, finite-state, calculus, covariance and geometry APIs; source overlap does not certify direct Lean compatibility.

03

Frontier Cells

Only genuinely missing mathematical edges become theorem-sized tasks.

04

Graph placement

Dependencies, consumers, cross-library bridges, and reusable shared interfaces.

Primary v1 · printed p.4 / PDF p.10 ↗

This page establishes a stable source route and truth boundary; it does not claim a completed formalization.

Separate the sampler from its target and its estimator.

\[\pi P=\pi,\qquad \widehat I_n=\frac1n\sum_{k=1}^n f(X_k)\]

Share measurable kernels, invariance, covariance and integrability. The RKHS kernel of §1.5 is not a Markov transition kernel. Pull §1.3 forward; stochastic calculus is only a prerequisite for the diffusion branch. A Markov law contract is not an existence theorem for a process or semigroup.

ASTIS orientation, not a verbatim source theorem or Lean closure.

Primary source anchors

  1. §1.1 · Monte Carlo Methods printed 5 / PDF 11
  2. §1.1.1 · What is Monte Carlo Integration? printed 5 / PDF 11
  3. §1.1.2 · Importance Sampling printed 7 / PDF 13
  4. §1.1.3 · Monte Carlo or Quadrature? printed 7 / PDF 13
  5. §1.1.4 · Control Variates printed 9 / PDF 15
  6. §1.1.5 · Monte Carlo Integration and Bayesian Statistics printed 11 / PDF 17
  7. §1.2 · Example Applications printed 14 / PDF 20
  8. §1.2.1 · Logistic Regression printed 15 / PDF 21
  9. §1.2.2 · Bayesian Matrix Factorisation printed 15 / PDF 21
  10. §1.2.3 · Bayesian Neural Networks for Classification printed 16 / PDF 22
  11. §1.3 · Markov Chains printed 17 / PDF 23
  12. §1.3.1 · Reversible Markov chains printed 18 / PDF 24
  13. §1.3.2 · Convergence, Averages, and Variances printed 19 / PDF 25
  14. §1.4 · Stochastic Differential Equations printed 22 / PDF 28
  15. §1.4.1 · The Ornstein–Uhlenbeck Process printed 23 / PDF 29
  16. §1.4.2 · The Infinitesimal Generator printed 24 / PDF 30
  17. §1.4.3 · Langevin Diffusions printed 26 / PDF 32
  18. §1.5 · The Kernel Trick printed 28 / PDF 34
  19. §1.5.1 · Finite-Dimensional Inner Product Spaces printed 28 / PDF 34
  20. §1.5.2 · Kernels in a Finite-Dimensional Inner Product Space printed 31 / PDF 37
  21. §1.5.3 · A New Inner Product and the Kernel Trick in Finite Dimensions printed 34 / PDF 40
  22. §1.5.4 · General Kernels printed 35 / PDF 41
  23. §1.5.5 · The Power of the Kernel Trick printed 38 / PDF 44
  24. §1.6 · Chapter Notes printed 40 / PDF 46

Attached extended material

All chapters and extensions · Method and target intersections