Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
Statistical Optimal Transport Library

Statistical Optimal Transport

Sinho Chewi · Jonathan Niles-Weed · Philippe Rigollet. Eight chapters and two appendices in the shared Samplinglib reader.

Statuschapter environment established Primary source ↗
Formalization contract

Map first, reuse first, prove only real gaps.

Search Samplinglib, Mathlib and compatible formal upstreams first. Recover omitted details from Villani, Santambrogio and Ambrosio–Gigli–Savaré without silently changing the source theorem.

reuseadaptmissingout of scope
Book contents

Chapter scaffolds

01
scaffold

Optimal transport

Printed p. 9 · PDF p. 15 · source map and reuse audit; not a Lean closure.

A
scaffold

Convex analysis

Printed p. 247 · PDF p. 253 · source map and reuse audit; not a Lean closure.

B
scaffold

Probability

Printed p. 255 · PDF p. 261 · source map and reuse audit; not a Lean closure.

Dependency-first, not cover-to-cover.

Chapter 1 unlocks Chapters 2, 3, 4, 5 and 7; then 5 → 6 and 7 → 8. The book separates prerequisites from cross-references in Figure 0.1. Appendices A/B are shared-entry material, not a second convex/probability library.

Statistical Optimal Transport Route · Functor Hypergraph

Pagination audited on 5 September 2026. The public PDF is mutable; every claimed theorem must pin its edition and exact statement independently.