ListOptimum

Graham's ω₀ is the optimum: for nonnegative lengths every assignment τ is matched or improved by a list schedule (helpers carry the prefix lo_). The order is the start times of τ with each machine's jobs run back to back in index order, s j = loadBefore p τ j (τ j). In that order every list schedule starts each job of positive length no later than τ does (lo_core): if job k found every machine busy past s k, each machine would carry an earlier job running at time s k; those m jobs run at s k under τ too, on m distinct machines of τ, one of them τ k, which overlaps k. Hence every list-schedule load is at most max_j (s j + p j) ≤ makespan p τ.

theorem GrahamLPT.lo_exists_cover {m n : ℕ} (q : Fin n → ℝ) (σ : Fin n → Fin m) (T : ℝ) (hT : 0 ≤ T) (i : Fin m) (k : ℕ) : T < loadBefore q σ k i → ∃ (a : Fin n), ↑a < k ∧ σ a = i ∧ loadBefore q σ (↑a) i ≤ T ∧ T < loadBefore q σ (↑a) i + q a

A machine whose load before k exceeds T ≥ 0 carries a job before k that is running at time T.

theorem GrahamLPT.lo_core {m n : ℕ} (q : Fin n → ℝ) (σ : Fin n → Fin m) (hσ : IsListSchedule q σ) (ρ : Fin n → Fin m) (t : Fin n → ℝ) (ht : Monotone t) (ht0 : ∀ (j : Fin n), 0 ≤ t j) (hdisj : ∀ (a b : Fin n), a ≠ b → ρ a = ρ b → t a + q a ≤ t b ∨ t b + q b ≤ t a) (N : ℕ) (k : Fin n) : ↑k < N → 0 < q k → loadBefore q σ (↑k) (σ k) ≤ t k

In an order by nondecreasing times t that are the start times of a schedule ρ (no two jobs of one machine of ρ overlap), every list schedule starts each job of positive length no later than ρ does.

theorem GrahamLPT.lo_makespan_le {m n : ℕ} [NeZero m] (q : Fin n → ℝ) (hq : ∀ (j : Fin n), 0 ≤ q j) (σ : Fin n → Fin m) (hσ : IsListSchedule q σ) (ρ : Fin n → Fin m) (t : Fin n → ℝ) (ht : Monotone t) (ht0 : ∀ (j : Fin n), 0 ≤ t j) (hdisj : ∀ (a b : Fin n), a ≠ b → ρ a = ρ b → t a + q a ≤ t b ∨ t b + q b ≤ t a) (C : ℝ) (hC0 : 0 ≤ C) (hC : ∀ (j : Fin n), t j + q j ≤ C) : makespan q σ ≤ C

Every list schedule in such an order has makespan at most any bound C ≥ 0 on the completion times t j + q j.

theorem GrahamLPT.exists_listSchedule_le {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 ≤ p j) (τ : Fin n → Fin m) : ∃ (π : Equiv.Perm (Fin n)) (σ : Fin n → Fin m), IsListSchedule (p ∘ ⇑π) (σ ∘ ⇑π) ∧ makespan p σ ≤ makespan p τ

Graham's ω₀ is attained: for nonnegative lengths every assignment τ is matched or improved by a list schedule in some order (the jobs listed by their start times when each machine of τ runs its jobs in index order).

theorem GrahamLPT.isLeast_listSchedule_makespan {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 ≤ p j) : IsLeast ((fun (σ : Fin n → Fin m) => makespan p σ) '' {σ : Fin n → Fin m | ∃ (π : Equiv.Perm (Fin n)), IsListSchedule (p ∘ ⇑π) (σ ∘ ⇑π)}) (optMakespan m p)

The optimal makespan is the least makespan over the list schedules in all orders (Graham's ω₀ equals optMakespan).