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

General first-order oracle lower bound

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

Chewi et al. (2023), query lower boundsprimary theorem audit in progress
Complexity / rate
\[\widetilde\Omega(\min\{\sqrt\kappa\log d,d\})\]

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 · Hard-instance and oracle-separation route

This is a source-linked reading map for Chewi et al. (2023), query lower bounds, not a transcription of the paper's proof. Exact source proof equations replace this map once theorem-level audit is complete.

01

Construct a family of targets satisfying the same model/regularity assumptions as the upper-bound problem.

02

Show that too few oracle queries cannot reliably distinguish the hard instances or locate the relevant geometry.

03

Translate indistinguishability into separation in the theorem's target accuracy metric.

04

Solve the resulting information/query inequality to obtain the displayed lower-bound scaling.

\[\widetilde\Omega(\min\{\sqrt\kappa\log d,d\})\]
Assumptions and implicit prerequisites

What must be true before the rate can be read

Model and geometry

  • The potential is strongly convex and smooth in the sense stated by the cited theorem.
  • The condition number is the source's ratio of smoothness to strong-convexity scales.
  • Warm-start assumptions are theorem-specific; when a result assumes bounded chi-squared divergence, that assumption is not hidden by the final TV guarantee.

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
Complexity / rate
\[\widetilde\Omega(\min\{\sqrt\kappa\log d,d\})\]
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-STRONGLY-LOG-CONCAVE-SMOOTH-BEST-LOWER-GENERAL-FIRST-ORDER-ORACLE-LOWER-BOUND · source snapshot f6b7a4718591927f