4.1 · Book p. 124 · PDF p. 136
Proof via Wasserstein Coupling
Proves Langevin Monte Carlo error bounds by synchronously coupling the diffusion and its Euler discretization.
Open this section in the canonical August 9 source ↗Place in the proof route
The chapter uses this material in the route toward Wasserstein coupling yields contraction plus a one-step discretization bias. The declaration-level source map is intentionally left inside the formalization layer until exact theorem anchors have been audited.
Why is this valid?
Chapter-level validity conditions
- 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.
View Lean formalization
No declaration-level mapping has been accepted for this section. This is a route status, not a failed Lean declaration.