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

LMC Rényi interpolation

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 (2026), Theorem 6.1.2primary theorem audit in progress
Guarantee / accuracy
\[\sqrt{\mathcal R_q}\le\varepsilon\]
Complexity / rate
\[\widetilde O(\kappa^2dq\,\varepsilon^{-2}\log\mathcal R_2(\mu_0\Vert\pi))\]

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 · Rényi interpolation route

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

01

Interpolate the discrete LMC chain by a continuous process and differentiate a Rényi power functional.

02

Use LSI/hypercontractivity to absorb the Rényi-Fisher term and control the discretization contribution.

03

Run the source's waiting/interpolation phase to move from the initial order to the requested Rényi order.

\[\sqrt{\mathcal R_q}\le\varepsilon\]
04

Unroll the recursion and tune step size/time to obtain the displayed Rényi guarantee.

\[\widetilde O(\kappa^2dq\,\varepsilon^{-2}\log\mathcal R_2(\mu_0\Vert\pi))\]
Assumptions and implicit prerequisites

What must be true before the rate can be read

Model and geometry

  • The target has a smooth log-density; the cited theorem specifies the smoothness normalization.
  • A Poincaré or log-Sobolev inequality is assumed exactly where the cited result invokes it.
  • Initialization and warm-start quantities such as KL or Rényi divergence remain theorem-specific.

Case-specific qualifiers

  • Comparison-row qualifier: under LSI.

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
\[\sqrt{\mathcal R_q}\le\varepsilon\]
Complexity / rate
\[\widetilde O(\kappa^2dq\,\varepsilon^{-2}\log\mathcal R_2(\mu_0\Vert\pi))\]
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-FUNCTIONAL-INEQUALITY-SMOOTH-UPPER-LMC-R-NYI-INTERPOLATION · source snapshot 0273c4725e5e6b43