Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
upper · Exact source theorem

FORS-implemented proximal sampler

A paper-first mathematical case study: read the theorem, the derivation route, and the hidden prerequisites before opening formal infrastructure.

Formal topologyOpen this result's proof branch↗
Statement

Exact source theorem

Theorem G.1(3), specialized to s=1

Chen, Chewi, Daskalakis, Rakhlin, High-accuracy sampling for diffusion models and log-concave distributionsarXiv:2602.01338v2 (2026-04-27)
Theorem statement
\[D_{\mathsf{KL}}(\widehat\mu\Vert\mu)\le\varepsilon^2,\qquad N=\widetilde O\!\left(\beta\sqrt d\frac{W_2^2(\mu_0,\mu)}{\varepsilon^2}\right)\]

Reading. Read the accuracy guarantee together with the complexity/rate: the source assumptions and its notion of oracle cost are part of the result.

Primary-source audit complete. The displayed theorem statement is the controlling mathematical contract for this case.

Proof / derivation

proof omitted; inherited proximal/RGO error tracking

The primary source explicitly omits this proof or inherits it from an earlier argument. ASTIS preserves that omission instead of inventing missing source steps.

Assumptions and implicit prerequisites

What must be true before the rate can be read

Model and geometry

  • The target is log-concave with the source's smoothness hypothesis on the potential or score.
  • The initialization scale, typically expressed through a Wasserstein or divergence quantity, is part of the bound.
  • Implemented proximal results additionally require the restricted-Gaussian/proximal oracle promised by the source theorem.

Analytic / proof prerequisites

  • same shared prerequisites as the weak-smooth G.1(3) case
  • smooth specialization s=1
ASTIS rigorous LaTeX
Theorem statement
\[D_{\mathsf{KL}}(\widehat\mu\Vert\mu)\le\varepsilon^2,\qquad N=\widetilde O\!\left(\beta\sqrt d\frac{W_2^2(\mu_0,\mu)}{\varepsilon^2}\right)\]
Lean formalization

This fold is intentionally quiet while the source statement, proof route, and assumptions are being completed case by case. A source-facing Lean theorem will appear here only after it compiles and its statement has been matched to the audited source.

References and provenance

SampleWiki setting

ASTIS-SW-SETTING-LOG-CONCAVE-SMOOTH-UPPER-FORS-IMPLEMENTED-PROXIMAL-SAMPLER · source snapshot b280bbe6689edc53