Samplinglib
Lean gate not recorded for this source state main · ed709a7f320d
External proof memory · seven-library coverage

OpenAI Math intake map

A pinned, truth-preserving map from relevant OpenAI Math result families into Samplinglib's seven textbook and research libraries. It tells readers where a route belongs without claiming that upstream Lean is ASTIS-owned Lean.

32 domain routes7 libraries372 upstream families audited185 manifest endpoints inspected

Pinned upstream snapshot Attribution and licenses

How to read the status

Every card is an external reference. Comparator-backed means that a named endpoint is exposed by the audited upstream verification material; it does not create a solid edge in Samplinglib's Lean graph. Only an ASTIS-owned declaration that compiles locally may become blue.

Place by consumer, not keyword

Seven library shelves

Log-Concave Sampling9 mapped routesSampleWiki8 mapped routesRiemannian Optimization7 mapped routesOptimisation8 mapped routesStatistical Optimal Transport11 mapped routesDiscrete Sampling11 mapped routesMarkov Chain Monte Carlo8 mapped routes
Audited domain sweep

Relevant result and substrate routes

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

  • Log-Concave Sampling: Chapter 2 — The result belongs beside LSI and concentration, with its centered-density and subgaussian-marginal assumptions explicit.
  • 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 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.
  • 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

  • Log-Concave Sampling: Extended E1: Convex geometry of log-concave laws — Projection bodies are supporting convex geometry, not part of the primary sampling text.
  • 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

  • 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.
  • 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

  • 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.
  • 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 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.
  • 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-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
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.
  • Statistical Optimal Transport: Appendix B — The probability appendix is the natural cross-reference, not evidence of an OT theorem.
Pinned upstream paths and provenance

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

Comparator-backed upstream endpointOpenAI Math result 360

Weak MTW curvature, injectivity-domain convexity and transport regularity

Weak MTW, sectional/Ricci curvature, geodesic convexity and displacement convexity remain distinct predicates.

Samplinglib placement

  • Riemannian Optimization: Chapter 8, Chapter 10, Chapter 11 — The manifold, geodesic and curvature interfaces fit these chapters; the transport conclusion remains external.
  • Statistical Optimal Transport: Chapter 1, Chapter 3, Chapter 7 — Squared-distance cost geometry, map regularity and Wasserstein geometry meet here.
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.WeakMTWGlobalSupport.current_main_convexity
Comparator-backed upstream endpointOpenAI Math result 360

Uniform bi-Holder regularity of transport

This is a source-specific regularity endpoint and needs adapters before it can consume ASTIS transport definitions.

Samplinglib placement

  • Statistical Optimal Transport: Chapter 3, Chapter 7, Extended E1: Regularity beyond the textbook spine — Map estimation and Wasserstein geometry are its nearest textbook consumers.
  • Riemannian Optimization: Extended E1: Transport regularity on manifolds — The manifold geometry is supporting substrate, not an optimisation conclusion.
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.WeakMTWTransport.uniform_biHolder_transport
Lean present; Comparator audit pendingOpenAI Math result technical substrate

Riemannian harmonic and geodesic technical substrate

A reusable-candidate directory, not one sealed paper theorem; every promoted declaration requires its own semantic audit.

Samplinglib placement

  • Riemannian Optimization: Chapter 8, Chapter 10 — General-manifold and additional-tool chapters are the honest audit locations.
Pinned upstream paths and provenance

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

Lean present; Comparator audit pendingOpenAI Math result 356

RCD heat-flow technical route

Candidate metric-measure infrastructure; no source theorem is locally admitted merely because files exist.

Samplinglib placement

  • Riemannian Optimization: Extended E2: RCD and nonsmooth metric geometry — Nonsmooth RCD geometry is outside Boumal's smooth-manifold spine.
  • Statistical Optimal Transport: Chapter 5, Chapter 7, Extended E1: Regularity beyond the textbook spine — Heat flow and metric geometry are the closest OT locations.
Pinned upstream paths and provenance

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

Comparator-backed upstream endpointOpenAI Math result 356

Weak Hessian bounds along every geodesic in RCD spaces

The weak distributional Hessian and RCD hypotheses cannot be replaced by a smooth Riemannian Hessian bound.

Samplinglib placement

  • Riemannian Optimization: Extended E2: RCD and nonsmooth metric geometry — This is a nonsmooth extension, not a theorem of the smooth optimisation text.
  • Statistical Optimal Transport: Chapter 5, Chapter 7, Extended E1: Regularity beyond the textbook spine — Geodesic inequalities and metric-measure flow are the natural OT bridge.
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.WeakHessian.every_geodesic
Manuscript only in this auditOpenAI Math result 357

Bi-Lipschitz coordinates at regular RCD points

The audited formalization manifest does not list a comparator-backed main result for this family.

Samplinglib placement

  • Riemannian Optimization: Extended E2: RCD and nonsmooth metric geometry — This is nonsmooth metric geometry beyond the primary source.
  • Statistical Optimal Transport: Chapter 7, Extended E1: Regularity beyond the textbook spine — Metric-space geometry is the closest textbook placement.
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 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

  • Statistical Optimal Transport: Chapter 3, Extended E1: Regularity beyond the textbook spine — Stability of estimated Brenier maps directly extends the transport-map estimation chapter.
  • 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-backed upstream endpointOpenAI Math result 238

Binary-sweep contraction and mixing

A discrete finite-chain theorem; no Langevin/SDE interpretation is inferred.

Samplinglib placement

  • Discrete Sampling: Chapter 3, Chapter 6, Extended E1: Card shuffles and deterministic sweeps — Kernel mixing foundations and an explicit shuffle extension meet here.
  • Markov Chain Monte Carlo: Chapter 2, Extended E2: Discrete chains beyond the source text — Reversible-chain contraction belongs to the method view, with discrete state explicit.
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.binary_sweep_contraction_and_mixing
Comparator-backed, partial familyOpenAI Math result 238

Conditional information under coordinate sweeps

Conditional-information endpoints do not by themselves prove the entire Thorp mixing family.

Samplinglib placement

  • Discrete Sampling: Chapter 3, Extended E1: Card shuffles and deterministic sweeps — Conditional resampling and sweep composition extend the kernel foundations.
  • Markov Chain Monte Carlo: Chapter 2, Extended E2: Discrete chains beyond the source text — Systematic scans are an MCMC mechanism, but this route is a card-shuffle source 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.CoordinateSweeps.conditional_main
  • OAI.CoordinateSweeps.all_grid_moment
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

  • Discrete Sampling: Extended E2: Exact sampling, approximate counting and IID factors — Exact combinatorial sampling and counting are outside the source textbook's spin/matroid spine.
  • 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-backed upstream endpointOpenAI Math result 131

Rapid mixing of graph switches

Connectivity, spectral/comparison estimates and TV mixing remain separate proof obligations.

Samplinglib placement

  • Discrete Sampling: Chapter 3, Chapter 4, Extended E2: Exact sampling, approximate counting and IID factors — Finite-chain foundations and comparison-based rapid mixing are the closest source chapters.
  • Markov Chain Monte Carlo: Chapter 2, Extended E2: Discrete chains beyond the source text — The switch chain is a reversible MCMC 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.Problem315.switch_chain_main
  • OAI.Problem315.switch_chain_tv_bound
  • OAI.Problem315.switch_connectivity
Comparator-backed, partial familyOpenAI Math result 238

Optimal logarithmic mixing of the Thorp shuffle

The family has multiple comparator endpoints; routing, compatibility, energy decay and final mixing must not be flattened into one implication.

Samplinglib placement

  • Discrete Sampling: Chapter 3, Extended E1: Card shuffles and deterministic sweeps — This is the dedicated card-shuffle extension after finite-chain foundations.
  • Markov Chain Monte Carlo: Chapter 2, Extended E2: Discrete chains beyond the source text — It illustrates mixing analysis outside the MCMC source 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.Thorp.Current.first_reciprocal_main
  • OAI.ThorpResults.remaining_main
  • OAI.ThorpNine.main
  • OAI.ThorpCompatibility.weightedCompatibility_main
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

  • Discrete Sampling: Chapter 7, Extended E2: Exact sampling, approximate counting and IID factors — Strong Rayleigh structure directly extends the matroid/negative-dependence route.
  • 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 upstream endpointOpenAI Math result 227

Critical SK heat-bath/Glauber mixing

Spin-glass-specific hypotheses are source binders; generic Dirichlet, entropy or TV leaves may be extracted only after audit.

Samplinglib placement

  • Discrete Sampling: Chapter 3, Chapter 6, Chapter 10, Chapter 12 — Glauber dynamics, optimal mixing, critical-point analysis and spin systems all participate.
  • Markov Chain Monte Carlo: Chapter 2, Chapter 5, Extended E2: Discrete chains beyond the source text — The heat-bath chain belongs to reversible/continuous-time MCMC with a discrete target.
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.CriticalSK.critical_mixing_bounds
Comparator-backed, partial familyOpenAI Math result 113

Perfect-matching entropy and approximate counting

The named entropy endpoint does not certify the complete FPRAS paper family.

Samplinglib placement

  • Discrete Sampling: Chapter 7, Extended E2: Exact sampling, approximate counting and IID factors — Matching laws and entropy sit beside matroid/negative-dependence tools, while counting remains an 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.MatchingEntropy.entropy_main
Comparator-backed, partial familyOpenAI Math result 114

FPRAS for common matroid bases

The formal endpoint covers equal-rank matroid bases with explicit oracle and error contracts, not the entire integer-polymatroid family.

Samplinglib placement

  • Discrete Sampling: Chapter 7, Extended E2: Exact sampling, approximate counting and IID factors — The theorem directly extends the source's matroid chapter into approximate counting.
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.common_bases_fpras
Comparator linked by upstream result noteOpenAI Math result 229

Three-state reconstruction above the Kesten-Stigum threshold

Upstream Lean covers only the supercritical direction; non-reconstruction, equality and stochastic-block-model consequences remain outside the selected statements.

Samplinglib placement

  • Discrete Sampling: Chapter 9, Chapter 12, Extended E2: Exact sampling, approximate counting and IID factors — Tree recursions and spin-system thresholds are the closest source route.
  • Markov Chain Monte Carlo: Extended E2: Discrete chains beyond the source text — This is a discrete probabilistic threshold, not automatically an MCMC mixing theorem.
Pinned upstream paths and provenance

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

Comparator-backed upstream endpointOpenAI Math result 236

Factor-of-IID threshold for free Ising spins on trees

Finitary coding and coding-radius bounds are explicitly outside the upstream formalized endpoint.

Samplinglib placement

  • Discrete Sampling: Chapter 12, Extended E2: Exact sampling, approximate counting and IID factors — The Ising source chapter is the natural anchor; IID-factor semantics are an 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.Problem367.free_ising_factor_iff_threshold
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.
  • Statistical Optimal Transport: Appendix B — The probability appendix is a reference surface, not a proof dependency.
  • 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.
  • Optimisation: Chapter 4 — The information model is relevant to lower-bound methodology but is not Chewi's smooth-optimisation oracle theorem.
  • Statistical Optimal Transport: Chapter 2, Appendix B — Statistical estimation and Gaussian probability are the closest reference points.
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 327

Markov type characterizes superreflexivity

Markov type is metric/Banach geometry of chains; it is not an invariant-law or convergence theorem for an arbitrary MCMC kernel.

Samplinglib placement

  • Markov Chain Monte Carlo: Extended E1: Metric geometry of Markov chains — The metric geometry of chains deserves a separate extension rather than insertion into the applied source text.
  • Statistical Optimal Transport: Chapter 7, Extended E1: Regularity beyond the textbook spine — Metric geometry is the genuine bridge to Wasserstein-space geometry.
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.MarkovSuperreflexivity.hasNontrivialMarkovType_iff_hasEquivalentUCNorm
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.
  • Riemannian Optimization: Extended E1: Transport regularity on manifolds — No manifold fixed-point transport is asserted without an adapter.
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
Manuscript only in this auditOpenAI Math result 332

Metric Markov cotype two for l1

No result-specific Lean document or comparator-backed endpoint was found in the audited snapshot.

Samplinglib placement

  • Markov Chain Monte Carlo: Extended E1: Metric geometry of Markov chains — It belongs beside Markov type as metric chain geometry, not as a standard MCMC result.
  • Statistical Optimal Transport: Chapter 7, Extended E1: Regularity beyond the textbook spine — The bridge is metric-geometric and remains conceptual.
Pinned upstream paths and provenance

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

Negative classification evidence

Similar words do not imply the same mathematics

  • 145. Rokhlin multiple mixing — Ergodic-theory mixing is not Markov-chain mixing merely because the word mixing appears.
  • 150. Weak mixing of triangular billiards — Dynamical weak mixing is outside the seven current library spines.
  • 211. Random planar maps — Diffusion and spectra in random geometry have no current textbook consumer.
  • 220. Random-environment ballisticity — A random walk in random environment is not automatically an MCMC method route.
  • 221. Mezard-Parisi formula — Spin-glass free-energy structure is background only until a concrete discrete-sampling consumer is named.
  • 273. Entropy photon-number inequality — Quantum information entropy is not the KL/LSI entropy used by the sampling routes.