Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Statistical Optimal Transport · Chapter 5
Wasserstein gradient flows: theory
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
\[\partial_t\mu_t+\nabla\!\cdot(\mu_t v_t)=0\]
Transport velocities and metric derivatives connect probability laws with differential geometry. Otto calculus is not a blanket assertion that all Wasserstein space is a smooth manifold. For omitted analytic details, use Ambrosio–Gigli–Savaré with explicit weak-solution and absolute-continuity contracts.
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
- §5.1 · Continuity equation and speed printed p. 136 / PDF p. 142
- §5.2 · Riemannian prerequisites printed p. 141 / PDF p. 147
- §5.3 · Geometry of probability laws printed p. 143 / PDF p. 149
- §5.4 · Otto calculus printed p. 145 / PDF p. 151
- §5.5 · Gaussian covariance geometry printed p. 149 / PDF p. 155
- §5.6 · Mixture families printed p. 152 / PDF p. 158
- §5.7 · Transport and mass variation printed p. 154 / PDF p. 160
- §5.8 · Mean-field particles printed p. 159 / PDF p. 165
- §5.9 · Discussion printed p. 162 / PDF p. 168
- §5.10 · Exercises printed p. 163 / PDF p. 169