Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Statistical Optimal Transport · Chapter 3
Estimation of transport maps
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
\[\mathcal S(\varphi)=\int\varphi\,d\mu+\int\varphi^*\,d\nu\]
Convex conjugacy produces the semidual; stability translates excess objective into map error only under the stated regularity and identifiability hypotheses. Share the convex core with optimization, not an unqualified strong-convexity claim about measures.
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
- §3.1 · Statistical model printed p. 89 / PDF p. 95
- §3.2 · Semidual stability printed p. 91 / PDF p. 97
- §3.3 · Affine example printed p. 94 / PDF p. 100
- §3.4 · Slow rates printed p. 95 / PDF p. 101
- §3.5 · Fixed-point argument printed p. 99 / PDF p. 105
- §3.6 · Fast rates printed p. 100 / PDF p. 106
- §3.7 · Discussion printed p. 104 / PDF p. 110
- §3.8 · Exercises printed p. 105 / PDF p. 111