Open problems
Sampling frontier
Literature-open mathematical questions are separated from results whose mathematics is known but whose Lean dependency graph is still incomplete.
Literature-open cases
lower unknown · Open problem
General sampling lower bound
Matching lower bound not currently known in the pinned literature trail
Matching result remains open.
lower unknown · Open problem
Matching PI/LSI oracle lower bound
Matching lower bound not currently known in the pinned literature trail
Matching result remains open.
lower unknown · Open problem
Matching Hölder-model lower bound
Matching lower bound not currently known in the pinned literature trail
Matching result remains open.
lower unknown · Open problem
Matching first-order lower bound
Matching lower bound not currently known in the pinned literature trail
Guarantee / accuracy
\[\operatorname{KL}\le\varepsilon^2\]
Formalization frontier
Ideal proximal chain
Theorem statement
Inspect exact open Lean interfaces →\[\operatorname{KL}(\mu_n^X\Vert\pi^X)\le \frac{W_2^2(\mu_0^X,\pi^X)}{nh}\]