Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
upper · 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 4.3.6(1) (Durmus et al. 2019; weakly convex case)

Sinho Chewi, Log-Concave Sampling2026-08-09 edition
Theorem statement
\[\begin{gathered}0\preceq\nabla^2V\preceq\beta I_d,\qquad h\asymp\frac{\varepsilon^2}{\beta d},\qquad \bar\mu_{Nh}:=\frac1N\sum_{n=1}^N\widehat\mu_{nh},\\ \sqrt{\operatorname{KL}(\bar\mu_{Nh}\Vert\pi)}\le\varepsilon\quad\text{after}\quad N=O\!\left(\frac{\beta d\,W_2^2(\widehat\mu_0,\pi)}{\varepsilon^4}\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
\[2h\operatorname{KL}(\widehat\mu_{(n+1)h}\Vert\pi)\le W_2^2(\widehat\mu_{nh},\pi)-W_2^2(\widehat\mu_{(n+1)h},\pi)+2\beta dh^2\]

Lemma 4.3.4 is the one-step evolution variational inequality with discretization error when alpha=0.

02
\[\operatorname{KL}(\bar\mu_{Nh}\Vert\pi)\le\frac1N\sum_{n=1}^N\operatorname{KL}(\widehat\mu_{nh}\Vert\pi)\le\frac{W_2^2(\widehat\mu_0,\pi)}{2Nh}+\beta dh\]

Summing telescopes the Wasserstein terms; convexity of KL passes the average bound to the mixture output.

03
\[h\asymp\frac{\varepsilon^2}{\beta d},\qquad N=O\!\left(\frac{\beta d\,W_2^2(\widehat\mu_0,\pi)}{\varepsilon^4}\right)\]

The optimization term and discretization term are balanced at order epsilon squared.

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

  • The target is pi = exp(-V) with V normalized as in the source discussion.
  • For the displayed weakly convex specialization, V is convex and beta-smooth: 0 <= Hessian V <= beta I.
  • The initial law has finite W2 distance to the target.
  • The output is the uniform mixture of the first N LMC marginal laws, not just the final iterate.
ASTIS rigorous LaTeX
Theorem statement
\[\begin{gathered}0\preceq\nabla^2V\preceq\beta I_d,\qquad h\asymp\frac{\varepsilon^2}{\beta d},\qquad \bar\mu_{Nh}:=\frac1N\sum_{n=1}^N\widehat\mu_{nh},\\ \sqrt{\operatorname{KL}(\bar\mu_{Nh}\Vert\pi)}\le\varepsilon\quad\text{after}\quad N=O\!\left(\frac{\beta d\,W_2^2(\widehat\mu_0,\pi)}{\varepsilon^4}\right).\end{gathered}\]
Source proof equation 1
\[2h\operatorname{KL}(\widehat\mu_{(n+1)h}\Vert\pi)\le W_2^2(\widehat\mu_{nh},\pi)-W_2^2(\widehat\mu_{(n+1)h},\pi)+2\beta dh^2\]
Source proof equation 2
\[\operatorname{KL}(\bar\mu_{Nh}\Vert\pi)\le\frac1N\sum_{n=1}^N\operatorname{KL}(\widehat\mu_{nh}\Vert\pi)\le\frac{W_2^2(\widehat\mu_0,\pi)}{2Nh}+\beta dh\]
Source proof equation 3
\[h\asymp\frac{\varepsilon^2}{\beta d},\qquad N=O\!\left(\frac{\beta d\,W_2^2(\widehat\mu_0,\pi)}{\varepsilon^4}\right)\]
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-AVERAGED-LMC · source snapshot 7a02639c1661b25f