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

Averaged 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 11.2.1

Sinho Chewi, Log-Concave Sampling; theorem attributed to Balasubramanian et al. (2022)2026-08-09 book edition
Theorem statement
\[\frac1{Nh}\int_0^{Nh}\mathrm{FI}(\widehat\mu_t\Vert\pi)\,dt\le\frac{2\mathrm{KL}(\widehat\mu_0\Vert\pi)}{Nh}+6\beta^2dh\]

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 Chewi

01
\[\partial_t\mathrm{KL}(\widehat\mu_t\Vert\pi)\le-\tfrac12\mathrm{FI}(\widehat\mu_t\Vert\pi)+6\beta^2d(t-nh)\]

Reuse the LMC interpolation estimate from the proof of Theorem 4.2.7.

02
\[\mathrm{KL}_{n+1}-\mathrm{KL}_n\le-\tfrac12\int_{nh}^{(n+1)h}\mathrm{FI}_t\,dt+3\beta^2dh^2\]

Integrate over one LMC step.

03
\[\frac1{Nh}\int_0^{Nh}\mathrm{FI}_t\,dt\le\frac{2\mathrm{KL}_0}{Nh}+6\beta^2dh\]

Telescope over n=0,...,N-1.

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.

Case-specific qualifiers

  • Comparison-row qualifier: on average.

Analytic / proof prerequisites

  • relative Fisher information
  • Chewi Theorem 4.2.7 interpolation/dissipation estimate
  • finite telescoping and integration
ASTIS rigorous LaTeX
Theorem statement
\[\frac1{Nh}\int_0^{Nh}\mathrm{FI}(\widehat\mu_t\Vert\pi)\,dt\le\frac{2\mathrm{KL}(\widehat\mu_0\Vert\pi)}{Nh}+6\beta^2dh\]
Source proof equation 1
\[\partial_t\mathrm{KL}(\widehat\mu_t\Vert\pi)\le-\tfrac12\mathrm{FI}(\widehat\mu_t\Vert\pi)+6\beta^2d(t-nh)\]
Source proof equation 2
\[\mathrm{KL}_{n+1}-\mathrm{KL}_n\le-\tfrac12\int_{nh}^{(n+1)h}\mathrm{FI}_t\,dt+3\beta^2dh^2\]
Source proof equation 3
\[\frac1{Nh}\int_0^{Nh}\mathrm{FI}_t\,dt\le\frac{2\mathrm{KL}_0}{Nh}+6\beta^2dh\]
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-UPPER-LOWER-AVERAGED-LMC · source snapshot e5f29efb15b8ac6c