TightList

The unit-job family: optimum m, list-schedule makespan 2m − 1.

theorem GrahamLPT.tl_unitJobs_apply_lt (m : ℕ) (j : Fin (m * (m - 1) + 1)) (h : ↑j < m * (m - 1)) : unitJobs m j = 1

theorem GrahamLPT.tl_unitJobs_apply_last (m : ℕ) (j : Fin (m * (m - 1) + 1)) (h : m * (m - 1) ≤ ↑j) : unitJobs m j = ↑m

theorem GrahamLPT.tl_unitJobs_nonneg (m : ℕ) (j : Fin (m * (m - 1) + 1)) : 0 ≤ unitJobs m j

theorem GrahamLPT.tl_loadBefore_eq_card (m : ℕ) (σ : Fin (m * (m - 1) + 1) → Fin m) (k : ℕ) (hk : k ≤ m * (m - 1)) (i : Fin m) : loadBefore (unitJobs m) σ k i = ↑{j : Fin (m * (m - 1) + 1) | ↑j < k ∧ σ j = i}.card

Before the long job, the load of a machine is the number of its jobs.

theorem GrahamLPT.tl_sum_filter_lt (m k : ℕ) (hk : k ≤ m * (m - 1)) : ∑ j : Fin (m * (m - 1) + 1) with ↑j < k, unitJobs m j = ↑k

The jobs before k ≤ m(m − 1) have total length k.

theorem GrahamLPT.tl_nat_le (m c : ℕ) (hm : 1 ≤ m) (h : m * c ≤ m * (m - 1) + (m - 1)) : c ≤ m - 1

theorem GrahamLPT.tl_div_lt (m j : ℕ) (hm : 0 < m) (h : j < m * (m - 1)) : j / m < m - 1

theorem GrahamLPT.tl_loadBefore_le (m : ℕ) [NeZero m] (σ : Fin (m * (m - 1) + 1) → Fin m) (hσ : IsListSchedule (unitJobs m) σ) (k : ℕ) (hk : k ≤ m * (m - 1)) (i : Fin m) : ↑m * loadBefore (unitJobs m) σ k i ≤ ↑k + ↑m - 1

The invariant of a list schedule of the unit jobs: m · loadBefore k i ≤ k + m − 1 for k ≤ m(m − 1).

theorem GrahamLPT.tl_loadBefore_units (m : ℕ) [NeZero m] (σ : Fin (m * (m - 1) + 1) → Fin m) (hσ : IsListSchedule (unitJobs m) σ) (i : Fin m) : loadBefore (unitJobs m) σ (m * (m - 1)) i = ↑m - 1

Every load after the unit jobs is m − 1.

theorem GrahamLPT.tl_le_makespan (m : ℕ) [NeZero m] (τ : Fin (m * (m - 1) + 1) → Fin m) : ↑m ≤ makespan (unitJobs m) τ

theorem GrahamLPT.tl_exists_makespan_eq (m : ℕ) [NeZero m] : ∃ (τ : Fin (m * (m - 1) + 1) → Fin m), makespan (unitJobs m) τ = ↑m

An assignment of makespan m: the unit jobs spread m per machine over m − 1 machines, the long job alone.

theorem GrahamLPT.unitJobs_optMakespan (m : ℕ) [NeZero m] : optMakespan m (unitJobs m) = ↑m

The m(m − 1) unit jobs with one job of length m have optimal makespan m.

theorem GrahamLPT.unitJobs_listSchedule_makespan (m : ℕ) [NeZero m] (σ : Fin (m * (m - 1) + 1) → Fin m) (hσ : IsListSchedule (unitJobs m) σ) : makespan (unitJobs m) σ = 2 * ↑m - 1

Every list schedule of the unit jobs followed by the job of length m has makespan 2m − 1.