Section 3, eq. (3.1) — weak Monge–Kantorovich duality

Proved

MongeKantorovichYao.weak_duality

by Lucas · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

dualitymeasure-theoryoptimal-transport

Let $X,Y$ be measurable spaces, $\mu$ and $\nu$ measures on $X$ and $Y$ , and $c : X\times Y\to\mathbb R$ a cost function. Let $\pi\in\Pi(\mu,\nu)$ be a transference plan with $c\in L^1(\pi)$ , and let $\psi\in L^1(\mu)$ , $\varphi\in L^1(\nu)$ satisfy $\psi(x)+\varphi(y)\le c(x,y)$ for all $x\in X$ , $y\in Y$ . Then

\int_X\psi\,d\mu+\int_Y\varphi\,d\nu\le\int_{X\times Y}c\,d\pi .

Taking the infimum over plans and the supremum over admissible pairs gives the weak duality inequality (3.1): $\inf_{\pi}\int c\,d\pi\ge\sup_{\psi,\varphi}\big(\int\psi\,d\mu+\int\varphi\,d\nu\big)$ .

Formalization Note The statement is given plan-by-plan (equivalent to the inf/sup form). Integrability of $c$ with respect to $\pi$ is assumed so that $\int c\,d\pi$ is a genuine finite integral; the constraint $\psi+\varphi\le c$ is imposed at every point, as in the proof in the source.

Preamble

import Mathlib
import Definitions.Def_MongeKantorovichYao_Defs

open MeasureTheory

Formal statement

namespace MongeKantorovichYao

theorem weak_duality {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
    (μ : Measure X) (ν : Measure Y) (c : X × Y → ℝ)
    (π : Measure (X × Y)) (hπ : π ∈ transferencePlans μ ν)
    (ψ : X → ℝ) (φ : Y → ℝ) (hψ : Integrable ψ μ) (hφ : Integrable φ ν)
    (hc : Integrable c π) (hfeas : ∀ x y, ψ x + φ y ≤ c (x, y)) :
    ∫ x, ψ x ∂μ + ∫ y, φ y ∂ν ≤ ∫ p, c p ∂π := by sorry

end MongeKantorovichYao

Source

Colin Yao, *Monge–Kantorovich and Transportation Theory* (paper dated September 10, 2023), pp. 5–6, Section 3 (Weak Monge–Kantorovich), inequality (3.1) and its proof

Read-back

What the Lean code literally says, in plain math · Aristotle by Harmonic (same agent as the drafter; non-blind)

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement, with full knowledge of the source paper and of the intended meaning. It is not a blind audit and must not be mistaken for independent testimony; reviewers should compare the Lean code against the source themselves (or obtain an independent read-back).

Data. Arbitrary types $X,Y$ with σ-algebras (no topology). Measures $\mu$ on $X$ , $\nu$ on $Y$ (arbitrary), a function $c : X\times Y\to\mathbb R$ , a measure $\pi$ on $X\times Y$ , and real functions $\psi$ on $X$ , $\varphi$ on $Y$ .

Hypotheses.

$\pi\in\Pi(\mu,\nu)$ : $\pi$ is a probability measure whose first-coordinate pushforward is $\mu$ and second-coordinate pushforward is $\nu$ (so $\mu,\nu$ are forced to be probability measures).
$\psi$ is Bochner-integrable with respect to $\mu$ ; $\varphi$ is integrable with respect to $\nu$ .
$c$ is integrable with respect to $\pi$ .
For all $x\in X$ and $y\in Y$ : $\psi(x)+\varphi(y)\le c(x,y)$ .

Conclusion.

\int_X\psi\,d\mu+\int_Y\varphi\,d\nu\ \le\ \int_{X\times Y}c\,d\pi,

all three being ordinary real-valued (Bochner) integrals. It is a statement about one fixed plan and one fixed pair; no infimum or supremum appears.

Human review

Endorsed by Shuze Chen · Sep 30, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph