Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
best upper · Exact source theorem

Exact ULD / FORS

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 6.2, using Theorem 6.1 and Theorem 3.2(ii)

Chen, Chewi, Rakhlin, Zhang, Exact simulation of diffusions and improved algorithms for log-concave samplingarXiv:2608.05022v1 (2026-08-05)
Theorem statement
\[\mathsf{FI}(\widehat\pi\Vert\pi)\le\varepsilon^2,\qquad \widetilde O\!\left(M(d^{1/3}+\log(M/p))\right),\quad M=O\!\left(1+\frac{\beta\mathsf{KL}_0}{\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 in Appendix F

01
\[U(0)+\tfrac12\|x\|^2\le U(x)\le U(0)+\tfrac32\|x\|^2\]

Quadratic sandwich for each strongly-log-concave RGO subproblem.

02
\[\mathsf R_\infty(\nu_0\Vert\varpi\otimes N(0,I))\le\tfrac d2\log 3\]

Warm-start bound for the auxiliary ULD sampler.

03
\[\mathsf R_3(\widehat\nu\Vert\varpi\otimes N(0,I))\le\delta_{\rm RGO}^2\]

Theorem 3.2(ii), q=3.

04
\[\text{data processing}\;\Longrightarrow\;\mathtt{Alg}\text{ satisfies Theorem 6.1's RGO assumption}\]

Project phase-space output to position.

05
\[M=O(1+\beta\mathsf{KL}_0/\varepsilon^2)\quad\Longrightarrow\quad \widetilde O(M(d^{1/3}+\log(M/p)))\]

Union bound and summation over the M approximate RGO calls.

Assumptions and implicit prerequisites

What must be true before the rate can be read

Model and geometry

  • No global log-concavity is assumed merely because Fisher information is the output criterion.
  • The potential/score smoothness and finite initial-information quantity are inherited from the cited theorem.
  • Relative Fisher information requires a legitimate density/score representative; ASTIS keeps this regularity obligation visible.

Analytic / proof prerequisites

  • regularity-aware relative Fisher information
  • high-accuracy RGO reduction (Theorem 6.1 / Chewi-Wibisono reduction)
  • Theorem 3.2(ii) exact ULD/FORS block
  • Rényi data processing and Gaussian warm-start bounds
ASTIS rigorous LaTeX
Theorem statement
\[\mathsf{FI}(\widehat\pi\Vert\pi)\le\varepsilon^2,\qquad \widetilde O\!\left(M(d^{1/3}+\log(M/p))\right),\quad M=O\!\left(1+\frac{\beta\mathsf{KL}_0}{\varepsilon^2}\right)\]
Source proof equation 1
\[U(0)+\tfrac12\|x\|^2\le U(x)\le U(0)+\tfrac32\|x\|^2\]
Source proof equation 2
\[\mathsf R_\infty(\nu_0\Vert\varpi\otimes N(0,I))\le\tfrac d2\log 3\]
Source proof equation 3
\[\mathsf R_3(\widehat\nu\Vert\varpi\otimes N(0,I))\le\delta_{\rm RGO}^2\]
Source proof equation 4
\[\text{data processing}\;\Longrightarrow\;\mathtt{Alg}\text{ satisfies Theorem 6.1's RGO assumption}\]
Source proof equation 5
\[M=O(1+\beta\mathsf{KL}_0/\varepsilon^2)\quad\Longrightarrow\quad \widetilde O(M(d^{1/3}+\log(M/p)))\]
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-NONLOGCONCAVE-FISHER-BEST-UPPER-EXACT-ULD-FORS · source snapshot 979f9c367b59f295