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

Convergence in Rényi Divergence

Analyze LMC and ULMC in Rényi divergence using interpolation and Girsanov arguments.

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

Chapter route

This chapter develops Rényi divergence, Langevin Monte Carlo, underdamped LMC, continuous interpolation. Its main destination is to connect the definitions below to the results that later chapters consume.

Core definitions

  • Rényi divergence is the logarithmic power integral of a density ratio at a chosen order.
  • LMC and ULMC interpolations are continuous processes agreeing with the discrete algorithms at grid times.
  • Local drift error is the squared discrepancy between the true and frozen or discretized drift.

Main results

  • LMC admits a Rényi-divergence analysis through interpolation.
  • A Girsanov route controls LMC by an integrated drift mismatch.
  • The underdamped analogue requires phase-space moment and drift-error bounds.
  • The final complexity estimates balance continuous convergence, divergence order, and step size.

Contents

  1. 6.1Analysis of LMC via Interpolation ArgumentBook p. 174
  2. 6.2Analysis of LMC via Girsanov's TheoremBook p. 178
  3. 6.3Analysis of ULMC via Girsanov's TheoremBook p. 183
  4. 6.bibBibliographical NotesBook p. 184
  5. 6.exExercisesBook p. 185
Why is this chapter route valid?

Analytic contracts

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

Open boundaries

  • Full LMC strong/weak interpolation chain
  • ULMC path-space comparison
  • Optimized complexity corollaries
View Lean formalization

These mappings are evidence links, not a claim that the entire chapter is formalized.