Gluing transport plans #
Two transport plans that share an intermediate marginal can be realised simultaneously: if π is a
measure on X × Y whose second marginal agrees with the first marginal of a measure σ on
Y × Z, then there is a measure γ on X × Y × Z whose (X, Y)-marginal is π and whose
(Y, Z)-marginal is σ. This is the gluing lemma, and it is what lets transport costs be composed
— it is the measure-theoretic input to the triangle inequality for Wasserstein distances and to
the composition of couplings.
The construction is a composition-product against a conditional kernel, so it needs a
disintegration of one of the two plans. There are two ways to obtain one. Mathlib's regular
conditional kernel gives it under a standard Borel hypothesis on one of the two outer spaces,
the middle space Y then carrying no hypothesis at all. Alternatively, when the middle space is
countable with measurable singletons, TauCeti.MeasureTheory.countableCondKernel gives it with no
hypothesis on either outer space — the regime the cut distance of the dense graph limit theory
needs, since its two carriers are arbitrary probability spaces.
Main definitions #
TauCeti.Measure.glue π κ— the measure onX × Y × Zobtained by extending a measureπ : Measure (X × Y)along a kernelκ : Kernel Y Zacting on the middle coordinate. It is the associated right-nested form ofπ ⊗ₘ Kernel.prodMkLeft X κ.
Main statements #
TauCeti.Measure.map_prodMap_id_fst_glue— the(X, Y)-marginal ofglue π κisπ;TauCeti.Measure.snd_glue— its(Y, Z)-marginal isπ.snd ⊗ₘ κ;TauCeti.Measure.lintegral_glue— the iterated-integral formula againstglue π κ;TauCeti.Measure.glue_deterministic— gluing against a deterministic kernel is a pushforward, so a graph plan glues without adding randomness;TauCeti.Measure.exists_glue_of_standardBorel_rightandTauCeti.Measure.exists_glue_of_standardBorel_left— the gluing lemma, in the two regimes obtained by disintegratingσoverY(which needsZstandard Borel) and by disintegratingπoverY(which needsXstandard Borel);TauCeti.MeasureTheory.exists_glue_of_countable_middle— the gluing lemma over a countable middle space, which needs nothing of either outer space;TauCeti.Measure.exists_comp_of_exists_glue— the composition of plans read off a glued measure, withTauCeti.Measure.exists_comp_of_standardBorel_right,TauCeti.Measure.exists_comp_of_standardBorel_leftandTauCeti.MeasureTheory.exists_comp_of_countable_middleits three concrete forms;TauCeti.Measure.lintegral_map_prodMap_id_snd_le— the composition estimate: a cost onX × Zdominated by the sum of a cost onX × Yand a cost onY × Zintegrates against the composed plan to at most the sum of the two integrals. This is the mechanism behind the triangle inequality for transport costs.
Implementation notes #
Marginals of a measure on X × Y × Z are written as pushforwards along Prod.map id Prod.fst
(the (X, Y)-marginal), Prod.map id Prod.snd (the (X, Z)-marginal) and Prod.snd (the
(Y, Z)-marginal, which is MeasureTheory.Measure.snd).
The hypothesis relating the two plans is stated as π.snd = σ.fst rather than through a coupling
predicate: gluing needs neither of the two outer marginals, only the agreement of the middle one,
and stating it this way keeps the theorems usable by any packaging of couplings built on
MeasureTheory.Measure.fst/MeasureTheory.Measure.snd.
References #
- C. Villani, Topics in Optimal Transportation, Graduate Studies in Mathematics 58, 2003, Lemma 7.6 ("Gluing lemma"), and Optimal Transport: Old and New, Grundlehren 338, 2009, Chapter 1. Both state it for three Polish probability spaces; the versions here ask for a standard Borel structure on one outer space only — or, in the countable-middle version, for nothing at all on the outer spaces — and no normalisation of the plans.
- Roadmap:
TauCetiRoadmap/DenseGraphLimits/README.md, the design-validation milestone preceding the arbitrary-carrier triangle inequality of Layer 1 — "finite coupling gluing with zero-mass middle atoms explicit".TauCeti.MeasureTheory.exists_glue_of_countable_middleis that gluing.
The gluing of a measure π on X × Y with a kernel κ : Kernel Y Z along the middle
coordinate: the measure on X × Y × Z which draws (x, y) from π and then z from κ y.
Its (X, Y)-marginal is π (TauCeti.Measure.map_prodMap_id_fst_glue) and its (Y, Z)-marginal
is π.snd ⊗ₘ κ (TauCeti.Measure.snd_glue), so choosing κ to be a conditional kernel of a
second plan σ glues π and σ.
Equations
Instances For
The measure a gluing assigns to a measurable set: integrate the kernel mass of the fibre against the plan being extended.
Integration against a gluing is the iterated integral: first over the fibre of the kernel, then over the plan being extended.
The (X, Y)-marginal of a gluing is the plan it extends.
The (Y, Z)-marginal of a gluing is the composition-product of the middle marginal with the
kernel.
The X-marginal of a gluing is the X-marginal of the plan it extends.
The middle marginal of a gluing is the middle marginal of the plan it extends: gluing does not disturb the coordinate the kernel is indexed by.
Gluing against a deterministic kernel is a pushforward: the third coordinate is the image of the second. This is the graph-plan case, in which the glued measure carries no new randomness.
Gluing π against a conditional kernel of σ recovers σ as the (Y, Z)-marginal, as soon
as the two plans share their middle marginal.
The gluing lemma, obtained by disintegrating the second plan over the middle space.
Two plans sharing a middle marginal, π.snd = σ.fst, admit a joint law on X × Y × Z with π and
σ as its two consecutive two-coordinate marginals. Only the last space is assumed standard Borel;
the middle space Y carries no hypothesis.
When Z is nonempty, the explicit witness is glue π σ.condKernel; use it instead of this
statement when the probability-measure or finiteness instances of the glued measure are needed.
The gluing lemma, obtained by disintegrating the first plan over the middle space.
This is the mirror image of TauCeti.Measure.exists_glue_of_standardBorel_right: it assumes the
first space standard Borel instead of the last one. Neither version implies the other, and the
middle space Y again carries no hypothesis.
The composition of two plans is the (X, Z)-marginal of a glued measure. Its first marginal is
the first marginal of the first plan.
The second marginal of the composition of two plans is the second marginal of the second plan.
The composition estimate. If a cost on X × Z is dominated pointwise by the sum of a cost on
X × Y and a cost on Y × Z, then the composition of two glued plans costs at most the sum of
their two costs.
This is the mechanism behind the triangle inequality for transport costs: taking c, c₁ and c₂
to be a ground distance recovers d (x, z) ≤ d (x, y) + d (y, z), and the glued measure is what
lets the three integrals be compared on a common space.
The composition of two plans, read off a glued measure: the (X, Z)-marginal of a gluing of
π and σ has the outer marginals of π and σ.
The composed plan of TauCeti.Measure.exists_comp_of_exists_glue, together with the cost
estimate of TauCeti.Measure.lintegral_map_prodMap_id_snd_le.
Two plans sharing a middle marginal compose to a plan with the two outer marginals, when the last space is standard Borel.
Two plans sharing a middle marginal compose to a plan with the two outer marginals, when the first space is standard Borel.
Gluing over a countable middle space #
These live in TauCeti.MeasureTheory rather than alongside their standard Borel siblings in
TauCeti.Measure: scripts/lint-dot-notation.py forbids a new declaration under
TauCeti.Measure whose statement mentions MeasureTheory.Measure, because such a namespace
blocks dot notation on Mathlib's type. TauCeti.MeasureTheory is the namespace of the
conditional kernel these consume.
Gluing π against the conditional kernel of σ over a countable middle space recovers σ as
the (Y, Z)-marginal, as soon as the two plans share their middle marginal.
The gluing lemma over a countable middle space.
Two plans sharing a middle marginal, π.snd = σ.fst, admit a joint law on X × Y × Z with π
and σ as its two consecutive two-coordinate marginals, as soon as the middle space Y is
countable with measurable singletons. Neither outer space carries any hypothesis — in particular
neither is assumed standard Borel, so this is not a special case of either
TauCeti.Measure.exists_glue_of_standardBorel_right or
TauCeti.Measure.exists_glue_of_standardBorel_left, and conversely neither of those covers it.
When Z is nonempty the explicit witness is TauCeti.Measure.glue π (countableCondKernel σ); use
it instead of this statement when the probability-measure or finiteness instances of the glued
measure are needed.
Two plans sharing a middle marginal compose to a plan with the two outer marginals, when the middle space is countable. Unlike the two standard Borel forms, this asks nothing of either outer space.