Samplinglib
Lean gate not recorded for this source state main · ed709a7f320d
SampleWiki · external extension shelf

OpenAI Math routes for SampleWiki

These routes are placed beside the chapters that can explain or consume them. They do not alter the primary source's chapter numbering, and they remain external until a reviewed ASTIS adapter or theorem compiles.

Back to SampleWiki All seven libraries

Extended chapters

  • E1 — External research frontiers and oracle models (Samplinglib extension; not a source-text chapter)
8 mapped routes

Chapter and extension placement

Comparator-backed upstream endpointOpenAI Math result 139

Subpolynomial query complexity for log-concave sampling

The exact value-and-gradient oracle model, deterministic query cap, TV 1/10 target, upper bound, and independent logarithmic lower bound must remain separate from runtime complexity.

Samplinglib placement

  • SampleWiki: Extended E1: External research frontiers and oracle models — This is a research-frontier source route, not a theorem of Chewi's textbook.
Pinned upstream paths and provenance

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Upstream Lean endpoints (external; not callable ASTIS dependencies)
  • OAI.LogConcaveSampling.exact_source_main
Manuscript only in this auditOpenAI Math result 093

Dimension-free logarithmic Sobolev inequality for subgaussian log-concave measures

Provenance only: no verified-Lean badge until an exact comparator-backed route or an ASTIS-owned proof exists.

Samplinglib placement

  • SampleWiki: Extended E1: External research frontiers and oracle models — It is a live functional-inequality frontier rather than completed ASTIS Lean.
Pinned upstream paths and provenance

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Comparator-backed upstream endpointOpenAI Math result 096

Gaussian propeller inequality

This is an external Gaussian partition theorem, not a generic Gaussian integration-by-parts or sampling lemma.

Samplinglib placement

  • SampleWiki: Extended E1: External research frontiers and oracle models — Its proof technology may seed future Gaussian extremal case studies.
Pinned upstream paths and provenance

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Upstream Lean endpoints (external; not callable ASTIS dependencies)
  • OAI.GaussianPropeller.all_partitions
Comparator linked by upstream result noteOpenAI Math result 374

Sharp one-third stability of Brenier maps

The upstream result page links a Comparator statement, but the audited formalization manifest does not name its solution declaration; ASTIS therefore does not upgrade it to comparator-backed.

Samplinglib placement

  • SampleWiki: Extended E1: External research frontiers and oracle models — The sharp exponent and counterexample form a useful research case.
Pinned upstream paths and provenance

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Comparator linked by upstream result noteOpenAI Math result 115

Exact sampling and approximate counting of contingency tables

Upstream documentation separates almost-sure exact sampling, bounded-time TV approximation and FPRAS counting; ASTIS must preserve all three cost/error contracts.

Samplinglib placement

  • SampleWiki: Extended E1: External research frontiers and oracle models — The algorithm/cost distinctions make a useful frontier case.
Pinned upstream paths and provenance

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Comparator linked by upstream result noteOpenAI Math result 231

Strongly Rayleigh laws, determinantal processes and IID factors

Negative-dependence infrastructure and the free uniform spanning forest result must remain distinguishable.

Samplinglib placement

  • SampleWiki: Extended E1: External research frontiers and oracle models — Equivariant IID sampling is a distinct frontier mechanism.
Pinned upstream paths and provenance

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Comparator-backed, partial familyOpenAI Math result 119

Courtade-Kumar and Hellinger information inequalities

Boolean-noise information inequalities are not interchangeable with KL/LSI statements for continuous Gibbs laws.

Samplinglib placement

  • SampleWiki: Extended E1: External research frontiers and oracle models — The extremal-information proof is a useful research case.
Pinned upstream paths and provenance

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Upstream Lean endpoints (external; not callable ASTIS dependencies)
  • OAI.LeanBlast.CourtadeKumar.courtadeKumarAndAttainment
Comparator-backed, partial familyOpenAI Math result 140

Memory-sample lower bounds for noiseless Gaussian regression

Posterior conditioning, projection moments, subsphere control and final memory-sample lower bounds form an AND-route; none should be displayed as the whole proof alone.

Samplinglib placement

  • SampleWiki: Extended E1: External research frontiers and oracle models — This is a canonical oracle/information lower-bound case study.
Pinned upstream paths and provenance

Apache-2.0 upstream snapshot adc7f1241b42e322a6451854ab7e4b4c146bf78a. Presence here is provenance, not local compilation.

Upstream Lean endpoints (external; not callable ASTIS dependencies)
  • OAI.MemoryPrecision.main
  • OAI.PosteriorReplicas.source_main
  • OAI.ProjectionMoments.main
  • OAI.SubsphereCurrent.full_current_main_scope