Chapter 4 · Book pp. 123–140 · August 9, 2026 edition
Analysis of Langevin Monte Carlo
Derive Langevin Monte Carlo guarantees through Wasserstein coupling, interpolation, convex optimization, and Girsanov comparison.
Begin with 4.1 Open this chapter in the canonical August 9 source ↗Chapter route
This chapter develops synchronous coupling, reflection coupling, interpolation, gradient flow. Its main destination is to connect the definitions below to the results that later chapters consume.
Core definitions
- Langevin Monte Carlo is the Euler discretization of overdamped Langevin diffusion.
- A synchronous coupling shares Brownian noise between two trajectories.
- A continuous interpolation embeds the discrete chain into an SDE with frozen drift.
- Girsanov comparison measures the interpolation error at the path-law level.
Main results
- Wasserstein coupling yields contraction plus a one-step discretization bias.
- Interpolation arguments control terminal error through a differential inequality.
- A convex-optimization analogy recovers a sampling convergence estimate.
- Girsanov's theorem converts integrated drift mismatch into a divergence bound for LMC.
Contents
Why is this chapter route valid?
Analytic contracts
- The coupled processes must be constructed on one filtered probability space.
- Path-space laws and filtration-adapted drift differences must be explicit.
- Optimization analogies do not replace stochastic existence or integrability assumptions.
Open boundaries
- Reflection coupling construction
- Full path-law comparison
View Lean formalization
These mappings are evidence links, not a claim that the entire chapter is formalized.
No declaration-level source block is mapped for this chapter yet.