6.3 · Book p. 183 · PDF p. 195
Analysis of ULMC via Girsanov's Theorem
Carries the Girsanov route to underdamped dynamics, with phase-space moment and discretization estimates.
Open this section in the canonical August 9 source ↗Place in the proof route
The chapter uses this material in the route toward LMC admits a Rényi-divergence analysis through interpolation. 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 interpolated chain must be adapted and have the same diffusion coefficient as the comparison process.
- Moment estimates must be established before integrating local drift error.
- Step-size restrictions and all dimension/condition-number constants must be retained.
View Lean formalization
No declaration-level mapping has been accepted for this section. This is a route status, not a failed Lean declaration.