# Subpolynomial query complexity for log-concave sampling

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Subpolynomial query complexity for well-conditioned log-concave sampling](../../preprints/Subpolynomial-query-complexity-for-well-conditioned-log-concave-sampling-September-26-2026/article.pdf)

## Scope

The formalized result determines the dimension exponent of exact value-and-gradient query complexity for well-conditioned log-concave sampling. For potentials with $V(0)=0$, $\nabla V(0)=0$, and $I\le\nabla^2V\le2I$, the least worst-case query budget achieving total-variation error at most $1/10$ is at most $C_\varepsilon d^\varepsilon$ for every $\varepsilon>0$, and at least $c\log d$ eventually. Hence the infimal polynomial exponent is zero. Algorithms may be measurable, randomized, and adaptive; arithmetic and bit costs are not bounded.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Subpolynomial query complexity for log-concave sampling | [LogConcaveQuery.lean](../ComparatorChallenges/LogConcaveQuery.lean) |