Prove2Me

Supply–demand theorem (fractional Hall): a bipartite transport meeting real demands and capacities exactly

Proved
AGT.fractional_hall

by korbonits · Sep 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

algorithmic-game-theorycombinatoricshall-theoremnetwork-flow

The supply–demand theorem (Gale 1957; Ford–Fulkerson 1962), in its bipartite, real-valued form. Let JJ be a finite set of buyers and SS a finite set of goods. Buyer jj has a demand mj≥0m_j \ge 0 and may be served only by the goods in a prescribed set Γj∩S\Gamma_j \cap S; good aa has a capacity ca≥0c_a \ge 0. For a set J′⊆JJ' \subseteq J of buyers write Γ(J′)=⋃j∈J′Γj\Gamma(J') = \bigcup_{j \in J'} \Gamma_j for the goods they can reach. Suppose

  1. total demand equals total capacity, ∑j∈Jmj=∑a∈Sca\displaystyle\sum_{j \in J} m_j = \sum_{a \in S} c_a, and
  2. (Hall's condition) every set of buyers can be served: ∑j∈J′mj  ≤  ∑a∈Γ(J′)∩Sca\displaystyle\sum_{j \in J'} m_j \;\le\; \sum_{a \in \Gamma(J') \cap S} c_a for every J′⊆JJ' \subseteq J.

Then there is a transport x=(xja)x = (x_{ja}) with

xja≥0,xja≠0  ⟹  j∈J, a∈S, a∈Γj,∑a∈Sxja=mj  (j∈J),∑j∈Jxja=ca  (a∈S).x_{ja} \ge 0,\qquad x_{ja} \ne 0 \implies j \in J,\ a \in S,\ a \in \Gamma_j,\qquad \sum_{a \in S} x_{ja} = m_j\ \ (j \in J),\qquad \sum_{j \in J} x_{ja} = c_a\ \ (a \in S).

This is the fractional (or weighted) version of Hall's marriage theorem: with unit demands and capacities and an integral transport it is Hall's theorem, and for general nonnegative reals it is the feasibility criterion for a bipartite transportation problem, usually derived from the max-flow min-cut theorem. It is the combinatorial engine behind the existence of market-clearing prices in the linear 0/1 market of Algorithmic Game Theory, Section 1.8.1 (milestone AGT.market_clearing_existence): once the equilibrium prices are known, the allocation of money to goods is exactly a transport of this kind for each price level.

A note on the hypotheses. Both conditions are necessary. The empty case is allowed: if J=∅J = \varnothing then (1) forces every capacity to vanish and the zero transport works. Demands and capacities are real numbers, not integers; no divisibility or rationality is assumed.

Formalization Note. Buyers and goods are elements of arbitrary types B, A, and the instance is specified by finsets J : Finset B, S : Finset A, the adjacency adj : B → Finset A, and real-valued m, c. The reachable goods of J' are J'.biUnion adj ∩ S. The transport is a total function x : B → A → ℝ whose support is required to lie in the admissible pairs. Only DecidableEq A is assumed, for the finset operations in the statement.

Preamble
import Mathlib.Data.Real.Basic
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
Formal statement
namespace AGT

/-- **Supply–demand theorem** (bipartite, real-valued; Gale 1957, Ford–Fulkerson
1962, Ch. II §3).  Buyers `j ∈ J` carry demands `m j ≥ 0` and may be served by
the goods `adj j ∩ S`; goods `a ∈ S` carry capacities `c a ≥ 0`.  If the total
demand equals the total capacity and every set `J'` of buyers has demand at
most the capacity of the goods it can reach, then there is a nonnegative
transport `x j a`, supported on the admissible pairs, meeting every demand
exactly and using every capacity exactly. -/
theorem fractional_hall {A B : Type*} [DecidableEq A]
    (J : Finset B) (S : Finset A) (adj : B → Finset A) (m : B → ℝ) (c : A → ℝ)
    (hm : ∀ j ∈ J, 0 ≤ m j) (hc : ∀ a ∈ S, 0 ≤ c a)
    (hHall : ∀ J' ⊆ J, ∑ j ∈ J', m j ≤ ∑ a ∈ J'.biUnion adj ∩ S, c a)
    (htot : ∑ j ∈ J, m j = ∑ a ∈ S, c a) :
    ∃ x : B → A → ℝ, (∀ j a, 0 ≤ x j a) ∧
      (∀ j a, x j a ≠ 0 → j ∈ J ∧ a ∈ S ∧ a ∈ adj j) ∧
      (∀ j ∈ J, ∑ a ∈ S, x j a = m j) ∧
      (∀ a ∈ S, ∑ j ∈ J, x j a = c a) := by
  sorry

end AGT
Source
D. Gale, A theorem on flows in networks, Pacific J. Math. 7 (1957), 1073-1082, https://doi.org/10.2140/pjm.1957.7.1073, Theorem 1 (feasibility theorem), specialized to bipartite supply-demand networks; L. R. Ford, D. R. Fulkerson, Flows in Networks, Princeton Univ. Press 1962, Chapter II, Section 3, Theorem 3.1 (Supply-Demand Theorem) and its bipartite corollary; used for Lemmas 1.15-1.16 / Theorem 1.17 of Nisan-Roughgarden-Tardos-Vazirani (eds.), Algorithmic Game Theory, Cambridge 2007, Section 1.8.1, pp. 22-26 (max-flow feasibility of the allocation).

View graph