Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
best upper · Normalized SampleWiki statement

Proximal / In-and-Out with restart

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

Normalized SampleWiki statement

Primary theorem audit pending — this is not presented as a verbatim paper theorem

Kook–Vempala (2026), Theorem 1.1, v2primary theorem audit in progress
Guarantee / accuracy
\[\mathcal R_q\le\varepsilon\]
Complexity / rate
\[\widetilde O(qd^2\Lambda\log^6(1/\varepsilon))\]

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 theorem audit pending. The formulas below are the cleaned SampleWiki normalization of the cited result, not a claim of verbatim theorem transcription.

Proof / derivation

Reader derivation map · Geometry and annealing route

This is a source-linked reading map for Kook–Vempala (2026), Theorem 1.1, v2, not a transcription of the paper's proof. Exact source proof equations replace this map once theorem-level audit is complete.

01

Construct the source's warm-start or annealing path inside the convex-body membership model.

02

Control one transition/phase in the divergence used by the theorem.

03

Compose the phases or restart epochs while preserving the required warmness/geometric control.

\[\mathcal R_q\le\varepsilon\]
04

Choose the annealing and accuracy parameters to obtain the displayed membership-query complexity.

\[\widetilde O(qd^2\Lambda\log^6(1/\varepsilon))\]
Assumptions and implicit prerequisites

What must be true before the rate can be read

Model and geometry

  • The target is supported on a convex body and access is through the membership-oracle model fixed by the source setting.
  • Geometric quantities such as radius, warmness, and any Gaussian-annealing parameter keep the normalization used by the cited paper.
  • The displayed divergence/accuracy target is part of the theorem contract, not an interchangeable metric.

Analytic / proof prerequisites

  • Exact theorem-level parameter ranges and technical hypotheses remain controlled by the cited paper until primary-source audit is complete.
ASTIS rigorous LaTeX
Guarantee / accuracy
\[\mathcal R_q\le\varepsilon\]
Complexity / rate
\[\widetilde O(qd^2\Lambda\log^6(1/\varepsilon))\]
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-CONVEX-BODY-MEMBERSHIP-BEST-UPPER-PROXIMAL-IN-AND-OUT-WITH-RESTART · source snapshot 4ed82a9e159febc0