The Monge problem

The Monge problem for a cost c : X × Y → ℝ≥0∞ and two measures μ and ν asks for a transport map — a map T : X → Y with ProbabilityTheory.HasLaw T ν μ, so that T pushes μ forward to ν — of least cost ∫⁻ x, c (x, T x) ∂μ. This is the original transport problem, and it is genuinely harder than the Kantorovich problem TauCeti.transportCost of TauCeti/MeasureTheory/OptimalTransport/Cost/Basic.lean, whose feasible set is the couplings: the feasible set here can be empty when the Kantorovich one is not, so TauCeti.mongeCost is only an upper bound for TauCeti.transportCost.

This file introduces the objective TauCeti.transportMapCost, the value TauCeti.mongeCost, the two optimality predicates for maps, and the relations between them. The relaxation TauCeti.transportCost_le_mongeCost is the passage from Monge to Kantorovich, and it comes from the graph plan of TauCeti/MeasureTheory/OptimalTransport/GraphPlan/Basic.lean: every transport map induces a coupling whose cost is at most the map cost. Its equality case, TauCeti.isKantorovichOptimalTransportMap_iff_isOptimalCoupling_graphPlan, says that a map is optimal for the Kantorovich value exactly when its graph plan is an optimal plan; this is the form in which the existence of an optimal map is proved downstream, where a plan is first shown to be deterministic and then read as a map.

The inequality is strict in general: TauCeti.transportCost_lt_mongeCost_dirac splits a Dirac source, whose mass cannot be divided by any map, over a target that is null on singletons. So a statement about transport maps really is a statement about TauCeti.mongeCost, and the two optimality notions for maps — minimality among maps, TauCeti.IsMongeMinimizer, and attainment of the Kantorovich value, TauCeti.IsKantorovichOptimalTransportMap — are kept apart: the second implies the first, and the gap between them is exactly the gap between the two values.

The definitions and the relaxation need no topology and no normalisation (only the strict example asks for a probability target), and the two factors are arbitrary measurable spaces; the cost is extended-nonnegative and integrated by lintegral, so an infeasible problem and a feasible problem whose maps all have infinite cost both take the value ∞; the value alone does not distinguish these cases. TauCeti.exists_hasLaw_of_mongeCost_ne_top only proves that a non-top value implies feasibility.

Main definitions

• TauCeti.transportMapCost c μ T — the cost ∫⁻ x, c (x, T x) ∂μ of transporting μ by the map T, the objective of the Monge problem;
• TauCeti.mongeCost c μ ν — the Monge value: the infimum of TauCeti.transportMapCost c μ T over the transport maps T from μ to ν, and ∞ when there are none;
• TauCeti.transportMapCost_smul and TauCeti.mongeCost_smul — homogeneity under scaling of the source, respectively of both marginals;
• TauCeti.IsMongeMinimizer c μ ν T — T is a transport map attaining the Monge value;
• TauCeti.IsKantorovichOptimalTransportMap c μ ν T — T is a transport map whose cost is the Kantorovich value TauCeti.transportCost c μ ν.

Main statements

• TauCeti.transportCost_le_mongeCost — the Monge-to-Kantorovich relaxation inequality, the Monge value dominates the Kantorovich value;
• TauCeti.mongeCost_zero_measure and TauCeti.mongeCost_eq_transportCost_zero_measure — at zero mass, with a nonempty target type, both values vanish;
• TauCeti.mongeCost_eq_transportCost_of_normalized — equality of the two values for the measures rescaled by a nonzero finite source mass transfers to the source and its target;
• TauCeti.transportCost_lt_mongeCost_dirac — the inequality is strict for a Dirac source and a target that is null on singletons, where TauCeti.mongeCost_eq_top_of_measure_singleton_ne_zero makes the Monge problem infeasible while the Kantorovich problem is not;
• TauCeti.mongeCost_eq_top_of_measure_atom — a positive finite-mass measurable atom makes the Monge problem infeasible when the standard Borel target law is null on singletons;
• TauCeti.isMongeMinimizer_iff — minimality among transport maps is the form of TauCeti.IsMongeMinimizer that avoids the value TauCeti.mongeCost c μ ν, which may be ∞;
• TauCeti.IsKantorovichOptimalTransportMap.isMongeMinimizer and TauCeti.isKantorovichOptimalTransportMap_iff — a map attaining the Kantorovich value is a Monge minimizer, and forces the two values to agree; the converse needs that agreement;
• TauCeti.isKantorovichOptimalTransportMap_iff_isOptimalCoupling_graphPlan — the equality case of the relaxation: a transport map attains the Kantorovich value exactly when its graph plan is an optimal plan;
• TauCeti.lintegral_eq_transportCost_of_ae_eq_comp and TauCeti.lintegral_le_of_ae_eq_comp — if U = T ∘ s almost everywhere for an optimal transport map T from μ to the law of U and a map s of law μ, then s attains the transport cost and minimises the cost of (s', U) among maps s' of law μ;
• TauCeti.isKantorovichOptimalTransportMap_id and TauCeti.mongeCost_self_eq_zero — for a cost vanishing on the diagonal the identity transports any measure onto itself at no cost;
• TauCeti.isKantorovichOptimalTransportMap_dirac_dirac and TauCeti.mongeCost_dirac_dirac — between two Dirac measures the constant transport map is optimal and the Monge value is the value of the cost at the pair.

Implementation notes

TauCeti.mongeCost is an iterated ⨅ over maps and over proofs of ProbabilityTheory.HasLaw, matching TauCeti.transportCost: an empty feasible set gives ∞ with no case split.

The two optimality predicates are structures extending ProbabilityTheory.HasLaw, so that a minimizer carries its transport-map hypothesis, exactly as TauCeti.IsOptimalCoupling extends TauCeti.IsCoupling.

Transport maps are only assumed μ-almost everywhere measurable, since that is what ProbabilityTheory.HasLaw supplies; TauCeti.transportMapCost_congr shows the objective only sees a map up to μ-a.e. equality, and TauCeti.IsMongeMinimizer.congr propagates this to the minimizers.

References

• C. Villani, Topics in Optimal Transportation, Graduate Studies in Mathematics 58, 2003, §1.1.1, where the Monge problem is stated and relaxed to the Kantorovich problem.
• F. Santambrogio, Optimal Transport for Applied Mathematicians, Progress in Nonlinear Differential Equations and their Applications 87, 2015, §1.1, for the Dirac counterexample to equality of the two values.

The cost of a transport map

noncomputable def TauCeti.transportMapCost {X : Type u} {Y : Type v} [MeasurableSpace X] (c : X × Y → ENNReal) (μ : MeasureTheory.Measure X) (T : X → Y) : ENNReal

The cost of transporting μ by the map T: the mass at x travels to T x, at price c (x, T x). This is the objective of the Monge problem, whose value is TauCeti.mongeCost.

theorem TauCeti.transportMapCost_def {X : Type u} {Y : Type v} [MeasurableSpace X] {c : X × Y → ENNReal} {μ : MeasureTheory.Measure X} {T : X → Y} : transportMapCost c μ T = ∫⁻ (x : X), c (x, T x) ∂μ

The cost of a transport map as its defining integral, exposed as a convenient rewrite lemma.

@[simp]

theorem TauCeti.transportMapCost_zero_measure {X : Type u} {Y : Type v} [MeasurableSpace X] (c : X × Y → ENNReal) (T : X → Y) : transportMapCost c 0 T = 0

There is nothing to transport out of the zero measure.

@[simp]

theorem TauCeti.transportMapCost_smul {X : Type u} {Y : Type v} [MeasurableSpace X] (a : ENNReal) (c : X × Y → ENNReal) (μ : MeasureTheory.Measure X) (T : X → Y) : transportMapCost c (a • μ) T = a * transportMapCost c μ T

Scaling the source measure scales the cost of a fixed transport map.

theorem TauCeti.transportMapCost_congr {X : Type u} {Y : Type v} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T S : X → Y} (h : T =ᵐ[μ] S) (c : X × Y → ENNReal) : transportMapCost c μ T = transportMapCost c μ S

The cost of a transport map only depends on the map up to μ-almost everywhere equality, which is the equivalence ProbabilityTheory.HasLaw is invariant under.

theorem TauCeti.transportMapCost_mono {X : Type u} {Y : Type v} [MeasurableSpace X] {c c' : X × Y → ENNReal} {μ : MeasureTheory.Measure X} {T : X → Y} (h : c ≤ c') : transportMapCost c μ T ≤ transportMapCost c' μ T

The cost of a transport map is monotone in the cost function.

@[simp]

theorem TauCeti.transportMapCost_dirac {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSingletonClass X] (c : X × Y → ENNReal) (x : X) (T : X → Y) : transportMapCost c (MeasureTheory.Measure.dirac x) T = c (x, T x)

A Dirac source leaves a map nothing to integrate: the cost of T is the cost of its single move.

theorem TauCeti.transportMapCost_eq_lintegral_graphPlan {X : Type u} {Y : Type v} [MeasurableSpace X] {c : X × Y → ENNReal} {μ : MeasureTheory.Measure X} {T : X → Y} [MeasurableSpace Y] (hT : AEMeasurable T μ) (hc : AEMeasurable c (graphPlan T μ)) : transportMapCost c μ T = ∫⁻ (z : X × Y), c z ∂graphPlan T μ

The cost of a transport map is the cost integral of its graph plan.

The Monge value

noncomputable def TauCeti.mongeCost {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] (c : X × Y → ENNReal) (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) : ENNReal

The Monge value of μ and ν for the cost c: the infimum of TauCeti.transportMapCost c μ T over the transport maps T from μ to ν. It is ∞ when μ and ν admit no transport map at all, which — unlike for TauCeti.transportCost — happens already for a Dirac μ and a ν that is null on singletons.

theorem TauCeti.mongeCost_def {X : Type u} {Y : Type v} [MeasurableSpace X] {c : X × Y → ENNReal} {μ : MeasureTheory.Measure X} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} : mongeCost c μ ν = ⨅ (T : X → Y), ⨅ (_ : ProbabilityTheory.HasLaw T ν μ), transportMapCost c μ T

The Monge value as the infimum of the costs of all transport maps.

theorem TauCeti.mongeCost_smul {X : Type u} {Y : Type v} [MeasurableSpace X] {a : ENNReal} [MeasurableSpace Y] (ha₀ : a ≠ 0) (ha : a ≠ ⊤) (c : X × Y → ENNReal) (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) : mongeCost c (a • μ) (a • ν) = a * mongeCost c μ ν

Homogeneity of the Monge cost. Scaling both marginals by the same nonzero finite factor scales the Monge value by that factor. The nonzero assumption is necessary: at zero mass a transport map need not exist when the target type is empty.

theorem TauCeti.mongeCost_le_transportMapCost {X : Type u} {Y : Type v} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {T : X → Y} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} (hT : ProbabilityTheory.HasLaw T ν μ) (c : X × Y → ENNReal) : mongeCost c μ ν ≤ transportMapCost c μ T

Every transport map bounds the Monge value from above.

theorem TauCeti.le_mongeCost {X : Type u} {Y : Type v} [MeasurableSpace X] {c : X × Y → ENNReal} {μ : MeasureTheory.Measure X} {a : ENNReal} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} (h : ∀ (T : X → Y), ProbabilityTheory.HasLaw T ν μ → a ≤ transportMapCost c μ T) : a ≤ mongeCost c μ ν

A bound valid on every transport map bounds the Monge value from below.

theorem TauCeti.mongeCost_lt_iff {X : Type u} {Y : Type v} [MeasurableSpace X] {c : X × Y → ENNReal} {μ : MeasureTheory.Measure X} {a : ENNReal} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} : mongeCost c μ ν < a ↔ ∃ (T : X → Y), ProbabilityTheory.HasLaw T ν μ ∧ transportMapCost c μ T < a

The Monge value is below a threshold exactly when some transport map is.

theorem TauCeti.mongeCost_mono {X : Type u} {Y : Type v} [MeasurableSpace X] {c c' : X × Y → ENNReal} {μ : MeasureTheory.Measure X} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} (h : c ≤ c') : mongeCost c μ ν ≤ mongeCost c' μ ν

The Monge value is monotone in the cost function.

theorem TauCeti.mongeCost_eq_top_of_not_exists_hasLaw {X : Type u} {Y : Type v} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} (h : ¬∃ (T : X → Y), ProbabilityTheory.HasLaw T ν μ) (c : X × Y → ENNReal) : mongeCost c μ ν = ⊤

An infeasible Monge problem has value ∞.

theorem TauCeti.exists_hasLaw_of_mongeCost_ne_top {X : Type u} {Y : Type v} [MeasurableSpace X] {c : X × Y → ENNReal} {μ : MeasureTheory.Measure X} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} (h : mongeCost c μ ν ≠ ⊤) : ∃ (T : X → Y), ProbabilityTheory.HasLaw T ν μ

A finite Monge value is witnessed by a transport map. The converse fails: feasibility does not guarantee a finite-cost transport map, since every feasible map may have infinite cost. This is why the result is not stated as an iff with TauCeti.mongeCost_eq_top_of_not_exists_hasLaw.

theorem TauCeti.transportCost_le_mongeCost {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] (c : X × Y → ENNReal) (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) : transportCost c μ ν ≤ mongeCost c μ ν

The Monge-to-Kantorovich relaxation inequality: the Kantorovich value of μ and ν is at most their Monge value, because the graph plan of a transport map is a coupling whose cost is at most the map cost. The inequality can be strict — see TauCeti.transportCost_lt_mongeCost_dirac — and its equality case at a fixed map is TauCeti.isKantorovichOptimalTransportMap_iff_isOptimalCoupling_graphPlan.

@[simp]

theorem TauCeti.mongeCost_zero_measure {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] [Nonempty Y] (c : X × Y → ENNReal) : mongeCost c 0 0 = 0

At zero mass a constant map transports the zero source onto the zero target at no cost, so the Monge value vanishes. The target type must be nonempty for such a map to exist.

theorem TauCeti.mongeCost_eq_transportCost_zero_measure {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] [Nonempty Y] (c : X × Y → ENNReal) : mongeCost c 0 0 = transportCost c 0 0

At zero mass the Monge and Kantorovich values agree, both being zero, as soon as the target type is nonempty.

theorem TauCeti.mongeCost_eq_transportCost_of_normalized {X : Type u} {Y : Type v} [MeasurableSpace X] {c : X × Y → ENNReal} {μ : MeasureTheory.Measure X} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} [MeasureTheory.IsFiniteMeasure μ] (hμ : μ ≠ 0) (hnorm : mongeCost c ((μ Set.univ)⁻¹ • μ) ((μ Set.univ)⁻¹ • ν) = transportCost c ((μ Set.univ)⁻¹ • μ) ((μ Set.univ)⁻¹ • ν)) : mongeCost c μ ν = transportCost c μ ν

Equality of the Monge and Kantorovich values for the measures obtained by rescaling a nonzero finite source μ and a target ν by the mass of μ transfers to μ and ν themselves. The rescaled source is a probability measure, and the rescaled target is one when ν univ = μ univ. Combined with TauCeti.mongeCost_eq_transportCost_zero_measure, this reduces equality for finite measures of equal mass to the probability case.

Optimal transport maps

structure TauCeti.IsMongeMinimizer {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] (c : X × Y → ENNReal) (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) (T : X → Y) extends ProbabilityTheory.HasLaw T ν μ : Prop

IsMongeMinimizer c μ ν T says that T solves the Monge problem: it is a transport map from μ to ν, and its cost is the Monge value of the pair.

• aemeasurable : AEMeasurable T μ
• map_eq : MeasureTheory.Measure.map T μ = ν
• transportMapCost_eq : transportMapCost c μ T = mongeCost c μ ν

  A Monge minimizer attains the Monge value.

structure TauCeti.IsKantorovichOptimalTransportMap {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] (c : X × Y → ENNReal) (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) (T : X → Y) extends ProbabilityTheory.HasLaw T ν μ : Prop

IsKantorovichOptimalTransportMap c μ ν T says that T is a transport map from μ to ν whose cost is the Kantorovich value of the pair. By TauCeti.transportCost_le_mongeCost this is the stronger of the two optimality notions: such a map is a Monge minimizer, TauCeti.IsKantorovichOptimalTransportMap.isMongeMinimizer, and it forces the two values to agree. It is the conclusion of the existence theorems for optimal maps, which produce a map out of an optimal plan.

• aemeasurable : AEMeasurable T μ
• map_eq : MeasureTheory.Measure.map T μ = ν
• transportMapCost_eq : transportMapCost c μ T = transportCost c μ ν

  A Kantorovich-optimal transport map attains the Kantorovich value.

theorem TauCeti.IsMongeMinimizer.transportMapCost_le {X : Type u} {Y : Type v} [MeasurableSpace X] {c : X × Y → ENNReal} {μ : MeasureTheory.Measure X} {T S : X → Y} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} (h : IsMongeMinimizer c μ ν T) (hS : ProbabilityTheory.HasLaw S ν μ) : transportMapCost c μ T ≤ transportMapCost c μ S

A Monge minimizer costs no more than any other transport map of the same pair.

theorem TauCeti.IsMongeMinimizer.congr {X : Type u} {Y : Type v} [MeasurableSpace X] {c : X × Y → ENNReal} {μ : MeasureTheory.Measure X} {T S : X → Y} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} (h : IsMongeMinimizer c μ ν T) (hS : S =ᵐ[μ] T) : IsMongeMinimizer c μ ν S

Being a Monge minimizer only depends on the map up to μ-almost everywhere equality.

theorem TauCeti.isMongeMinimizer_iff {X : Type u} {Y : Type v} [MeasurableSpace X] {c : X × Y → ENNReal} {μ : MeasureTheory.Measure X} {T : X → Y} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} : IsMongeMinimizer c μ ν T ↔ ProbabilityTheory.HasLaw T ν μ ∧ ∀ (S : X → Y), ProbabilityTheory.HasLaw S ν μ → transportMapCost c μ T ≤ transportMapCost c μ S

Being a Monge minimizer is minimality among the transport maps. This form of the definition avoids the value TauCeti.mongeCost c μ ν, so it is the one to check when that value may be ∞.

theorem TauCeti.IsKantorovichOptimalTransportMap.mongeCost_eq_transportCost {X : Type u} {Y : Type v} [MeasurableSpace X] {c : X × Y → ENNReal} {μ : MeasureTheory.Measure X} {T : X → Y} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} (h : IsKantorovichOptimalTransportMap c μ ν T) : mongeCost c μ ν = transportCost c μ ν

A map attaining the Kantorovich value closes the gap in TauCeti.transportCost_le_mongeCost: the two values agree.

theorem TauCeti.IsKantorovichOptimalTransportMap.isMongeMinimizer {X : Type u} {Y : Type v} [MeasurableSpace X] {c : X × Y → ENNReal} {μ : MeasureTheory.Measure X} {T : X → Y} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} (h : IsKantorovichOptimalTransportMap c μ ν T) : IsMongeMinimizer c μ ν T

A map attaining the Kantorovich value is a Monge minimizer.

theorem TauCeti.IsKantorovichOptimalTransportMap.congr {X : Type u} {Y : Type v} [MeasurableSpace X] {c : X × Y → ENNReal} {μ : MeasureTheory.Measure X} {T S : X → Y} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} (h : IsKantorovichOptimalTransportMap c μ ν T) (hS : S =ᵐ[μ] T) : IsKantorovichOptimalTransportMap c μ ν S

Attaining the Kantorovich value only depends on the map up to μ-almost everywhere equality.

theorem TauCeti.isKantorovichOptimalTransportMap_iff {X : Type u} {Y : Type v} [MeasurableSpace X] {c : X × Y → ENNReal} {μ : MeasureTheory.Measure X} {T : X → Y} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} : IsKantorovichOptimalTransportMap c μ ν T ↔ IsMongeMinimizer c μ ν T ∧ mongeCost c μ ν = transportCost c μ ν

A Monge minimizer attains the Kantorovich value exactly when the two values agree. So the two optimality notions for maps differ by exactly the gap in TauCeti.transportCost_le_mongeCost.

theorem TauCeti.isKantorovichOptimalTransportMap_iff_isOptimalCoupling_graphPlan {X : Type u} {Y : Type v} [MeasurableSpace X] {c : X × Y → ENNReal} {μ : MeasureTheory.Measure X} {T : X → Y} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} (hT : ProbabilityTheory.HasLaw T ν μ) (hc : AEMeasurable c (graphPlan T μ)) : IsKantorovichOptimalTransportMap c μ ν T ↔ IsOptimalCoupling c (graphPlan T μ) μ ν

The equality case of the relaxation inequality at a fixed map: a transport map attains the Kantorovich value exactly when its graph plan is an optimal plan. This is how an optimal map is read off an optimal plan that has been shown to be deterministic.

theorem TauCeti.lintegral_eq_transportCost_of_ae_eq_comp {X : Type u} {Y : Type v} [MeasurableSpace X] {c : X × Y → ENNReal} {μ : MeasureTheory.Measure X} {T : X → Y} [MeasurableSpace Y] {α : Type u_1} [MeasurableSpace α] {m : MeasureTheory.Measure α} {U : α → Y} {s : α → X} (hc : Measurable c) (hT : IsKantorovichOptimalTransportMap c μ (MeasureTheory.Measure.map U m) T) (hs : ProbabilityTheory.HasLaw s μ m) (h : U =ᵐ[m] T ∘ s) : ∫⁻ (ω : α), c (s ω, U ω) ∂m = transportCost c μ (MeasureTheory.Measure.map U m)

A factor through an optimal map attains the transport cost. Let T be an optimal transport map for a measurable cost c from μ to the law of U : α → Y, and let s : α → X have law μ with U = T ∘ s almost everywhere. Then the pair (s, U) pushes m to the graph plan of T, so ∫⁻ c (s ω, U ω) dm is the optimal transport cost from μ to the law of U.

theorem TauCeti.lintegral_le_of_ae_eq_comp {X : Type u} {Y : Type v} [MeasurableSpace X] {c : X × Y → ENNReal} {μ : MeasureTheory.Measure X} {T : X → Y} [MeasurableSpace Y] {α : Type u_1} [MeasurableSpace α] {m : MeasureTheory.Measure α} {U : α → Y} {s s' : α → X} (hc : Measurable c) (hT : IsKantorovichOptimalTransportMap c μ (MeasureTheory.Measure.map U m) T) (hs : ProbabilityTheory.HasLaw s μ m) (h : U =ᵐ[m] T ∘ s) (hs' : ProbabilityTheory.HasLaw s' μ m) : ∫⁻ (ω : α), c (s ω, U ω) ∂m ≤ ∫⁻ (ω : α), c (s' ω, U ω) ∂m

A factor through an optimal map is cost-minimising. Let T be an optimal transport map for a measurable cost c from μ to the law of U : α → Y, and let s : α → X have law μ with U = T ∘ s almost everywhere. Then among all maps s' of law μ, s minimises the cost ∫⁻ c (s' ω, U ω) dm.

Transporting a measure to itself

theorem TauCeti.mongeCost_self_eq_zero {X : Type u} [MeasurableSpace X] {c : X × X → ENNReal} (hc : ∀ (x : X), c (x, x) = 0) (μ : MeasureTheory.Measure X) : mongeCost c μ μ = 0

A cost vanishing on the diagonal makes the identity a free transport map, so the Monge problem of a measure with itself has value 0 for every measure.

theorem TauCeti.isKantorovichOptimalTransportMap_id {X : Type u} [MeasurableSpace X] {c : X × X → ENNReal} (hc : ∀ (x : X), c (x, x) = 0) (μ : MeasureTheory.Measure X) : IsKantorovichOptimalTransportMap c μ μ id

The identity is a Kantorovich-optimal transport map of a measure onto itself whenever the cost vanishes on the diagonal. Together with TauCeti.mongeCost_self_eq_zero this exhibits both optimality notions at an arbitrary measure, not only at Dirac measures.

Dirac measures

theorem TauCeti.isKantorovichOptimalTransportMap_dirac_dirac {X : Type u} {Y : Type v} [MeasurableSpace X] {c : X × Y → ENNReal} [MeasurableSpace Y] (hc : Measurable c) (x : X) (y : Y) : IsKantorovichOptimalTransportMap c (MeasureTheory.Measure.dirac x) (MeasureTheory.Measure.dirac y) fun (x : X) => y

Between two Dirac measures the constant map is a transport map attaining the Kantorovich value computed by TauCeti.transportCost_dirac_dirac.

theorem TauCeti.mongeCost_dirac_dirac {X : Type u} {Y : Type v} [MeasurableSpace X] {c : X × Y → ENNReal} [MeasurableSpace Y] (hc : Measurable c) (x : X) (y : Y) : mongeCost c (MeasureTheory.Measure.dirac x) (MeasureTheory.Measure.dirac y) = c (x, y)

The Monge value of two Dirac measures is the value of the cost at the pair, matching TauCeti.transportCost_dirac_dirac.

Source atoms obstruct the Monge problem

theorem TauCeti.mongeCost_eq_top_of_measure_atom {X : Type u} {Y : Type v} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} [StandardBorelSpace Y] [MeasureTheory.NullSingletonClass ν] {A : Set X} (hAfin : μ A ≠ ⊤) (hAatom : μ.IsAtom A) (c : X × Y → ENNReal) : mongeCost c μ ν = ⊤

A positive finite-mass source atom makes the Monge problem infeasible over a singleton-null standard Borel target. An a.e.-measurable map sends the entire mass of the atom to one point, whereas a law that is null on singletons gives that point no mass. Consequently the Monge value is ∞ for every cost.

theorem TauCeti.mongeCost_eq_top_of_measure_singleton_ne_zero {X : Type u} {Y : Type v} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} [MeasureTheory.NullSingletonClass ν] {x : X} (hx : μ {x} ≠ 0) (c : X × Y → ENNReal) : mongeCost c μ ν = ⊤

A nonzero source singleton makes the Monge problem infeasible over a target that is null on singletons. No map can split the mass sitting at a single point, so such a source has no transport map onto the target, and the Monge value is ∞ for every cost.

theorem TauCeti.transportCost_lt_mongeCost_dirac {X : Type u} {Y : Type v} [MeasurableSpace X] {c : X × Y → ENNReal} [MeasurableSpace Y] {ν : MeasureTheory.Measure Y} [MeasureTheory.IsProbabilityMeasure ν] [MeasureTheory.NullSingletonClass ν] (hc : Measurable c) {x : X} (h : ∫⁻ (y : Y), c (x, y) ∂ν ≠ ⊤) : transportCost c (MeasureTheory.Measure.dirac x) ν < mongeCost c (MeasureTheory.Measure.dirac x) ν

The relaxation inequality is strict in general. Splitting a Dirac source over an target that is null on singletons and has finite cost is a Kantorovich problem with a finite value and a Monge problem with no competitor at all. This is the standard obstruction to Monge's problem: there is no map carrying a point mass onto such a measure.