Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
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.11 (Durmus et al. 2019)

Sinho Chewi, Log-Concave Sampling2026-08-09 edition
Theorem statement
\[\begin{gathered}V\text{ is convex and }L\text{-Lipschitz},\qquad h\asymp\frac{\varepsilon^2}{L^2},\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{L^2W_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 by reduction in source; ASTIS expands the indicated telescoping step

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)+L^2h^2\]

Lemma 4.3.10 replaces the smooth discretization term by the bounded-subgradient/Lipschitz error.

02
\[\operatorname{KL}(\bar\mu_{Nh}\Vert\pi)\le\frac{W_2^2(\widehat\mu_0,\pi)}{2Nh}+\frac{L^2h}{2}\]

This is the telescoping-and-convexity calculation that the source says follows exactly as in Theorem 4.3.6(1).

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

Balancing the two terms yields the theorem's epsilon accuracy and iteration count.

Assumptions and implicit prerequisites

What must be true before the rate can be read

Model and geometry

  • The potential is convex and satisfies the weak/Hölder smoothness model of the cited theorem.
  • The Hölder exponent and constant are source parameters; ASTIS does not silently replace them by ordinary smoothness.
  • The initial transport scale and the requested KL accuracy are kept explicit in the rate.

Analytic / proof prerequisites

  • The target is pi = exp(-V).
  • V is convex and globally L-Lipschitz; differentiability/smoothness is not assumed for this theorem.
  • The LMC marginal laws and the uniform mixture output are defined as in Section 4.3.
  • The initial law has finite W2 distance to pi.
ASTIS rigorous LaTeX
Theorem statement
\[\begin{gathered}V\text{ is convex and }L\text{-Lipschitz},\qquad h\asymp\frac{\varepsilon^2}{L^2},\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{L^2W_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)+L^2h^2\]
Source proof equation 2
\[\operatorname{KL}(\bar\mu_{Nh}\Vert\pi)\le\frac{W_2^2(\widehat\mu_0,\pi)}{2Nh}+\frac{L^2h}{2}\]
Source proof equation 3
\[h\asymp\frac{\varepsilon^2}{L^2},\qquad N=O\!\left(\frac{L^2W_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-HOLDER-SMOOTH-LOG-CONCAVE-UPPER-AVERAGED-LMC · source snapshot babd7760e8082ef4