Graph plans: the transport plan induced by a transport map #
A transport map from μ to ν is a map T : X → Y that pushes μ forward to ν. Mathlib
already has the predicate for this, ProbabilityTheory.HasLaw T ν μ, which asks for
μ-almost-everywhere measurability of T together with μ.map T = ν; this file adds no second
predicate. What it adds is the optimal-transport interface around it: the graph plan
TauCeti.graphPlan T μ, the pushforward of μ along x ↦ (x, T x), which is the transport
plan that moves all the mass sitting at x to the single point T x.
Two facts organise the file. First, TauCeti.isCoupling_graphPlan_iff: for an
almost-everywhere measurable T, the graph plan couples μ and ν exactly when T is a
transport map from μ to ν. This is the passage from the Monge problem to the Kantorovich
problem, whose effect on values is the change of variables TauCeti.lintegral_graphPlan; the
resulting inequality of transport costs belongs to the cost theory and is stated in
TauCeti/MeasureTheory/OptimalTransport/Cost/Basic.lean. Second, TauCeti.eq_graphPlan_iff: a plan
is a graph plan exactly when it is deterministic, that is, concentrated on the graph of T.
With TauCeti.graphPlan_eq_graphPlan_iff, which says that the map is determined μ-almost
everywhere by its graph plan, this makes the graph construction a bijection between transport
maps modulo μ-a.e. equality and deterministic plans.
Nothing here needs a topology, a metric or a normalisation, and the two factors are arbitrary
measurable spaces. The determinism statements do ask that the diagonal of Y × Y be
measurable, MeasurableEq Y, because "π is carried by the graph of T" is otherwise not a
statement about a measurable set. That hypothesis holds for every standard Borel space, every
second-countable Hausdorff space with measurable open sets and every countable measurable space
with measurable singletons.
Main definitions #
TauCeti.graphPlan T μ— the graph plan, or Monge plan, ofT: the pushforward ofμalongx ↦ (x, T x);TauCeti.Coupling.graph— the graph plan of a transport map between two probability measures, bundled as an element ofTauCeti.Coupling;TauCeti.Coupling.coe_graphidentifies its underlying probability measure with the bundled pushforwardMeasureTheory.ProbabilityMeasure.mapalongx ↦ (x, T x), whichTauCeti.toMeasure_map_prodMk_selfidentifies with the graph plan.
Main statements #
TauCeti.fst_graphPlanandTauCeti.snd_graphPlan— whenTisμ-a.e. measurable, the two marginals of its graph plan areμandμ.map T;TauCeti.isCoupling_graphPlan_iff— the graph plan of an a.e. measurableTcouplesμandνexactly whenProbabilityTheory.HasLaw T ν μ;TauCeti.lintegral_graphPlan— the change of variables∫⁻ z, c z ∂graphPlan T μ = ∫⁻ x, c (x, T x) ∂μ, which feeds the Monge-to-Kantorovich inequalityTauCeti.transportCost_le_lintegral_of_hasLawinTauCeti/MeasureTheory/OptimalTransport/Cost/Basic.lean, and its Bochner versionTauCeti.integral_graphPlan;TauCeti.eq_graphPlan_iff— a plan is the graph plan ofTexactly when it is concentrated on the graph ofT, withTauCeti.graphPlan_eq_graphPlan_iffthe uniqueness of the map that induces a given deterministic plan;TauCeti.comp_ae_eq_id_of_map_swap_graphPlan_eq— when the coordinate swap of the graph plan ofTis the graph plan ofR, the maps are two-sided inverses almost everywhere;TauCeti.eq_dirac_of_hasLaw_dirac— a transport map out of a Dirac measure forces the target to be a Dirac measure, so the unique plan out of an atom is deterministic only in that case.
Implementation notes #
TauCeti.graphPlan records the map in the second coordinate, matching the plan-first
convention of TauCeti.IsCoupling π μ ν, in which the source is the first factor. The opposite
convention is available as TauCeti.map_swap_graphPlan, which identifies the coordinate swap
of a graph plan with the pushforward along x ↦ (T x, x).
Measurability hypotheses are AEMeasurable rather than Measurable throughout, because that
is what ProbabilityTheory.HasLaw supplies and what the pushforward really uses. Both marginal
formulas need T to be a.e. measurable: Measure.map sends a function that is not a.e.
measurable to a junk Dirac mass, which neither marginal formula survives.
This module needs nothing from the transport cost, so it sits below it: the Monge-to-Kantorovich
relaxation inequality of Layer 4, item 1, which the change of variables here supplies, is stated
with the cost itself in TauCeti/MeasureTheory/OptimalTransport/Cost/Basic.lean.
This is Layer 0, item 2 of the optimal-transport roadmap.
References #
- C. Villani, Optimal Transport: Old and New, Grundlehren 338, 2009, Chapter 1: a coupling is
called deterministic when it is of the form
(id, T)_# μ, and the discussion following Definition 1.2 records that this happens exactly when the coupling is concentrated on the graph of a map. - C. Villani, Topics in Optimal Transportation, Graduate Studies in Mathematics 58, 2003, §1.1.1, where the Monge problem is relaxed to the Kantorovich problem precisely by sending a transport map to its graph plan.
The graph plan, or Monge plan, of a map T : X → Y and a measure μ on X: the
pushforward of μ along x ↦ (x, T x). It is the transport plan that sends all the mass at
x to the single point T x; TauCeti.isCoupling_graphPlan_iff says that it couples μ and
ν exactly when T pushes μ forward to ν.
Equations
- TauCeti.graphPlan T μ = MeasureTheory.Measure.map (fun (x : X) => (x, T x)) μ
Instances For
The graph plan is the pushforward along the graph map. The definition's body is not exposed, so this is the lemma downstream modules should rewrite with.
The graph map x ↦ (x, T x) is a.e. measurable as soon as T is.
The graph plan of a measurable set is the mass of the set of points whose graph point lies in it.
The graph plan of a measurable rectangle is the mass of the part of its base that T maps
into its height.
The graph plan over the zero measure is the zero measure.
The second marginal of the graph plan of an a.e. measurable T is the pushforward of μ
along T.
The first marginal of the graph plan of an a.e. measurable T is μ.
The graph plan of an a.e. measurable T couples μ and the pushforward μ.map T.
From the Monge problem to the Kantorovich problem: the graph plan of a transport map
from μ to ν is a coupling of μ and ν.
The graph plan of an a.e. measurable map couples μ and ν exactly when the map is a
transport map from μ to ν. The Monge problem is therefore the Kantorovich problem
restricted to the graph plans.
A map transports μ to ν exactly when its graph plan has second marginal ν.
The second marginal of the graph plan of a transport map is its target.
Chaining two transport maps chains the targets of their graph plans.
The second marginal of the graph plan of a measure-preserving map is its target.
The second marginal of the graph plan of the identity is the original measure.
The identity is a transport map from μ to itself, so its graph plan — the diagonal plan,
carried by the diagonal of X × X — couples μ with itself.
A measurable equivalence is a transport map from μ to μ.map e.
A function of the first coordinate is a.e. measurable for a graph plan as soon as it is a.e. measurable for the source measure.
Two maps that agree μ-almost everywhere have the same graph plan.
Taking the graph plan of a fixed map is additive in the source measure.
Taking the graph plan of a fixed map commutes with rescaling the source measure.
Exchanging the coordinates of a graph plan gives the pushforward of μ along
x ↦ (T x, x), the graph plan for the opposite convention.
Postcomposing a transport map with a map that is a.e. measurable for the transported measure
pushes its graph plan forward in the second coordinate. Together with
ProbabilityTheory.HasLaw.comp this is how transport maps compose.
Reparametrizing the source measure pushes the graph plan through the first coordinate.
A measurable equivalence and its inverse have graph plans exchanged by coordinate swap.
Change of variables along a graph plan: integrating a cost against the graph plan of T
is integrating the cost of moving x to T x.
Change of variables along a graph plan, Bochner version: integrating a vector-valued
function against the graph plan of T is integrating its values at the graph points.
The mass a graph plan of T gives to the complement of the graph of S is the mass of the
set where T and S differ.
A graph plan of T is carried by the graph of S exactly when S agrees with T
almost everywhere.
A graph plan is carried by the graph of its map: almost every point of graphPlan T μ has
second coordinate the value of T at its first.
A plan carried by the graph of T is the graph plan of T over its own first marginal.
This direction needs no hypothesis on Y.
A plan is deterministic exactly when it is a graph plan: a plan is the graph plan of T
over its own first marginal if and only if it is concentrated on the graph of T.
The map of a deterministic plan is unique: two a.e. measurable maps have the same graph
plan exactly when they agree μ-almost everywhere.
Inverse graph plans come from inverse maps. If exchanging the coordinates of the graph
plan of T : X → Y over μ gives the graph plan of R : Y → X over ν, then R ∘ T = id
μ-almost everywhere and T ∘ R = id ν-almost everywhere.
A transport map out of a Dirac measure forces the target to be the Dirac measure at its
value. So the unique coupling of Measure.dirac x with a non-Dirac probability measure ν,
namely the pushforward of ν along y ↦ (x, y), is not a graph plan: the Monge problem out of
an atom is infeasible unless the target is an atom too.
The graph plan of an a.e. measurable map at a Dirac measure is the Dirac measure at the graph point.
The bundled pushforward of a probability measure along the graph map x ↦ (x, T x) is the
graph plan of T.
The graph plan of a transport map between two probability measures, bundled as an element of
TauCeti.Coupling.
Instances For
The underlying probability measure of a bundled graph plan is the pushforward of μ along
the graph map x ↦ (x, T x).