1.3 · Book p. 19 · PDF p. 31

The Geometry of Optimal Transport

Develops couplings and Wasserstein distance as geometry on probability laws, preparing metric contraction arguments for diffusions.

Open this section in the canonical August 9 source ↗

Definition 1.3.16

Informally, a curve is absolutely continuous when its finite metric derivative exists almost everywhere.

\[|\dot\mu_t|:=\lim_{h\to0}\frac{W_2(\mu_{t+h},\mu_t)}{|h|}\quad\text{for a.e. }t\]

The metric derivative is the punctured-time limit of distance(curve(s),curve(t))/abs(s-t).

Why is this valid?

The a.e. time quantifier, punctured neighborhood, nonnegative finite speed, and real Lebesgue measure are explicit.

Source assumptions

a curve in Wasserstein P2ac
the informal metric derivative criterion

Formal assumptions

a PseudoMetricSpace
a real-time curve
a.e. existence of HasMetricDerivativeAt

View Lean formalization

compiled · faithful paraphrase

ASTIS formalizes exactly the source's informal criterion on a generic pseudometric space without introducing a tangent vector.

`AutoSamplingTheory.TechnicalLemmas.Geometry.MetricCurve.IsAbsolutelyContinuousMetricCurve`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/Geometry/MetricCurve.lean:34

def IsAbsolutelyContinuousMetricCurve
    {M : Type*} [PseudoMetricSpace M]
    (curve : ℝ → M) : Prop :=
  ∀ᵐ t ∂(by volume_tac : Measure ℝ),
    ∃ speed : ℝ, HasMetricDerivativeAt curve speed t

end MetricCurve
end Geometry
end TechnicalLemmas
end AutoSamplingTheory

Imports

Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Mathlib.Topology.MetricSpace.Basic

Local dependencies

No Registry dependency inferred.

Downstream consumers

continuity equation
kinetic action
Wasserstein geodesics

Definition 1.3.26

A functional is alpha-geodesically convex when its value along each geodesic lies below endpoint interpolation minus the alpha quadratic distance correction.

\[\mathcal F(\mu_t)\le(1-t)\mathcal F(\mu_0)+t\mathcal F(\mu_1)-\frac{\alpha}{2}t(1-t)W_2^2(\mu_0,\mu_1)\]

For t in [0,1], F(p_t) is at most (1-t)F(p_0)+tF(p_1)-alpha t(1-t)d(p_0,p_1)^2/2.

Why is this valid?

The ambient metric, complete path, geodesic selection, interval membership, coefficient normalization, and endpoint distance are explicit.

Source assumptions

a Riemannian manifold
smooth functional
all geodesics

Formal assumptions

a MetricSpace
an explicit geodesic predicate
real-valued functional

View Lean formalization

compiled · faithful paraphrase

ASTIS chooses the first of the source's equivalent conditions and parameterizes the predicate selecting geodesics.

`AutoSamplingTheory.TechnicalLemmas.Geometry.GeodesicConvexity.IsAlphaGeodesicallyConvex`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/Geometry/GeodesicConvexity.lean:23

def IsAlphaGeodesicallyConvex
    {M : Type*} [MetricSpace M]
    (isGeodesic : (ℝ → M) → Prop) (F : M → ℝ) (alpha : ℝ) : Prop :=
  ∀ path : ℝ → M, isGeodesic path →
    ∀ t : ℝ, t ∈ Icc (0 : ℝ) 1 →
      F (path t) ≤
        (1 - t) * F (path 0) + t * F (path 1) -
          (alpha * t * (1 - t) / 2) * dist (path 0) (path 1) ^ 2

/-- The chord formulation of geodesic alpha-convexity implies its first-order
form along a differentiable selected geodesic.  The scalar
`gradientPairing` is the derivative of `F` along the path at its initial
point; identifying it with the Riemannian or Wasserstein gradient pairing is
a separate geometric theorem.

This is the one-dimensional limiting argument behind Chewi display
(1.4.7). -/

Imports

Mathlib.Analysis.Calculus.Deriv.Slope
Mathlib.Topology.MetricSpace.Basic

Local dependencies

No Registry dependency inferred.

Downstream consumers

Wasserstein KL convexity
gradient-flow convergence

Definition 1.3.6

The dual optimal transport value is the supremum of the two potential integrals over feasible integrable potential pairs.

\[\mathcal D_c(\mu,\nu):=\sup_{f(x)+g(y)\le c(x,y)}\left\{\int f\,d\mu+\int g\,d\nu\right\}\]

Dual feasibility requires f(x)+g(y) to be at most the transport cost for mu-times-nu almost every pair.

Why is this valid?

The generic real-cost definition does not silently assume strong duality, boundedness, or attainment.

Source assumptions

finite-second-moment probability marginals
quadratic cost

Formal assumptions

measurable spaces and measures
integrable real potentials
product-a.e. dual constraint

View Lean formalization

compiled · faithful paraphrase

ASTIS keeps both integrability requirements and the product-measure a.e. constraint in the feasible predicate.

`AutoSamplingTheory.TechnicalLemmas.Measure.KantorovichDual.dualTransportValue`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/Measure/KantorovichDual.lean:32

noncomputable def dualTransportValue
    {E F : Type*} [MeasurableSpace E] [MeasurableSpace F]
    (cost : E × F → ℝ) (mu : Measure E) (nu : Measure F) : ℝ :=
  sSup {r : ℝ | ∃ (f : E → ℝ) (g : F → ℝ),
    DualFeasible cost mu nu f g ∧
      r = (∫ x, f x ∂mu) + ∫ y, g y ∂nu}

/-- Chewi display (1.3.7): source-facing expansion of the dual value. -/

Imports

Mathlib.MeasureTheory.Integral.Bochner.Basic
Mathlib.MeasureTheory.Measure.Prod

Local dependencies

No Registry dependency inferred.

Downstream consumers

Kantorovich strong duality
optimal maps

Displayed identity (1.3.7)

The dual value is the supremum of integral f dmu plus integral g dnu over dual-feasible potentials.

\[\mathcal D_c(\mu,\nu)=\sup\left\{\int f\,d\mu+\int g\,d\nu:\ f\oplus g\le c\right\}\]

This display expands the optimization objective and feasible set used by Definition 1.3.6.

Why is this valid?

Only the dual value is expanded; equality to one half W2 squared is not claimed here.

Source assumptions

Definition 1.3.6

Formal assumptions

dualTransportValue and DualFeasible

View Lean formalization

compiled · faithful paraphrase

The source display is a proved definitional expansion rather than an assumed primal-dual theorem.

`AutoSamplingTheory.TechnicalLemmas.Measure.KantorovichDual.dualTransportValue_eq_sSup`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/Measure/KantorovichDual.lean:40

theorem dualTransportValue_eq_sSup
    {E F : Type*} [MeasurableSpace E] [MeasurableSpace F]
    (cost : E × F → ℝ) (mu : Measure E) (nu : Measure F) :
    dualTransportValue cost mu nu =
      sSup {r : ℝ | ∃ (f : E → ℝ) (g : F → ℝ),
        DualFeasible cost mu nu f g ∧
          r = (∫ x, f x ∂mu) + ∫ y, g y ∂nu} :=
  rfl

end KantorovichDual
end Measure
end TechnicalLemmas
end AutoSamplingTheory

Imports

Mathlib.MeasureTheory.Integral.Bochner.Basic
Mathlib.MeasureTheory.Measure.Prod

Local dependencies

dualTransportValue

Downstream consumers

weak duality
strong duality

Definition 1.3.4

The 2-Wasserstein distance is the positive square root of the optimal quadratic coupling cost.

\[W_2(\mu,\nu):=\left(\inf_{\gamma\in\Pi(\mu,\nu)}\int\|x-y\|^2\,d\gamma(x,y)\right)^{1/2}\]

W2(mu,nu) is the square root of the infimum over couplings of the integral of the squared Euclidean distance.

Why is this valid?

The state space is a measurable real normed additive group, the cost is ENNReal.ofReal of squared norm, and infinite values remain representable.

Source assumptions

probability measures on Euclidean space
quadratic transport cost

Formal assumptions

measurable normed additive state space
compiled Kantorovich transportCost

View Lean formalization

compiled · faithful paraphrase

ASTIS specializes the compiled Kantorovich value to an ENNReal squared-norm cost and takes its positive ENNReal rpow one half.

`AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSpace.wassersteinDistance`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/Measure/WassersteinSpace.lean:29

noncomputable def wassersteinDistance
    {E : Type*} [NormedAddCommGroup E] [MeasurableSpace E]
    (μ ν : Measure E) : ℝ≥0∞ :=
  (Transport.transportCost (quadraticCost (E := E)) μ ν) ^ (1 / 2 : ℝ)

/-- Chewi display (1.3.5): the square of `W₂` is the infimum of the
quadratic costs over all couplings. -/

Imports

AutoSamplingTheory.TechnicalLemmas.Measure.Transport
Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Mathlib.MeasureTheory.Integral.Bochner.Basic

Local dependencies

transportCost

Downstream consumers

Wasserstein metric
geodesics
Langevin coupling

Displayed identity (1.3.5)

The square of W2 equals the infimum of integrated squared distance over all couplings.

\[W_2^2(\mu,\nu)=\inf_{\gamma\in\Pi(\mu,\nu)}\int\|x-y\|^2\,d\gamma(x,y)\]

W2(mu,nu)^2 equals the quadratic Kantorovich transport cost.

Why is this valid?

The theorem remains valid at infinite transport cost and does not require an optimal coupling witness.

Source assumptions

the W2 and quadratic cost of Definition 1.3.4

Formal assumptions

ENNReal rpow algebra

View Lean formalization

compiled · faithful paraphrase

The equality is proved by ENNReal rpow multiplication, not stored as an axiom.

`AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSpace.wassersteinDistance_sq`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/Measure/WassersteinSpace.lean:36

theorem wassersteinDistance_sq
    {E : Type*} [NormedAddCommGroup E] [MeasurableSpace E]
    (μ ν : Measure E) :
    wassersteinDistance μ ν ^ 2 =
      Transport.transportCost (quadraticCost (E := E)) μ ν := by
  rw [wassersteinDistance, ← ENNReal.rpow_two, ← ENNReal.rpow_mul]
  norm_num

/-- Chewi Definition 1.3.12: a probability measure in `P₂,ac` has finite
second moment and is absolutely continuous with respect to Lebesgue volume.

The generic finite-dimensional real inner-product space specializes to
Euclidean `R^d` in the source. -/

Imports

AutoSamplingTheory.TechnicalLemmas.Measure.Transport
Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Mathlib.MeasureTheory.Integral.Bochner.Basic

Local dependencies

transportCostwassersteinDistance

Downstream consumers

Wasserstein estimates
metric-space route

Definition 1.3.12

P2,ac consists of Euclidean probability laws with finite second moment that are absolutely continuous with respect to Lebesgue measure.

\[\mathcal P_{2,\mathrm{ac}}(\mathbb R^d):=\left\{\mu\ll dx:\int_{\mathbb R^d}\|x\|^2\,d\mu(x)<\infty\right\}\]

A measure belongs to P2,ac when it is a probability measure, its squared norm is integrable, and it is absolutely continuous with respect to volume.

Why is this valid?

The ambient space is a finite-dimensional real inner-product Borel space, so Mathlib volume represents Lebesgue measure and the real squared norm defines the second moment.

Source assumptions

a probability measure on Euclidean space
finite second moment
absolute continuity with respect to Lebesgue measure

Formal assumptions

finite-dimensional real inner-product space
Borel measurable structure
IsProbabilityMeasure, absolute continuity, and Integrable squared norm

View Lean formalization

compiled · faithful paraphrase

ASTIS packages the three measure-theoretic conditions without importing any optimal-map or Wasserstein metric conclusion.

`AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSpace.IsAbsolutelyContinuousFiniteSecondMoment`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/Measure/WassersteinSpace.lean:49

def IsAbsolutelyContinuousFiniteSecondMoment
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (μ : Measure E) : Prop :=
  IsProbabilityMeasure μ ∧
    μ ≪ (volume : Measure E) ∧
    Integrable (fun x : E => ‖x‖ ^ 2) μ

/-- Expansion of the three conditions in the `P₂,ac` definition. -/

Imports

AutoSamplingTheory.TechnicalLemmas.Measure.Transport
Mathlib.Analysis.SpecialFunctions.Pow.NNReal
Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace
Mathlib.MeasureTheory.Integral.Bochner.Basic

Local dependencies

No Registry dependency inferred.

Downstream consumers

Brenier optimal maps
Wasserstein tangent-space calculus
Langevin gradient-flow route

Definition 1.3.25

The Wasserstein geodesic between two P2,ac laws is the law of the affine interpolation of an optimally coupled endpoint pair; it is also called displacement or McCann interpolation.

\[\mu_t:=((1-t)x+ty)_\#\gamma^*,\qquad \gamma^*\in\operatorname*{argmin}_{\gamma\in\Pi(\mu_0,\mu_1)}\int\|x-y\|^2\,d\gamma\]

If gamma is an optimal quadratic coupling of mu0 and mu1, the curve mu_t is the pushforward of gamma by (x0,x1) mapped to (1-t)x0+t x1 for t in [0,1].

Why is this valid?

Both endpoints satisfy the compiled P2,ac predicate. The coupling has the requested marginals and attains the quadratic Kantorovich infimum. The curve agrees with its measurable affine pushforward throughout [0,1].

Source assumptions

two P2,ac probability laws
an optimally coupled endpoint pair

Formal assumptions

a finite-dimensional real inner-product Borel space
P2,ac endpoint predicates
a coupling attaining the quadratic transport cost
the affine pushforward identity on [0,1]

View Lean formalization

compiled · faithful paraphrase

ASTIS represents the joint endpoint law directly as a coupling measure, avoiding an unnecessary auxiliary probability space while preserving the exact law construction.

`AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolation.IsWassersteinGeodesic`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolation.lean:57

def IsWassersteinGeodesic
    (μ₀ μ₁ : Measure E) (curve : ℝ → Measure E) : Prop :=
  WassersteinSpace.IsAbsolutelyContinuousFiniteSecondMoment μ₀ ∧
    WassersteinSpace.IsAbsolutelyContinuousFiniteSecondMoment μ₁ ∧
    ∃ γ : Measure (E × E),
      IsQuadraticOptimalCoupling γ μ₀ μ₁ ∧
      ∀ t ∈ Icc (0 : ℝ) 1,
        curve t = displacementInterpolation γ t

/-- An optimal coupling and two `P₂,ac` endpoints generate the source
displacement-interpolation predicate. -/

Imports

AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSpace

Local dependencies

IsQuadraticOptimalCouplingdisplacementInterpolationIsAbsolutelyContinuousFiniteSecondMoment

Downstream consumers

geodesic convexity
Wasserstein gradient flows
McCann interpolation arguments

Definition 1.3.1

The Kantorovich transport cost is the infimum of expected cost over all joint probability laws with the prescribed marginals.

\[\mathcal T_c(\mu,\nu):=\inf_{\gamma\in\Pi(\mu,\nu)}\int c(x,y)\,d\gamma(x,y)\]

For an extended nonnegative cost c, T_c(mu,nu) is the infimum of the integrals of c against all couplings of mu and nu. The value is extended-real, so infinite transport cost remains representable.

Why is this valid?

The two state spaces are measurable, the cost is ENNReal-valued, and the feasible measures have exactly the requested marginals. Probability normalization follows from probability marginals.

Source assumptions

probability measures on complete separable metric spaces
an extended nonnegative transport cost

Formal assumptions

measurable state spaces
an ENNReal-valued cost
the exact coupling marginal predicate

View Lean formalization

compiled · faithful paraphrase

ASTIS defines the coupling feasible set and its ENNReal infimum directly; lower semicontinuity is reserved for the later minimizer-existence theorem.

`AutoSamplingTheory.TechnicalLemmas.Measure.Transport.transportCost`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/Measure/Transport.lean:36

noncomputable def transportCost {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    (c : α × β → ℝ≥0∞) (μ : Measure α) (ν : Measure β) : ℝ≥0∞ :=
  sInf {r : ℝ≥0∞ | ∃ γ ∈ couplingSet μ ν, r = ∫⁻ z, c z ∂γ}

/-- Source-facing expansion of the Kantorovich value in display (1.3.2). -/

Imports

Mathlib.MeasureTheory.Measure.Prod

Local dependencies

No Registry dependency inferred.

Downstream consumers

optimal-plan existence
2-Wasserstein distance
Kantorovich duality

Displayed identity (1.3.2)

The transport value expands as the infimum of the coupling lintegrals of the cost.

\[\mathcal T_c(\mu,\nu)=\inf_{\gamma\in\Pi(\mu,\nu)}\int_{X\times Y}c(x,y)\,d\gamma(x,y)\]

T_c(mu,nu) = inf over gamma in C(mu,nu) of the integral of c(x,y) against gamma.

Why is this valid?

The equality uses an ENNReal sInf and an ENNReal lintegral over the exact coupling set.

Source assumptions

the Kantorovich feasible set and cost of Definition 1.3.1

Formal assumptions

the compiled transportCost and couplingSet definitions

View Lean formalization

compiled · faithful paraphrase

The source-facing theorem unfolds the ASTIS definition without claiming that the infimum is attained.

`AutoSamplingTheory.TechnicalLemmas.Measure.Transport.transportCost_eq_sInf`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/Measure/Transport.lean:41

theorem transportCost_eq_sInf
    {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    (c : α × β → ℝ≥0∞) (μ : Measure α) (ν : Measure β) :
    transportCost c μ ν =
      sInf {r : ℝ≥0∞ | ∃ γ ∈ couplingSet μ ν, r = ∫⁻ z, c z ∂γ} :=
  rfl

/-- A prescribed probability marginal forces the joint coupling measure to
have total mass one. This recovers the probability-measure interface required
by expectations and transport costs from the marginal contract. -/

Imports

Mathlib.MeasureTheory.Measure.Prod

Local dependencies

transportCost

Downstream consumers

optimal transport comparison arguments
Wasserstein cost specialization

Supporting coupling interface

A coupling is a joint probability law with two prescribed marginals.

\[\Gamma(\mu,\nu)=\{\gamma\in\mathcal P(X\times Y):(\mathrm{proj}_X)_\#\gamma=\mu,\ (\mathrm{proj}_Y)_\#\gamma=\nu\},\qquad \mu\otimes\nu\in\Gamma(\mu,\nu).\]

For probability measures \(\mu\) and \(\nu\), a coupling \(\gamma\) is a measure on the product space whose first marginal is \(\mu\) and second marginal is \(\nu\). The independent product \(\mu\otimes\nu\) provides a canonical feasible coupling.

Why is this valid?

The source works with probability measures on complete separable metric spaces. The coupling contract itself is measure-theoretic; topology and cost measurability enter only when defining and minimizing the transport objective.

Source assumptions

probability measures on the two state spaces

Formal assumptions

measurable spaces
probability-measure instances for both marginals

View Lean formalization

partial · faithful paraphrase

Samplinglib isolates the marginal contract from transport costs and proves the independent-product witness using Mathlib's product-measure marginal identities.

`AutoSamplingTheory.TechnicalLemmas.Measure.Transport.isProbabilityMeasure_of_isCoupling_left`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/Measure/Transport.lean:51

theorem isProbabilityMeasure_of_isCoupling_left
    {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    {γ : Measure (α × β)} {μ : Measure α} {ν : Measure β}
    [IsProbabilityMeasure μ] (hγ : IsCoupling γ μ ν) :
    IsProbabilityMeasure γ := by
  constructor
  rw [← Measure.fst_univ, hγ.1, measure_univ]

/-- The independent product measure is a coupling of two probability measures.
This supplies the canonical nonemptiness witness for the Kantorovich feasible
set in Chewi, Definition 1.3.1. -/

Imports

Mathlib.MeasureTheory.Measure.Prod

Local dependencies

No Registry dependency inferred.

`AutoSamplingTheory.TechnicalLemmas.Measure.Transport.isCoupling_prod`

compiled Samplinglib leaf · AutoSamplingTheory/TechnicalLemmas/Measure/Transport.lean:62

theorem isCoupling_prod {α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
    (μ : Measure α) (ν : Measure β) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] :
    IsCoupling (μ.prod ν) μ ν := by
  constructor <;> simp

/-- The feasible set in the Kantorovich problem is nonempty for probability
marginals. -/

Imports

Mathlib.MeasureTheory.Measure.Prod

Local dependencies

prod

Downstream consumers

optimal transport cost
Wasserstein distance
synchronous Langevin coupling
LMC coupling analysis