5.bib · Book p. 166 · PDF p. 178
Bibliographical Notes
The bibliographical notes identify the papers and books behind this chapter's arguments and indicate where stronger or more technical versions can be found.
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.