Source audit
Definitions, theorems, assumptions, proof route, and exact anchors.
Statistical Optimal Transport · Chapter 8
Wasserstein barycenters
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 B(\mu)=\frac12\int W_2(\mu,\nu)^2\,d\mathbb P(\nu)\]
A distribution over probability measures defines a Fréchet objective. Existence, uniqueness and statistical estimation are separate questions. Compare with Euclidean quadratic minimization only after specifying the geometry and variance inequality.
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
- §8.1 · Hilbert-space model printed p. 231 / PDF p. 237
- §8.2 · Positive-curvature setting printed p. 233 / PDF p. 239
- §8.3 · Parametric statistical rates printed p. 240 / PDF p. 246
- §8.4 · Discussion printed p. 243 / PDF p. 249
- §8.5 · Exercises printed p. 244 / PDF p. 250