Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Statistical Optimal Transport · Chapter 4
Entropic 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
\[\inf_{\gamma\in\Pi(\mu,\nu)}\left\{\int c\,d\gamma+\varepsilon\,\mathrm{KL}(\gamma\Vert\mu\otimes\nu)\right\}\]
The displayed relative-entropy convention must be checked against each pinned theorem. Positivity, finite partition functions, potentials modulo constants and marginal constraints are separate obligations. Reuse Gibbs variational and convex-duality ingredients with explicit adapters.
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
- §4.1 · Entropic regularization printed p. 110 / PDF p. 116
- §4.2 · Dual formulation printed p. 114 / PDF p. 120
- §4.3 · Estimating dual solutions printed p. 117 / PDF p. 123
- §4.4 · Estimating primal solutions printed p. 123 / PDF p. 129
- §4.5 · Discussion printed p. 129 / PDF p. 135
- §4.6 · Exercises printed p. 131 / PDF p. 137