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

Ideal proximal chain

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 8.4.1 (Proximal sampler under log-concavity)

Sinho Chewi, Log-Concave Sampling2026-08-09 book edition
Theorem statement
\[\operatorname{KL}(\mu_n^X\Vert\pi^X)\le \frac{W_2^2(\mu_0^X,\pi^X)}{nh}\]

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 given in source

01
\[\partial_t K_t=-\tfrac12 I_t\]

Theorem 8.3.1 specialized to the simultaneous heat flow.

02
\[K_t^2\le I_t W_t^2\]

Theorem 1.4.5 plus the Wasserstein first variation and Cauchy-Schwarz.

03
\[W_t^2\le W_0^2\quad\Longrightarrow\quad K_t'\le-\frac{K_t^2}{2W_0^2}\]

Simultaneous heat-flow contraction.

04
\[\frac1{K_h}\ge\frac1{K_0}+\frac{h}{2W_0^2}\]

Solve the forward half-step differential inequality; the backward half-step gives the same increment.

05
\[\frac1{K_{j+1}}\ge\frac1{K_j}+\frac{h}{W_0^2}\quad\Longrightarrow\quad K_n\le\frac{W_0^2}{nh}\]

Full-step reciprocal growth followed by the already compiled telescoping tail.

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

  • Chewi §1.2 regularity-aware relative Fisher information
  • Chewi Theorem 1.4.5 and the Fisher-Wasserstein first-order bridge
  • Chewi Theorem 8.3.1 simultaneous f-divergence flow
  • forward/backward heat-flow W2 contraction and time reversal
ASTIS rigorous LaTeX
Theorem statement
\[\operatorname{KL}(\mu_n^X\Vert\pi^X)\le \frac{W_2^2(\mu_0^X,\pi^X)}{nh}\]
Source proof equation 1
\[\partial_t K_t=-\tfrac12 I_t\]
Source proof equation 2
\[K_t^2\le I_t W_t^2\]
Source proof equation 3
\[W_t^2\le W_0^2\quad\Longrightarrow\quad K_t'\le-\frac{K_t^2}{2W_0^2}\]
Source proof equation 4
\[\frac1{K_h}\ge\frac1{K_0}+\frac{h}{2W_0^2}\]
Source proof equation 5
\[\frac1{K_{j+1}}\ge\frac1{K_j}+\frac{h}{W_0^2}\quad\Longrightarrow\quad K_n\le\frac{W_0^2}{nh}\]
Compiled bridge hypothesis
\[\frac{1}{K_j}+\frac{h}{R_0^2}\le\frac{1}{K_{j+1}}\qquad(j\ge0)\]
Compiled bridge conclusion
\[K_n\le\frac{R_0^2}{nh}\]
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-IDEAL-PROXIMAL-CHAIN · source snapshot 57687ebfab7f7301