Complementary slackness, optimality certificates, and c-cyclical monotonicity

A pair of integrable potentials φ, ψ satisfying the Kantorovich dual constraint φ x + ψ y ≤ c (x, y) bounds the cost of every transport plan from below. When a plan is concentrated on the contact set where that constraint is an equality, the two bounds meet: the plan is optimal, the pair is a dual optimizer, and there is no duality gap. This is complementary slackness, and the resulting data is the standard optimality certificate that the Monge and barycentre layers verify instead of re-solving a transport problem.

This file builds that certificate for the raw extended-nonnegative interface — an arbitrary cost c : X × Y → ℝ≥0∞ on arbitrary measurable spaces — and shows that it is exact: in the dual-attainment regime, an optimal plan of almost-everywhere measurable cost is concentrated on the contact set. Measurability of the cost is needed for that converse only, and never for the consequences drawn from a certificate. No topology, compactness, or lower semicontinuity is used, so the certificate applies verbatim to the Borel-cost regime, where a dual optimizer is produced by other means. It is a statement about the unregularized Kantorovich problem only: an entropy-regularized optimizer is characterised by the stationarity condition dπ / d(μ ⊗ ν) = exp ((φ ⊕ ψ - c) / ε) and is typically of full support, so it is not concentrated on a contact set and no claim is made about it here.

The last section connects the cost-level notion of c-cyclical monotonicity to certificates by proving that the contact set of a dual feasible pair is c-cyclically monotone. Hence a certified plan is concentrated on a c-cyclically monotone set, which is measurable as soon as the cost and both potentials are. The converse implication — that concentration on a c-cyclically monotone set forces optimality — is the Schachermayer--Teichmann theorem and is not proved here.

Main definitions

• TauCeti.dualContactSet c φ ψ — the set where the dual constraint for an extended-nonnegative cost holds with equality;
• TauCeti.IsDualCertificate c π μ ν φ ψ — a coupling π together with an integrable dual feasible pair (φ, ψ) on whose contact set π is concentrated;
• TauCeti.IsCyclicallyMonotone c S — finite c-cyclical monotonicity of a set of pairs.

Main statements

• TauCeti.IsDualCertificate.lintegral_eq_ofReal — a certified plan costs exactly the value of its dual pair, with TauCeti.IsDualCertificate.transportCost_eq the resulting absence of a duality gap;
• TauCeti.IsDualCertificate.isOptimalCoupling and TauCeti.IsDualCertificate.kantorovichDualValue_le — a certificate proves primal optimality of the plan and dual optimality of the pair;
• TauCeti.isDualCertificate_iff — complementary slackness: for a fixed coupling π and a fixed feasible integrable pair, being a certificate is exactly having finite cost no larger than the dual value, provided AEMeasurable c π; so TauCeti.IsOptimalCoupling.isDualCertificate recovers the certificate from an optimal plan of almost-everywhere measurable cost whenever the dual value is attained;
• TauCeti.isDualCertificate_graphPlan and TauCeti.transportCost_eq_lintegral_of_ae_mem_dualContactSet — the Monge form: the Kantorovich value is attained at the graph plan of a map whose graph lies almost everywhere in the contact set; together with TauCeti.transportCost_le_lintegral_of_hasLaw, this exhibits the map as a minimizer among transport maps;
• TauCeti.DualFeasible.isCyclicallyMonotone_dualContactSet and TauCeti.IsDualCertificate.exists_isCyclicallyMonotone — contact sets are c-cyclically monotone, and a certified plan whose cost and potentials are measurable is concentrated on a measurable such set.

Implementation notes

TauCeti.contactSet is stated for a finite real cost and extended-real potentials, the signature forced by the c-transform calculus, where a transform of a real potential can take the value -∞. The primal problem instead uses an extended-nonnegative cost, so a plan can be forbidden to charge a pair by setting c to ∞ there, while the potentials appearing in an integrable dual pair are honestly real. TauCeti.dualContactSet is the contact set for that second signature, and TauCeti.dualContactSet_ofReal identifies the two whenever both apply. Membership is an equality of EReals rather than of extended-nonnegative numbers, because ENNReal.ofReal forgets the sign: for c (x, y) = 0 and φ x + ψ y = -1 the two ENNReal.ofReal values agree although the dual constraint is strict.

The complementary slackness converse is stated with the real number (∫⁻ z, c z ∂π).toReal rather than with ENNReal.ofReal (kantorovichDualValue μ ν φ ψ) on purpose: a dual feasible pair can have a negative value, and then ENNReal.ofReal truncates it to 0 and the ℝ≥0∞-valued inequality holds for reasons that have nothing to do with contact. The example above, with both spaces a point, is such a pair.

References

• C. Villani, Topics in Optimal Transportation, Graduate Studies in Mathematics 58, 2003, §1.1.1 and §2.3, for complementary slackness and cyclical monotonicity;
• C. Villani, Optimal Transport: Old and New, Grundlehren 338, 2009, Definition 5.1 and Theorem 5.10;
• F. Santambrogio, Optimal Transport for Applied Mathematicians, Progress in Nonlinear Differential Equations and their Applications 87, 2015, §1.3 and §1.6;
• W. Schachermayer and J. Teichmann, Characterization of optimal transport plans for the Monge--Kantorovich problem, Proc. Amer. Math. Soc. 137 (2009), 519--529, for the converse that is not proved here.

This is Layer 2, items 7 and 8 of the optimal-transport roadmap.

The contact set of an extended-nonnegative cost

def TauCeti.dualContactSet {X : Type u} {Y : Type v} (c : X × Y → ENNReal) (φ : X → ℝ) (ψ : Y → ℝ) : Set (X × Y)

The contact set of a pair of real potentials against an extended-nonnegative cost: the set of pairs where the Kantorovich dual constraint φ x + ψ y ≤ c (x, y) holds with equality. The equality is taken in EReal, so a pair at which the potentials sum to a negative number is never a contact point, and a pair of infinite cost is never one either.

Equations

• TauCeti.dualContactSet c φ ψ = {z : X × Y | ↑(φ z.1 + ψ z.2) = ↑(c z)}

@[simp]

theorem TauCeti.mem_dualContactSet_iff {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} {z : X × Y} : z ∈ dualContactSet c φ ψ ↔ ↑(φ z.1 + ψ z.2) = ↑(c z)

Membership in the contact set, for a point of the product.

theorem TauCeti.mk_mem_dualContactSet_iff {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} {x : X} {y : Y} : (x, y) ∈ dualContactSet c φ ψ ↔ ↑(φ x + ψ y) = ↑(c (x, y))

Membership in the contact set, for an explicit pair.

theorem TauCeti.mem_dualContactSet_iff_ofReal_eq {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} {z : X × Y} : z ∈ dualContactSet c φ ψ ↔ 0 ≤ φ z.1 + ψ z.2 ∧ ENNReal.ofReal (φ z.1 + ψ z.2) = c z

Membership in the contact set, in the extended-nonnegative form used by lintegral. The sign condition cannot be dropped: ENNReal.ofReal is not injective on the reals.

theorem TauCeti.add_nonneg_of_mem_dualContactSet {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} {z : X × Y} (hz : z ∈ dualContactSet c φ ψ) : 0 ≤ φ z.1 + ψ z.2

At a contact point the two potentials sum to a nonnegative number, since the cost is nonnegative.

theorem TauCeti.ofReal_eq_of_mem_dualContactSet {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} {z : X × Y} (hz : z ∈ dualContactSet c φ ψ) : ENNReal.ofReal (φ z.1 + ψ z.2) = c z

At a contact point the cost is the extended-nonnegative image of the sum of the two potentials.

theorem TauCeti.ne_top_of_mem_dualContactSet {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} {z : X × Y} (hz : z ∈ dualContactSet c φ ψ) : c z ≠ ⊤

The cost is finite at a contact point: the potentials are real there.

theorem TauCeti.toReal_eq_of_mem_dualContactSet {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} {z : X × Y} (hz : z ∈ dualContactSet c φ ψ) : (c z).toReal = φ z.1 + ψ z.2

At a contact point the sum of the potentials is the real value of the cost.

theorem TauCeti.mem_dualContactSet_of_toReal_eq {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} {z : X × Y} (hc : c z ≠ ⊤) (h : (c z).toReal = φ z.1 + ψ z.2) : z ∈ dualContactSet c φ ψ

A pair where the dual constraint is an equality, presented in real terms, is a contact point.

theorem TauCeti.dualContactSet_ofReal {X : Type u} {Y : Type v} {c : X × Y → ℝ} (hc : ∀ (z : X × Y), 0 ≤ c z) (φ : X → ℝ) (ψ : Y → ℝ) : dualContactSet (fun (z : X × Y) => ENNReal.ofReal (c z)) φ ψ = contactSet c (fun (x : X) => ↑(φ x)) fun (y : Y) => ↑(ψ y)

The contact set of a nonnegative real cost, viewed through ENNReal.ofReal, is the contact set of the c-transform calculus. This is the bridge between the two signatures.

theorem TauCeti.measurableSet_dualContactSet {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] (hc : Measurable c) (hφ : Measurable φ) (hψ : Measurable ψ) : MeasurableSet (dualContactSet c φ ψ)

The contact set of a measurable cost and measurable potentials is measurable.

Optimality certificates

structure TauCeti.IsDualCertificate {X : Type u} {Y : Type v} [MeasurableSpace X] [MeasurableSpace Y] (c : X × Y → ENNReal) (π : MeasureTheory.Measure (X × Y)) (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) (φ : X → ℝ) (ψ : Y → ℝ) extends TauCeti.IsCoupling π μ ν : Prop

An optimality certificate for the transport problem with cost c and marginals μ, ν: a coupling π together with an integrable dual feasible pair of potentials (φ, ψ) such that π gives full measure to the contact set of the pair. Complementary slackness turns this data into simultaneous primal optimality of π, dual optimality of (φ, ψ), and the absence of a duality gap, with no topological hypothesis whatsoever.

• fst_eq : π.fst = μ
• snd_eq : π.snd = ν
• dualFeasible : DualFeasible (fun (z : X × Y) => ↑(c z)) φ ψ

  The potentials satisfy the Kantorovich dual constraint everywhere.

• integrable_left : MeasureTheory.Integrable φ μ

  The first potential is integrable against the first marginal.

• integrable_right : MeasureTheory.Integrable ψ ν

  The second potential is integrable against the second marginal.

• ae_mem_dualContactSet : ∀ᵐ (z : X × Y) ∂π, z ∈ dualContactSet c φ ψ

  Complementary slackness: the plan is concentrated on the contact set.

theorem TauCeti.lintegral_eq_ofReal_kantorovichDualValue {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} (hπ : IsCoupling π μ ν) (hφ : MeasureTheory.Integrable φ μ) (hψ : MeasureTheory.Integrable ψ ν) (hae : ∀ᵐ (z : X × Y) ∂π, z ∈ dualContactSet c φ ψ) : ∫⁻ (z : X × Y), c z ∂π = ENNReal.ofReal (kantorovichDualValue μ ν φ ψ)

A plan concentrated on the contact set of an integrable pair costs exactly the value of that pair. Dual feasibility is not needed: the contact condition alone pins the cost down.

theorem TauCeti.lintegral_ne_top_of_ae_mem_dualContactSet {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} (hπ : IsCoupling π μ ν) (hφ : MeasureTheory.Integrable φ μ) (hψ : MeasureTheory.Integrable ψ ν) (hae : ∀ᵐ (z : X × Y) ∂π, z ∈ dualContactSet c φ ψ) : ∫⁻ (z : X × Y), c z ∂π ≠ ⊤

A plan concentrated on the contact set of an integrable pair has finite cost.

theorem TauCeti.kantorovichDualValue_nonneg_of_ae_mem_dualContactSet {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} (hπ : IsCoupling π μ ν) (hφ : MeasureTheory.Integrable φ μ) (hψ : MeasureTheory.Integrable ψ ν) (hae : ∀ᵐ (z : X × Y) ∂π, z ∈ dualContactSet c φ ψ) : 0 ≤ kantorovichDualValue μ ν φ ψ

The value of an integrable pair is nonnegative when a coupling is concentrated on its contact set. Dual feasibility is not needed.

theorem TauCeti.lintegral_eq_lintegral_of_ae_mem_dualContactSet {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π σ : MeasureTheory.Measure (X × Y)} (hπ : IsCoupling π μ ν) (hσ : IsCoupling σ μ ν) (hφ : MeasureTheory.Integrable φ μ) (hψ : MeasureTheory.Integrable ψ ν) (hπae : ∀ᵐ (z : X × Y) ∂π, z ∈ dualContactSet c φ ψ) (hσae : ∀ᵐ (z : X × Y) ∂σ, z ∈ dualContactSet c φ ψ) : ∫⁻ (z : X × Y), c z ∂σ = ∫⁻ (z : X × Y), c z ∂π

Two couplings concentrated on the same contact set of an integrable pair have equal cost. Dual feasibility is not needed.

theorem TauCeti.IsDualCertificate.lintegral_eq_ofReal {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} (h : IsDualCertificate c π μ ν φ ψ) : ∫⁻ (z : X × Y), c z ∂π = ENNReal.ofReal (kantorovichDualValue μ ν φ ψ)

A certified plan costs exactly the value of its dual pair.

theorem TauCeti.IsDualCertificate.kantorovichDualValue_nonneg {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} (h : IsDualCertificate c π μ ν φ ψ) : 0 ≤ kantorovichDualValue μ ν φ ψ

The value of a certified dual pair is nonnegative, because the cost is.

theorem TauCeti.IsDualCertificate.transportCost_eq {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} (h : IsDualCertificate c π μ ν φ ψ) : transportCost c μ ν = ENNReal.ofReal (kantorovichDualValue μ ν φ ψ)

No duality gap. The primal value equals the value of a certified dual pair.

theorem TauCeti.IsDualCertificate.transportCost_ne_top {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} (h : IsDualCertificate c π μ ν φ ψ) : transportCost c μ ν ≠ ⊤

A certificate exhibits a plan of finite cost, so the primal value is finite.

theorem TauCeti.IsDualCertificate.isOptimalCoupling {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} (h : IsDualCertificate c π μ ν φ ψ) : IsOptimalCoupling c π μ ν

The certificate proves primal optimality.

theorem TauCeti.IsDualCertificate.toReal_transportCost_eq {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} (h : IsDualCertificate c π μ ν φ ψ) : (transportCost c μ ν).toReal = kantorovichDualValue μ ν φ ψ

The primal value in real terms.

theorem TauCeti.IsDualCertificate.kantorovichDualValue_le {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} (h : IsDualCertificate c π μ ν φ ψ) {φ' : X → ℝ} {ψ' : Y → ℝ} (hfeas : DualFeasible (fun (z : X × Y) => ↑(c z)) φ' ψ') (hφ' : MeasureTheory.Integrable φ' μ) (hψ' : MeasureTheory.Integrable ψ' ν) : kantorovichDualValue μ ν φ' ψ' ≤ kantorovichDualValue μ ν φ ψ

The certificate proves dual optimality. No other integrable feasible pair has a larger value.

theorem TauCeti.IsDualCertificate.lintegral_eq_of_ae_mem_dualContactSet {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} (h : IsDualCertificate c π μ ν φ ψ) {σ : MeasureTheory.Measure (X × Y)} (hσ : IsCoupling σ μ ν) (hae : ∀ᵐ (z : X × Y) ∂σ, z ∈ dualContactSet c φ ψ) : ∫⁻ (z : X × Y), c z ∂σ = ∫⁻ (z : X × Y), c z ∂π

Any other coupling concentrated on the same contact set has the same cost.

theorem TauCeti.isDualCertificate_iff {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} (hc : AEMeasurable c π) (hπ : IsCoupling π μ ν) (hfeas : DualFeasible (fun (z : X × Y) => ↑(c z)) φ ψ) (hφ : MeasureTheory.Integrable φ μ) (hψ : MeasureTheory.Integrable ψ ν) : IsDualCertificate c π μ ν φ ψ ↔ ∫⁻ (z : X × Y), c z ∂π ≠ ⊤ ∧ (∫⁻ (z : X × Y), c z ∂π).toReal ≤ kantorovichDualValue μ ν φ ψ

Complementary slackness. For a fixed coupling and a fixed integrable dual feasible pair, being an optimality certificate is exactly having finite cost that does not exceed the value of the pair. The inequality is stated between real numbers: ENNReal.ofReal truncates a negative dual value to 0, and then the extended-nonnegative inequality carries no information.

theorem TauCeti.IsOptimalCoupling.isDualCertificate {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} (hc : AEMeasurable c π) (hopt : IsOptimalCoupling c π μ ν) (hfeas : DualFeasible (fun (z : X × Y) => ↑(c z)) φ ψ) (hφ : MeasureTheory.Integrable φ μ) (hψ : MeasureTheory.Integrable ψ ν) (htop : transportCost c μ ν ≠ ⊤) (hattain : (transportCost c μ ν).toReal = kantorovichDualValue μ ν φ ψ) : IsDualCertificate c π μ ν φ ψ

In the dual-attainment regime, optimality is contact-set concentration. An optimal plan of finite cost whose dual value is attained by an integrable feasible pair is certified by that pair.

theorem TauCeti.IsDualCertificate.of_isOptimalCoupling {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} (h : IsDualCertificate c π μ ν φ ψ) {σ : MeasureTheory.Measure (X × Y)} (hcσ : AEMeasurable c σ) (hσ : IsOptimalCoupling c σ μ ν) : IsDualCertificate c σ μ ν φ ψ

Once one certificate witnesses dual attainment, every optimal coupling with an almost-everywhere measurable cost is certified by the same potentials.

The Monge form of the certificate

theorem TauCeti.isDualCertificate_graphPlan {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {T : X → Y} (hc : AEMeasurable c (graphPlan T μ)) (hT : ProbabilityTheory.HasLaw T ν μ) (hfeas : DualFeasible (fun (z : X × Y) => ↑(c z)) φ ψ) (hφ : MeasureTheory.Integrable φ μ) (hψ : MeasureTheory.Integrable ψ ν) (hae : ∀ᵐ (x : X) ∂μ, (x, T x) ∈ dualContactSet c φ ψ) : IsDualCertificate c (graphPlan T μ) μ ν φ ψ

A transport map whose graph lies almost everywhere in the contact set of an integrable dual feasible pair is certified: its graph plan is an optimality certificate. This is the form in which the Brenier and polar-factorisation layers verify optimality of a map.

theorem TauCeti.transportCost_eq_lintegral_of_ae_mem_dualContactSet {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {T : X → Y} (hc : AEMeasurable c (graphPlan T μ)) (hT : ProbabilityTheory.HasLaw T ν μ) (hfeas : DualFeasible (fun (z : X × Y) => ↑(c z)) φ ψ) (hφ : MeasureTheory.Integrable φ μ) (hψ : MeasureTheory.Integrable ψ ν) (hae : ∀ᵐ (x : X) ∂μ, (x, T x) ∈ dualContactSet c φ ψ) : transportCost c μ ν = ∫⁻ (x : X), c (x, T x) ∂μ

The Kantorovich value is attained at the graph plan of a certified transport map. With TauCeti.transportCost_le_lintegral_of_hasLaw, this exhibits the map as a minimizer among transport maps.

Certificates and c-cyclical monotonicity

theorem TauCeti.DualFeasible.isCyclicallyMonotone_dualContactSet {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} (h : DualFeasible (fun (z : X × Y) => ↑(c z)) φ ψ) : IsCyclicallyMonotone c (dualContactSet c φ ψ)

The contact set of a dual feasible pair is c-cyclically monotone. Rearranging the targets replaces each equality φ (x i) + ψ (y i) = c (x i, y i) by an inequality, while the two total sums of potentials agree because a permutation does not change a finite sum.

theorem TauCeti.IsDualCertificate.exists_isCyclicallyMonotone {X : Type u} {Y : Type v} {c : X × Y → ENNReal} {φ : X → ℝ} {ψ : Y → ℝ} [MeasurableSpace X] [MeasurableSpace Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} {π : MeasureTheory.Measure (X × Y)} (h : IsDualCertificate c π μ ν φ ψ) (hc : Measurable c) (hφm : Measurable φ) (hψm : Measurable ψ) : ∃ (S : Set (X × Y)), MeasurableSet S ∧ IsCyclicallyMonotone c S ∧ π Sᶜ = 0

A certified plan with measurable cost and potentials is concentrated on a measurable c-cyclically monotone set. The converse implication, that concentration on a c-cyclically monotone set forces optimality, is the Schachermayer--Teichmann theorem and needs topological hypotheses.