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

FORS + 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)

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_s^{2/(1+s)}d^{s/(1+s)}\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; source says it follows the RGO implementation error tracking of Altschuler-Chewi

01
\[\eta^{-1}=C\left(\beta_s^2d^s\log(1/\varepsilon)+\beta_s^2d^{-(1-s)}\log^2(1/\varepsilon)\right)^{1/(1+s)}\]

Choose the RGO scale required by Theorem G.1.

02
\[D_{\mathsf{KL}}(\widehat\mu\Vert\mu)\le\varepsilon^2\]

Assemble ideal proximal convergence with per-RGO implementation error; the paper omits the repeated derivation.

Assumptions and implicit prerequisites

What must be true before the rate can be read

Model and geometry

  • The potential is convex and satisfies the weak/Hölder smoothness model of the cited theorem.
  • The Hölder exponent and constant are source parameters; ASTIS does not silently replace them by ordinary smoothness.
  • The initial transport scale and the requested KL accuracy are kept explicit in the rate.

Analytic / proof prerequisites

  • Chewi Theorem 8.4.1
  • proximal-sampler inexact-RGO error accumulation
  • FORS Gaussian-tilt/RGO implementation theorem
ASTIS rigorous LaTeX
Theorem statement
\[D_{\mathsf{KL}}(\widehat\mu\Vert\mu)\le\varepsilon^2,\qquad N=\widetilde O\!\left(\beta_s^{2/(1+s)}d^{s/(1+s)}\frac{W_2^2(\mu_0,\mu)}{\varepsilon^2}\right)\]
Source proof equation 1
\[\eta^{-1}=C\left(\beta_s^2d^s\log(1/\varepsilon)+\beta_s^2d^{-(1-s)}\log^2(1/\varepsilon)\right)^{1/(1+s)}\]
Source proof equation 2
\[D_{\mathsf{KL}}(\widehat\mu\Vert\mu)\le\varepsilon^2\]
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-HOLDER-SMOOTH-LOG-CONCAVE-BEST-UPPER-FORS-PROXIMAL-SAMPLER · source snapshot edb3cd2cfcacb355