Samplinglib
Lean gate passed 2026-08-19T06:04:36.257124+00:00 · 77184245109a
8.1 · Book p. 215 · PDF p. 227

Introduction to the Proximal Sampler

Introduces the Gaussian augmentation and alternating conditional updates defining the proximal sampler.

Open this section in the canonical August 9 source ↗
Section 8.1

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

The proximal sampler augments the target with a Gaussian coupling between x and y, then alternates the two conditional laws. The x-marginal remains the original target, while the conditional structure exposes a restricted Gaussian oracle.

Why is this valid?

Before composing kernels, both conditional normalizers must be measurable, positive, and finite.

Source assumptions

  • well-defined conditional samplers

Formal assumptions

  • kernel measurability
  • finite conditional normalizers
  • joint-law marginal identity
View Lean formalization
todo · faithful paraphrase

ASTIS treats kernel measurability, normalization, Fubini/Tonelli, and marginal preservation as independent reusable roots.

No ASTIS-owned declaration is mapped yet.

Downstream consumers

  • proximal sampler convergence
  • structured sampling