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

OpenAI Math routes for Riemannian Optimization

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 Riemannian Optimization All seven libraries

Extended chapters

  • E1 — Transport regularity on manifolds (Samplinglib extension; not a source-text chapter)
  • E2 — RCD and nonsmooth metric geometry (Samplinglib extension; not a source-text chapter)
7 mapped routes

Chapter and extension placement

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

  • 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.
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.
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.
Pinned upstream paths and provenance

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

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

  • 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