Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Statistical Optimal Transport · Chapter 6
Wasserstein gradient flows: applications
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 F(\mu)=\int V\,d\mu+\lambda\operatorname{Ent}(\mu)\]
With entropy relative to Lebesgue measure, the gradient-flow interpretation leads to Fokker–Planck under appropriate regularity. Sampling, variational inference and particle systems have distinct targets; invariant laws, dissipation and discretization each need their own proof.
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
- §6.1 · Variational inference printed p. 167 / PDF p. 173
- §6.2 · Sampling printed p. 177 / PDF p. 183
- §6.3 · Interacting particles printed p. 187 / PDF p. 193
- §6.4 · Nonparametric likelihood printed p. 191 / PDF p. 197
- §6.5 · Mean-field networks printed p. 195 / PDF p. 201
- §6.6 · Transformers printed p. 197 / PDF p. 203
- §6.7 · Discussion printed p. 201 / PDF p. 207
- §6.8 · Exercises printed p. 203 / PDF p. 209