Samplinglib
Lean gate not recorded for this source state main · ed709a7f320d
Statistical Optimal Transport · external extension shelf

OpenAI Math routes for Statistical Optimal Transport

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 Statistical Optimal Transport All seven libraries

Extended chapters

  • E1 — Regularity beyond the textbook spine (Samplinglib extension; not a source-text chapter)
11 mapped routes

Chapter and extension placement

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

  • 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

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

RCD heat-flow technical route

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

Samplinglib placement

  • 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

  • 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

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

  • Statistical Optimal Transport: Appendix B — The probability appendix is a reference surface, not a proof dependency.
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

  • 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

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

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