Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Statistical Optimal Transport · Appendix A
Convex analysis
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
\[\varphi^*(y)=\sup_x\{\langle x,y\rangle-\varphi(x)\}\]
This appendix is a reusable entry point shared with Chewi optimization. Keep finite-valued versus extended-real conventions explicit; reuse Mathlib and audited formal upstreams instead of adding a separate OT convex-analysis copy.
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
- §A.1 · Convexity and conjugates printed p. 247 / PDF p. 253
- §A.2 · Smoothness and strong convexity printed p. 250 / PDF p. 256
- §A.3 · Quadratic conjugates printed p. 253 / PDF p. 259