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

OpenAI Math routes for Optimisation

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 Optimisation All seven libraries

Extended chapters

  • E1 — Convex geometry, vector balancing and fixed points (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

  • Optimisation: Chapter 4, Chapter 8 — The exact oracle and proximal interfaces align with lower-bound and proximal-method chapters without becoming optimisation theorems.
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
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

  • Optimisation: Chapter 1, Chapter 9 — Convexity and polarity connect to convex foundations and duality, with no algorithmic convergence claim.
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

  • Optimisation: Extended E1: Convex geometry, vector balancing and fixed points — The family belongs in the convex-geometry extension rather than an algorithm 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.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

  • Optimisation: Chapter 1 — This supplies convex-geometric examples, not an optimisation method.
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

  • Optimisation: Extended E1: Convex geometry, vector balancing and fixed points — Covering and volumetric techniques belong in the convex-geometry extension.
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 097

Euclidean Steinitz-Bergstrom theorem

Vector balancing is relevant proof technology but is not a first-order optimisation convergence theorem.

Samplinglib placement

  • Optimisation: Chapter 6, Extended E1: Convex geometry, vector balancing and fixed points — Vector balancing is best presented beside nonsmooth convex geometry as an explicit extension.
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.EuclideanSteinitzBergstrom.main
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

  • Optimisation: Chapter 4 — The information model is relevant to lower-bound methodology but is not Chewi's smooth-optimisation oracle theorem.
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
Comparator-backed upstream endpointOpenAI Math result 328

Fixed points of nonexpansive maps in reflexive Banach spaces

The fixed-point theorem is reusable analysis, not convergence of a named optimisation algorithm without a verified iteration adapter.

Samplinglib placement

  • Optimisation: Chapter 2, Chapter 11, Extended E1: Convex geometry, vector balancing and fixed points — Gradient-flow and alternating/fixed-point viewpoints are the closest teaching locations.
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.ReflexiveFixedPoints.exists_fixedPoint_of_canonicallyReflexive