Proof of Claim 4.3 — every allocation has make-span at least $\frac1n\sum_j \min_i t^i_j$

Proved

AlgMechDesign.MinWork.sum_minTime_le_n_makespan

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

approximationp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1scheduling

Let $n \ge 1$ and let $t$ be a positive type vector. For every allocation $y$ of the $k$ tasks (in particular an optimal allocation $\mathrm{opt}(t)$ ),

g(y, t) \ge \frac{1}{n} \sum_{j=1}^k \min_i t^i_j .

This is the lower half of the proof of Claim 4.3.

Preamble

import Mathlib
import Definitions.Def_AlgMechDesign_MinWork_Model
import Definitions.Def_AlgMechDesign_MinWork_Mechanism

Formal statement

namespace AlgMechDesign.MinWork

/-- Proof of Claim 4.3, second bound: every allocation `y` (in particular an optimal one) has
make-span at least `(1/n) ∑_j minᵢ tⁱ_j`. -/
theorem sum_minTime_le_n_makespan {n k : ℕ} [NeZero n]
    (t : Fin n → Fin k → ℝ) (ht : IsType t) (y : Fin k → Fin n) :
    1 / (n : ℝ) * ∑ j, minTime t j ≤ makespan t y := by sorry

end AlgMechDesign.MinWork

Source

Nisan, Ronen, Algorithmic Mechanism Design, Games Econ. Behav. 35, 2001, p. 177, proof of Claim 4.3, second inequality

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 Claim 4.3 — every allocation has make-span at least 1n∑jmin⁡itji\frac1n\sum_j \min_i t^i_jn1​∑j​mini​tji​

Proof of Claim 4.3 — every allocation has make-span at least $\frac1n\sum_j \min_i t^i_j$