5.3 · Book p. 149 · PDF p. 161
The Underdamped Langevin Diffusion
Analyzes underdamped Langevin diffusion and its discretizations in phase space, where hypocoercive effects replace direct contraction.
Open this section in the canonical August 9 source ↗Place in the proof route
The chapter uses this material in the route toward Randomized midpoint improves the low-accuracy dimension dependence over basic Euler discretization. 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
- Invariant phase-space laws require both position and momentum normalization.
- Hypocoercive estimates mix position and velocity norms; coercivity is not pointwise in the position coordinate alone.
- Exact Hamiltonian flow and numerical integrators must not be conflated.
View Lean formalization
No declaration-level mapping has been accepted for this section. This is a route status, not a failed Lean declaration.