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

LMC

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 4.2.6 (Vempala–Wibisono 2019; current Chewi numbering)

Sinho Chewi, Log-Concave Sampling2026-08-09 edition
Theorem statement
\[\begin{gathered}C_{\mathrm{LSI}}(\pi)\le \alpha^{-1},\quad \nabla V\text{ is }\beta\text{-Lipschitz},\quad h\le (4\beta)^{-1},\\ \operatorname{KL}(\widehat\mu_{Nh}\Vert\pi)\le e^{-\alpha Nh}\operatorname{KL}(\widehat\mu_0\Vert\pi)+O\!\left(\frac{\beta^2dh}{\alpha}\right).\end{gathered}\]

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\operatorname{KL}(\widehat\mu_t\Vert\pi)\le-\tfrac12\operatorname{FI}(\widehat\mu_t\Vert\pi)+6\beta^2dh\]

The frozen-drift LMC interpolation dissipates KL up to the discretization error.

02
\[-\tfrac12\operatorname{FI}(\widehat\mu_t\Vert\pi)\le-\alpha\operatorname{KL}(\widehat\mu_t\Vert\pi)\]

The log-Sobolev inequality converts Fisher-information dissipation into KL contraction.

03
\[\operatorname{KL}(\widehat\mu_{Nh}\Vert\pi)\le e^{-\alpha Nh}\operatorname{KL}(\widehat\mu_0\Vert\pi)+O\!\left(\frac{\beta^2dh}{\alpha}\right)\]

Integrating the scalar differential inequality separates mixing from discretization bias.

04
\[h\asymp\frac{\varepsilon^2}{\beta\kappa d},\qquad N=O\!\left(\frac{\kappa^2d}{\varepsilon^2}\log\frac{\operatorname{KL}(\widehat\mu_0\Vert\pi)}{\varepsilon^2}\right),\quad \kappa=\beta/\alpha\]

Balancing the stationary discretization term against the target KL accuracy gives the advertised iteration complexity.

Assumptions and implicit prerequisites

What must be true before the rate can be read

Model and geometry

  • The target has a smooth log-density; the cited theorem specifies the smoothness normalization.
  • A Poincaré or log-Sobolev inequality is assumed exactly where the cited result invokes it.
  • Initialization and warm-start quantities such as KL or Rényi divergence remain theorem-specific.

Case-specific qualifiers

  • Comparison-row qualifier: under LSI.

Analytic / proof prerequisites

  • The target has density proportional to exp(-V).
  • The target satisfies a log-Sobolev inequality with constant at most 1/alpha.
  • The gradient of V is beta-Lipschitz and the LMC step size obeys h <= 1/(4 beta).
  • The complexity specialization uses kappa = beta/alpha and the source's stated epsilon range.
ASTIS rigorous LaTeX
Theorem statement
\[\begin{gathered}C_{\mathrm{LSI}}(\pi)\le \alpha^{-1},\quad \nabla V\text{ is }\beta\text{-Lipschitz},\quad h\le (4\beta)^{-1},\\ \operatorname{KL}(\widehat\mu_{Nh}\Vert\pi)\le e^{-\alpha Nh}\operatorname{KL}(\widehat\mu_0\Vert\pi)+O\!\left(\frac{\beta^2dh}{\alpha}\right).\end{gathered}\]
Source proof equation 1
\[\partial_t\operatorname{KL}(\widehat\mu_t\Vert\pi)\le-\tfrac12\operatorname{FI}(\widehat\mu_t\Vert\pi)+6\beta^2dh\]
Source proof equation 2
\[-\tfrac12\operatorname{FI}(\widehat\mu_t\Vert\pi)\le-\alpha\operatorname{KL}(\widehat\mu_t\Vert\pi)\]
Source proof equation 3
\[\operatorname{KL}(\widehat\mu_{Nh}\Vert\pi)\le e^{-\alpha Nh}\operatorname{KL}(\widehat\mu_0\Vert\pi)+O\!\left(\frac{\beta^2dh}{\alpha}\right)\]
Source proof equation 4
\[h\asymp\frac{\varepsilon^2}{\beta\kappa d},\qquad N=O\!\left(\frac{\kappa^2d}{\varepsilon^2}\log\frac{\operatorname{KL}(\widehat\mu_0\Vert\pi)}{\varepsilon^2}\right),\quad \kappa=\beta/\alpha\]
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-FUNCTIONAL-INEQUALITY-SMOOTH-UPPER-LMC · source snapshot 9d98df6c5e8496bb