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

Stochastic Gradient MCMC Algorithms

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.65 / PDF p.71 ↗

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

An approximate transition need not preserve the intended target.

\[X_{k+1}=X_k-h\widehat{\nabla V}(X_k)+\sqrt{2h}\,\xi_k\]

Use a stated time convention: this display is ASTIS normalization, not a verbatim equation of the book. Share the ULA recurrence with the Chewi route through a factor-of-two adapter. Fixed-step ULA/SGLD may have invariant-law bias; drift, stochastic-gradient error, discretization and mixing require separate bounds.

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

Primary source anchors

  1. §3.1 · The Unadjusted Langevin Algorithm printed 65 / PDF 71
  2. §3.2 · Approximate vs. Exact MCMC printed 67 / PDF 73
  3. §3.3 · Stochastic Gradient Langevin Dynamics printed 69 / PDF 75
  4. §3.3.1 · Controlling Stochasticity in the Gradient Estimator printed 72 / PDF 78
  5. §3.3.2 · Example: The Value of Control Variates printed 78 / PDF 84
  6. §3.3.3 · Convergence Results for Stochastic Gradient Langevin Dynamics printed 80 / PDF 86
  7. §3.4 · A General Framework for stochastic gradient MCMC printed 85 / PDF 91
  8. §3.5 · Guidance for Efficient Scalable Bayesian Learning printed 90 / PDF 96
  9. §3.5.1 · Experiments on a Logistic Regression Model printed 92 / PDF 98
  10. §3.5.2 · Experiments on a Bayesian Neural Network Model printed 97 / PDF 103
  11. §3.6 · Generalisations and Extensions printed 100 / PDF 106
  12. §3.6.1 · Scalable Inference for Models in Constrained Spaces printed 100 / PDF 106
  13. §3.6.2 · Scalable Inference with Time Series Data printed 102 / PDF 108
  14. §3.7 · Chapter Notes printed 105 / PDF 111

Attached extended material

All chapters and extensions · Method and target intersections