Samplinglib
Lean gate not recorded for this source state main · ed709a7f320d
Log-Concave Sampling · external extension shelf

OpenAI Math routes for Log-Concave Sampling

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 Log-Concave Sampling All seven libraries

Extended chapters

  • E1 — Convex geometry of log-concave laws (Samplinglib extension; not a source-text chapter)
  • E2 — Gaussian and information inequalities (Samplinglib extension; not a source-text chapter)
9 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

  • Log-Concave Sampling: Chapter 8, Chapter 9 — Proximal sampling supplies the upper-route interface; oracle lower bounds belong with the book's lower-bound chapter.
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

  • Log-Concave Sampling: Chapter 2 — The result belongs beside LSI and concentration, with its centered-density and subgaussian-marginal assumptions explicit.
Pinned upstream paths and provenance

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

Comparator-backed upstream endpointOpenAI Math result 087

Mahler conjectures and equality cases

Convex-body polarity and equality classifications are external source routes; they do not establish a sampling complexity bound.

Samplinglib placement

  • Log-Concave Sampling: Extended E1: Convex geometry of log-concave laws — Convex bodies, polarity and log-concave geometry support the geometric background but are outside the book spine.
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.SymmetricMahler.symmetric_mahler
  • OAI.SymmetricMahler.symmetric_mahler_equality
Comparator-backed, partial familyOpenAI Math result 088

Projection-body inequalities and simplex counterexamples

The comparator endpoints cover named projection-volume claims, not every manuscript statement in the family.

Samplinglib placement

  • Log-Concave Sampling: Extended E1: Convex geometry of log-concave laws — Projection bodies are supporting convex geometry, not part of the primary sampling text.
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.PettyProjection.petty_projection_volume
  • OAI.Paper092.product_counterexample
Comparator-backed, partial familyOpenAI Math result 091

Logarithmic Brunn-Minkowski and the B-conjecture

Keep the precise symmetry, measure and convex-body hypotheses; the family name is not a generic log-concavity theorem.

Samplinglib placement

  • Log-Concave Sampling: Chapter 2, Extended E1: Convex geometry of log-concave laws — The B-conjecture and log-concave geometry extend concentration/functional-inequality context.
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.LogBrunnMinkowski.main
Comparator-backed, partial familyOpenAI Math result 092

Convex-body covering density

Only the exact comparator endpoint is verification evidence; the full covering-density family has a wider manuscript scope.

Samplinglib placement

  • Log-Concave Sampling: Extended E1: Convex geometry of log-concave laws — A convex-geometry extension can expose the result without pretending it is used by the sampling text.
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.SingleLatticeCovering.single_lattice_covering
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

  • Log-Concave Sampling: Extended E2: Gaussian and information inequalities — It belongs in a Gaussian-inequalities extension with no implied dependency from the 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.GaussianPropeller.all_partitions
Manuscript only in this auditOpenAI Math result 101

Sharp simplex conjecture and entropy bound for log-concave densities

The catalogue records no comparator-backed main result for this family in the audited manifest.

Samplinglib placement

  • Log-Concave Sampling: Extended E1: Convex geometry of log-concave laws — Isotropic constants and entropy of log-concave laws are direct geometric background outside the textbook spine.
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

  • Log-Concave Sampling: Extended E2: Gaussian and information inequalities — This is an information-inequality comparison point outside the continuous book.
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