Samplinglib
Lean gate passed 2026-08-19T05:09:39.794721+00:00 · 644be936998e
Chapter 5 · Book pp. 141–173 · August 9, 2026 edition

Faster Low-Accuracy Samplers

Study randomized midpoint, Hamiltonian, and underdamped methods that improve low-accuracy complexity.

Begin with 5.1 Open this chapter in the canonical August 9 source ↗

Chapter route

This chapter develops Hamiltonian flow, momentum refreshment, underdamped Langevin, hypocoercivity. Its main destination is to connect the definitions below to the results that later chapters consume.

Core definitions

  • Randomized midpoint uses an internal random evaluation time to reduce discretization bias.
  • Hamiltonian Monte Carlo alternates approximate Hamiltonian flow with momentum refreshment.
  • Underdamped Langevin evolves position and momentum with friction and noise.
  • Hypocoercive metrics couple position and momentum errors.

Main results

  • Randomized midpoint improves the low-accuracy dimension dependence over basic Euler discretization.
  • Hamiltonian trajectories exploit second-order phase-space motion before refreshment.
  • Underdamped Langevin contracts in a suitable mixed metric under strong log-concavity.
  • Discretized accelerated dynamics produce faster low-accuracy sampling guarantees under stated smoothness and step-size regimes.

Contents

  1. 5.1Randomized Midpoint DiscretizationBook p. 141
  2. 5.2Hamiltonian Monte CarloBook p. 145
  3. 5.3The Underdamped Langevin DiffusionBook p. 149
  4. 5.bibBibliographical NotesBook p. 166
  5. 5.exExercisesBook p. 168
Why is this chapter route valid?

Analytic contracts

  • 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.

Open boundaries

  • Phase-space invariant-law theorem
  • Hypocoercive convergence packet
  • HMC flow and refreshment kernel
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.