Monge–Kantorovich existence theorem

monge_kantorovich

Submitter: Kim Morrison.

Notes: §73 of Oliver Knill's 'Some Fundamental Theorems in Mathematics'. The Monge–Kantorovich existence theorem states that for Polish probability spaces (X, P) and (Y, Q) and a continuous cost c : X × Y → [0, ∞], the functional π ↦ ∫ c dπ attains its minimum over all couplings of P and Q (the probability measures on X × Y with marginals P and Q). This is the basic existence result for optimal transport plans. Mathlib has the surrounding measure-theoretic and topological infrastructure — marginals, probability measures, weak convergence, Prokhorov-type compactness — but no dedicated coupling or Kantorovich-cost API and no theorem asserting existence of an optimal coupling.

Source: L. V. Kantorovich (1942), after G. Monge (1781). Listed as §73 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: The set of couplings Π(P, Q) is nonempty (the product measure P ⊗ Q is a coupling), and it is tight and weakly closed: each marginal P, Q is tight by Prokhorov on a Polish space, tightness of the marginals gives tightness of the couplings, and the marginal constraints π.fst = P, π.snd = Q are preserved under weak limits, so by Prokhorov's theorem Π(P, Q) is weakly compact. The Kantorovich functional π ↦ ∫ c dπ is weakly lower semicontinuous because c is continuous and nonnegative (write c as an increasing limit of bounded continuous functions and use the portmanteau characterisation). A lower semicontinuous function on a (nonempty) compact set attains its infimum, giving an optimal coupling.

theorem declaration uses `sorry`monge_kantorovich_exists {X Y : Type*}
    [TopologicalSpace X] [PolishSpace X] [MeasurableSpace X] [BorelSpace X]
    [TopologicalSpace Y] [PolishSpace Y] [MeasurableSpace Y] [BorelSpace Y]
    (P : Measure X) (Q : Measure Y)
    [IsProbabilityMeasure P] [IsProbabilityMeasure Q]
    (c : X × Y → ENNReal) (_hc : Continuous c) :
    ∃ π ∈ LeanEval.Analysis.Couplings P Q,
      ∀ π' ∈ LeanEval.Analysis.Couplings P Q, kantorovichCost c π ≤ kantorovichCost c π' := byX:Type u_1Y:Type u_2inst✝⁹:TopologicalSpace Xinst✝⁸:PolishSpace Xinst✝⁷:MeasurableSpace Xinst✝⁶:BorelSpace Xinst✝⁵:TopologicalSpace Yinst✝⁴:PolishSpace Yinst✝³:MeasurableSpace Yinst✝²:BorelSpace YP:Measure XQ:Measure Yinst✝¹:IsProbabilityMeasure Pinst✝:IsProbabilityMeasure Qc:X × Y → ENNReal_hc:Continuous c⊢ ∃ π ∈ Couplings P Q, ∀ π' ∈ Couplings P Q, kantorovichCost c π ≤ kantorovichCost c π'
  sorryAll goals completed! 🐙

Solved by

• @GanjinZero with Seed Prover (ByteDance) on Jun 2, 2026

• @LorenzoLuccioli with Aristotle (Harmonic) on Jun 2, 2026

• @mayorov-m-a with Aleph Prover(logicalintelligence.com) on Jun 3, 2026