Sec. 3.3, p. 122 — coordinate differences of core vectors are bounded by $u^_i - u_{i}$ and $v^_j - v_{j}$

Proved

AssignmentGame.CoreCorners.core_coord_diff_le

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

assignment-gamecooperative-gamesp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $M$ (sellers) and $N$ (buyers) be finite sets and $a_{ij} \ge 0$ . For a seller $i$ let $u^*_i$ and $u_{*i}$ be the highest and lowest payoff to $i$ over the core, and for a buyer $j$ let $v^*_j$ and $v_{*j}$ be defined likewise. Then any two core vectors $(u', v')$ and $(u'', v'')$ satisfy

|u'_i - u''_i| \le u^*_i - u_{*i} \quad \text{for all } i \in M, \qquad |v'_j - v''_j| \le v^*_j - v_{*j} \quad \text{for all } j \in N.

Combined with Theorem 3, these inequalities show that the two corners are the farthest-apart pair of core points for every distance that depends only on the absolute values of the coordinate differences , not only for Euclidean distance.

Formalization Note $u^*_i, u_{*i}, v^*_j, v_{*j}$ are the real supremum and infimum over the core (uHi, uLo, vHi, vLo); they are the true extrema because the core is nonempty and bounded (the other milestones).

Preamble

import Mathlib
import Definitions.Def_AssignmentGame_CoreCorners_Game

open Finset

Formal statement

namespace AssignmentGame.CoreCorners

/-- Sec. 3.3, p. 122: any two core vectors differ, in each coordinate, by at most the spread
between the highest and the lowest core payoff of that player. -/
theorem core_coord_diff_le {M N : Type*} [Fintype M] [Fintype N]
    (a : M → N → ℝ) (ha : ∀ i j, 0 ≤ a i j)
    (u' u'' : M → ℝ) (v' v'' : N → ℝ)
    (h' : (u', v') ∈ core a) (h'' : (u'', v'') ∈ core a) :
    (∀ i : M, |u' i - u'' i| ≤ uHi a i - uLo a i) ∧
    (∀ j : N, |v' j - v'' j| ≤ vHi a j - vLo a j) := by sorry

end AssignmentGame.CoreCorners

Source

Shapley and Shubik, The Assignment Game I: The Core, Int. J. Game Theory 1 (1971), p. 122, Sec. 3.3 (displayed inequalities after the proof of Theorem 3)

Read-back

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

This theorem takes arbitrary finite types $M$ and $N$ , a real matrix $a$ with $a_{ij} \ge 0$ for all $i, j$ , and two pairs $(u',v')$ and $(u'',v'')$ in $\mathrm{Core}(a)$ .

The core is the set of $(u,v) \in \mathbb{R}^M\times\mathbb{R}^N$ with both:

\sum_i u_i + \sum_j v_j = w_a(M,N)

and

\sum_{i\in A} u_i + \sum_{j\in B} v_j \ge w_a(A,B) \ \text{ for all } A\subseteq M,\ B\subseteq N.

The worth $w_a(A,B)$ is the maximum of $\sum_{(i,j)\in P} a_{ij}$ over partial matchings inside $A\times B$ , with the empty matching allowed.

The theorem asserts:

|u'_i - u''_i| \le u^*_i - u_{*i} \quad\text{for every } i \in M,

|v'_j - v''_j| \le v^*_j - v_{*j} \quad\text{for every } j \in N.

The quantities on the right are defined as follows:

u^*_i = \sup\{u_i : (u,v)\in\mathrm{Core}(a)\}, \qquad u_{*i} = \inf\{u_i : (u,v)\in\mathrm{Core}(a)\},

and similarly $v^*_j$ and $v_{*j}$ are the supremum and infimum of the $j$ -th buyer coordinate over the core.

Degenerate cases:

Sup/inf convention. These use the real supremum and infimum under the total-function convention: $0$ for an empty set, and $0$ for a set with no upper bound (for the supremum) or no lower bound (for the infimum).
Nonemptiness and boundedness. The hypotheses guarantee that each coordinate set is nonempty, since it contains $u'_i$ and $u''_i$ . The statement's own hypotheses do not include boundedness of those sets. If a coordinate set were unbounded, the relevant extreme would be the value $0$ , not $\pm\infty$ .
Empty $M$ or $N$ . If $M$ is empty, the first conjunct is vacuous; if $N$ is empty, the second is.
Equal vectors. If the two core vectors are equal, the claim reduces to $0 \le u^*_i - u_{*i}$ and $0 \le v^*_j - v_{*j}$ .

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

Sec. 3.3, p. 122 — coordinate differences of core vectors are bounded by ui∗−u∗iu^*_i - u_{*i}ui∗​−u∗i​ and vj∗−v∗jv^*_j - v_{*j}vj∗​−v∗j​

Sec. 3.3, p. 122 — coordinate differences of core vectors are bounded by $u^_i - u_{i}$ and $v^_j - v_{j}$