Primal–dual representation of D(J; q): the transportation LP and its dual both attain D(J; q)

Proved

ScenarioReduction.Redistribution.primal_dual_representation

by mikedeng1 · Sep 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-programminglp-dualityoptimal-transportp2o-batch-p100ap2o-gran-per-chapterp2o-plan-paperp2o-v1stochastic-programming

Let $P=\sum_{i=1}^N p_i\delta_{\omega_i}$ with $p_i>0$ and $\sum_i p_i=1$ , let $c:\Omega\times\Omega\to\mathbb R_+$ satisfy $c(\omega,\tilde\omega)=0$ iff $\omega=\tilde\omega$ and $c(\omega,\tilde\omega)=c(\tilde\omega,\omega)$ , and write $c_{ij}=c(\omega_i,\omega_j)$ . Let $J\subset\{1,\dots,N\}$ and let $q$ be reduced weights: $q_j\ge0$ for $j\notin J$ and $\sum_{j\notin J}q_j=1$ . Then the Kantorovich functional $D(J;q)$ of (10) is both the minimum of the transportation problem and the maximum of its dual:

D(J;q)=\min\Big\{\sum_{i,j}c_{ij}\eta_{ij}:\eta_{ij}\ge0,\ \sum_{j\notin J}\eta_{ij}=p_i,\ i\in I,\ \sum_{i=1}^N\eta_{ij}=q_j,\ j\notin J\Big\}=\max\Big\{\sum_{i=1}^Np_iu_i+\sum_{j\notin J}q_jv_j: u_i+v_j\le c_{ij},\ i\in I,\ j\notin J\Big\}.

Both extrema are attained. This is strong duality for a balanced transportation problem, and it is the tool the proof of Theorem 2 uses in both directions: dual feasible points give lower bounds on $D(J;q)$ and primal feasible plans give upper bounds.

Formalization Note The first conjunct says $D(J;q)$ is the least transport cost over feasible plans (so the infimum is attained); the second says it is the greatest dual objective over dual-feasible $(u,v)$ , with $u,v$ unrestricted in sign. Only entries $\eta_{ij}$ , $v_j$ with $j\notin J$ enter. The standing assumptions of §3 are carried; the measurability, continuity (C3) and growth (C4) conditions on $c$ concern $\Omega\subset\mathbb R^s$ and are dropped, so $\Omega$ is an arbitrary set.

Preamble

import Mathlib
import Definitions.Def_ScenarioReduction_Redistribution_transportValue

open Finset

Formal statement

namespace ScenarioReduction.Redistribution

theorem primal_dual_representation {Ω : Type*} {N : ℕ} (c : Ω → Ω → ℝ) (ω : Fin N → Ω) (p : Fin N → ℝ)
    (hc : ∀ a b : Ω, 0 ≤ c a b) (hc1 : ∀ a b : Ω, c a b = 0 ↔ a = b)
    (hc2 : ∀ a b : Ω, c a b = c b a)
    (hp : ∀ i, 0 < p i) (hp1 : ∑ i, p i = 1)
    (J : Finset (Fin N)) (q : Fin N → ℝ) (hq : IsReducedWeight J q) :
    IsLeast {x : ℝ | ∃ η : Fin N → Fin N → ℝ, IsTransportPlan p J q η ∧ x = transportCost c ω J η}
        (transportValue c ω p J q) ∧
      IsGreatest {x : ℝ | ∃ u v : Fin N → ℝ, IsDualFeasible c ω J u v ∧ x = dualObjective p J q u v}
        (transportValue c ω p J q) := by sorry

end ScenarioReduction.Redistribution

Source

Dupačová, Gröwe-Kuska, Römisch, Scenario reduction in stochastic programming, Math. Program. Ser. A 95 (2003), p. 501, §3, proof of Theorem 2, first display (lead-in at the foot of p. 500); cf. p. 495

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

The data are:

an arbitrary type $\Omega$ ;
$N \in \mathbb{N}$ ;
a function $c : \Omega \times \Omega \to \mathbb{R}$ ;
points $\omega : [N] \to \Omega$ , where $[N] = \{0, \dots, N-1\}$ ;
a vector $p : [N] \to \mathbb{R}$ ;
a subset $J \subseteq [N]$ ;
a vector $q : [N] \to \mathbb{R}$ .

The hypotheses are:

$c(a, b) \ge 0$ for all $a, b \in \Omega$ ;
$c(a, b) = 0 \iff a = b$ ;
$c(a, b) = c(b, a)$ ;
$p_i > 0$ for every $i$ , and $\sum_{i \in [N]} p_i = 1$ ;
$q$ is a reduced weight for $J$ : $q_j \ge 0$ for $j \notin J$ and $\sum_{j \notin J} q_j = 1$ , with $q_j$ for $j \in J$ unconstrained.

The theorem refers to $D(J; q)$ , defined as the infimum of $\sum_{i \in [N]} \sum_{j \notin J} c(\omega_i, \omega_j)\, \eta_{ij}$ over all matrices $\eta$ with:

$\eta_{ij} \ge 0$ for all $i$ and all $j \notin J$ ;
$\sum_{j \notin J} \eta_{ij} = p_i$ for every $i \in [N]$ ;
$\sum_{i \in [N]} \eta_{ij} = q_j$ for every $j \notin J$ .

Entries $\eta_{ij}$ with $j \in J$ are free. The infimum is $0$ if the set is empty or unbounded below.

The theorem asserts two things:

Primal side. $D(J; q)$ is the least element of the set of such costs. So a feasible plan exists, some feasible plan attains cost exactly $D(J; q)$ , and every feasible plan costs at least $D(J; q)$ .
Dual side. $D(J; q)$ is the greatest element of the set

\Big\{\sum_{i \in [N]} p_i u_i + \sum_{j \notin J} q_j v_j \;:\; u, v : [N] \to \mathbb{R},\ u_i + v_j \le c(\omega_i, \omega_j) \ \text{for all } i \in [N],\ j \notin J\Big\}.

So some dual-feasible pair $(u, v)$ attains $D(J; q)$ , and no dual-feasible pair exceeds it. The values $v_j$ for $j \in J$ play no role.

Degenerate cases:

$N = 0$ . The condition $\sum_i p_i = 1$ cannot hold, so the statement is vacuous.
$J = [N]$ . The reduced-weight condition requires an empty sum to equal $1$ , which is impossible, so the statement is vacuous. The effective cases therefore have $N \ge 1$ and $J^c \neq \emptyset$ .
$J = \emptyset$ . The statement is about transport from $p$ to $q$ on all of $[N]$ .
$\Omega$ empty. Then $N \ge 1$ leaves no possible $\omega$ .
Repeated points. $\omega$ need not be injective; if $\omega_i = \omega_j$ , then $c(\omega_i, \omega_j) = 0$ .

Human review

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

View graph