Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
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 3.2(ii) (High-accuracy simulation of ULD)

Chen, Chewi, Rakhlin, Zhang, Exact simulation of diffusions and improved algorithms for log-concave samplingarXiv:2608.05022v1 (2026-08-05)
Theorem statement
\[\mathsf R_q(\widehat\nu\Vert\pi)\le\delta\]

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 C

01
\[\mathsf R_{2q}(\widehat\nu\Vert\nu_K)\le\delta/3\]

FORS simulation error (Lemma C.3).

02
\[\mathsf R_{2q}(\nu_K\Vert\pi)\le\delta/2\]

Continuous ULD contraction under LSI.

03
\[\mathsf R_q(\widehat\nu\Vert\pi)\le\tfrac32\mathsf R_{2q}(\widehat\nu\Vert\nu_K)+\mathsf R_{2q}(\nu_K\Vert\pi)\le\delta\]

Rényi composition/interpolation (Lemma C.4).

Assumptions and implicit prerequisites

What must be true before the rate can be read

Model and geometry

  • The potential is strongly convex and smooth in the sense stated by the cited theorem.
  • The condition number is the source's ratio of smoothness to strong-convexity scales.
  • Warm-start assumptions are theorem-specific; when a result assumes bounded chi-squared divergence, that assumption is not hidden by the final TV guarantee.

Analytic / proof prerequisites

  • continuous ULD contraction in Rényi divergence
  • Girsanov path-density interface
  • FORS unbiased log-density-ratio estimator
  • single-step/path-to-terminal Rényi simulation error
  • Rényi composition/interpolation
ASTIS rigorous LaTeX
Theorem statement
\[\mathsf R_q(\widehat\nu\Vert\pi)\le\delta\]
Source proof equation 1
\[\mathsf R_{2q}(\widehat\nu\Vert\nu_K)\le\delta/3\]
Source proof equation 2
\[\mathsf R_{2q}(\nu_K\Vert\pi)\le\delta/2\]
Source proof equation 3
\[\mathsf R_q(\widehat\nu\Vert\pi)\le\tfrac32\mathsf R_{2q}(\widehat\nu\Vert\nu_K)+\mathsf R_{2q}(\nu_K\Vert\pi)\le\delta\]
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-STRONGLY-LOG-CONCAVE-SMOOTH-BEST-UPPER-EXACT-ULD-FORS · source snapshot 2de79774ed385e90