Proof of Theorem 4.10 — with $k \ge n^2$ tasks some agent receives at least $n$ tasks

Proved

AlgMechDesign.Additive.exists_agent_many_tasks

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

mechanism-designp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1scheduling

Let there be $n \ge 1$ agents and $k \ge n^2$ tasks. Then for every allocation $x$ of the tasks to the agents there is an agent $i$ with

|x^i| \ge n .

This is the pigeonhole step behind the sentence "Without loss of generality we assume that $|x^1(t)| \ge n$ " in the proof of Theorem 4.10, applied there to the allocation chosen at the all-ones type vector.

Preamble

import Mathlib
import Definitions.Def_AlgMechDesign_Additive_Model

Formal statement

namespace AlgMechDesign.Additive

/-- Proof of Theorem 4.10, p. 180 (the step "Without loss of generality we assume that
`|x¹(t)| ≥ n`"): with `n ≥ 1` agents and `k ≥ n²` tasks, every allocation gives some agent at
least `n` tasks. -/
theorem exists_agent_many_tasks {n k : ℕ} [NeZero n] (hk : n ^ 2 ≤ k) (x : Fin k → Fin n) :
    ∃ i : Fin n, n ≤ (taskSet x i).card := by sorry

end AlgMechDesign.Additive

Source

Nisan, Ronen, Algorithmic Mechanism Design, Games Econ. Behav. 35, 2001, p. 180, proof of Theorem 4.10, first paragraph

Human review

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

View graph

Proof of Theorem 4.10 — with k≥n2k \ge n^2k≥n2 tasks some agent receives at least nnn tasks

Proof of Theorem 4.10 — with $k \ge n^2$ tasks some agent receives at least $n$ tasks