LPTForm

Dósa's theorem for LPT schedules, the two-way statement, and the strict inequality for every job count other than 2m + 1.

theorem GrahamLPT.graham_of_lpt_eq_bound {m n : ℕ} [NeZero m] (hm : 2 ≤ m) (hn : 0 < n) (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 < p j) (σ : Fin n → Fin m) (hσ : IsLPTSchedule p σ) (heq : 3 * ↑m * makespan p σ = (4 * ↑m - 1) * optMakespan m p) : ∃ (a : ℝ) (e : Fin n ≃ Fin (2 * m + 1)), 0 < a ∧ ∀ (j : Fin n), p j = a * grahamJobs m (e j)

Dósa's theorem for LPT schedules: on m ≥ 2 machines, an LPT schedule of a nonempty positive instance attains Graham's bound against the optimum only when the instance is a positive multiple of Graham's 2m + 1 jobs in some order.

theorem GrahamLPT.lpt_eq_bound_iff_graham {m n : ℕ} [NeZero m] (hm : 2 ≤ m) (hn : 0 < n) (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 < p j) : (∃ (σ : Fin n → Fin m), IsLPTSchedule p σ ∧ 3 * ↑m * makespan p σ = (4 * ↑m - 1) * optMakespan m p) ↔ ∃ (a : ℝ) (e : Fin n ≃ Fin (2 * m + 1)), 0 < a ∧ ∀ (j : Fin n), p j = a * grahamJobs m (e j)

Graham's example is the only tight one (Dósa 2004): for a nonempty positive instance on m ≥ 2 machines, some LPT schedule attains Graham's bound 3m · C(σ) = (4m − 1) · optMakespan if and only if the instance is a positive multiple of Graham's 2m + 1 jobs in some order (and then every LPT schedule attains it, lpt_eq_bound_of_graham).

theorem GrahamLPT.lpt_lt_bound_of_card_ne {m n : ℕ} [NeZero m] (hm : 2 ≤ m) (hn : 0 < n) (hn' : n ≠ 2 * m + 1) (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 < p j) (σ : Fin n → Fin m) (hσ : IsLPTSchedule p σ) : 3 * ↑m * makespan p σ < (4 * ↑m - 1) * optMakespan m p

With any number of jobs other than 2m + 1, no LPT schedule of a nonempty positive instance on m ≥ 2 machines attains Graham's bound: the inequality is strict.