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

The Proximal Sampler

Study an augmented-variable sampler that isolates difficult geometry in a proximal subproblem.

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

Chapter route

This chapter develops proximal distribution, restricted Gaussian oracle, data augmentation, conditional Gibbs update. Its main destination is to connect the definitions below to the results that later chapters consume.

Core definitions

  • The proximal sampler alternates two conditionals of a Gaussian-augmented joint law.
  • A restricted Gaussian oracle samples a potential tilted by a local quadratic.
  • Simultaneous flow couples the target and auxiliary conditional evolutions.
  • Time reversal provides a second route to contraction and comparison.

Main results

  • The augmentation preserves the desired target as a marginal.
  • The proximal chain contracts under strong log-concavity.
  • Simultaneous flow and time reversal extend the analysis to general log-concavity.
  • Functional inequalities and implementable RGO constructions yield further convergence and application results.

Contents

  1. 8.1Introduction to the Proximal SamplerBook p. 215
  2. 8.2Convergence under Strong Log-ConcavityBook p. 216
  3. 8.3Simultaneous Flow and Time ReversalBook p. 218
  4. 8.4Convergence under Log-ConcavityBook p. 221
  5. 8.5Convergence under Functional InequalitiesBook p. 222
  6. 8.6Implementations of the RGO and ApplicationsBook p. 223
  7. 8.bibBibliographical NotesBook p. 229
  8. 8.exExercisesBook p. 230
Why is this chapter route valid?

Analytic contracts

  • Both conditional distributions require finite, measurable normalizing constants.
  • Marginal preservation follows from Tonelli/Fubini only after nonnegativity and measurability are established.
  • An oracle specification must state whether samples are exact or approximate.

Open boundaries

  • Restricted Gaussian conditional kernel
  • Marginal invariance
  • Oracle-error propagation
View Lean formalization

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

Section 8.1

A Gaussian augmentation creates alternating conditional distributions with the target as a marginal.

No local declaration is mapped yet.