Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Statistical Optimal Transport · Chapter 1
Optimal transport
Stable source-facing chapter environment inside the shared Samplinglib reader.
scaffoldsource mapFull source closure not claimed
Planned route
Source → theorem map → reusable Lean nodes
Upstream alignment
Reuse the canonical convex, coupling, entropy and calculus interfaces. Local source availability is not yet a compatible Lean theorem.
Frontier Cells
Only genuinely missing mathematical edges become theorem-sized tasks.
Graph placement
Dependencies, consumers, cross-library bridges, and reusable shared interfaces.
Mathematical orientation
\[W_p(\mu,\nu)^p=\inf_{\gamma\in\Pi(\mu,\nu)}\int d(x,y)^p\,d\gamma(x,y)\]
The coupling set fixes both marginals. Separate finite-moment assumptions, existence of a minimizer, and the stronger hypotheses needed for a transport map. Reuse existing coupling and convex-potential interfaces before rebuilding them.
This is ASTIS orientation, not a verbatim source theorem or a completed formalization. Each theorem needs its own assumptions and source-to-Lean audit.
Section source map
- §1.1 · Transport problems printed p. 9 / PDF p. 15
- §1.2 · Wasserstein metrics printed p. 15 / PDF p. 21
- §1.3 · One-dimensional transport printed p. 21 / PDF p. 27
- §1.4 · Brenier maps printed p. 23 / PDF p. 29
- §1.5 · Kantorovich duality printed p. 29 / PDF p. 35
- §1.6 · The W1 dual printed p. 39 / PDF p. 45
- §1.7 · Discussion printed p. 42 / PDF p. 48
- §1.8 · Exercises printed p. 43 / PDF p. 49