Key

The key lemma by counting, and the optimality of LPT when every job exceeds a third of the optimum.

theorem GrahamLPT.key_card_mul_le_sum {n : ℕ} (p : Fin n → ℝ) (hanti : Antitone p) (k : Fin n) (U : Finset (Fin n)) (hU : ∀ j ∈ U, ↑j < ↑k + 1) : ↑U.card * p k ≤ ∑ j ∈ U, p j

Jobs of index at most k are at least p k long, so a set of them sums to at least its size times p k.

theorem GrahamLPT.key_lemma {m n : ℕ} (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 ≤ p j) (hanti : Antitone p) (σ : Fin n → Fin m) (hσ : IsListSchedule p σ) (k : Fin n) (τ : Fin n → Fin m) (T : ℝ) (hT : ∀ (i : Fin m), loadBefore p τ (↑k + 1) i ≤ T) (h3 : T < 3 * p k) : loadBefore p σ (↑k) (σ k) + p k ≤ T

The counting lemma: p nonincreasing and nonnegative, σ a list schedule, τ any assignment whose loads from the jobs of index ≤ k are at most T, and T < 3 p_k: then the machine of k ends by T.

theorem GrahamLPT.key_optimal_sorted {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 ≤ p j) (hanti : Antitone p) (σ : Fin n → Fin m) (hσ : IsListSchedule p σ) (τ : Fin n → Fin m) (h : ∀ (j : Fin n), makespan p τ < 3 * p j) : makespan p σ ≤ makespan p τ

The sorted form of lpt_optimal_of_third_lt.

theorem GrahamLPT.lpt_optimal_of_third_lt {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 ≤ p j) (σ : Fin n → Fin m) (hσ : IsLPTSchedule p σ) (τ : Fin n → Fin m) (h : ∀ (j : Fin n), makespan p τ < 3 * p j) : makespan p σ ≤ makespan p τ

When every job is longer than a third of the makespan of τ, every LPT schedule is at least as good as τ.

theorem GrahamLPT.lpt_eq_optMakespan_of_third_lt {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 ≤ p j) (σ : Fin n → Fin m) (hσ : IsLPTSchedule p σ) (h : ∀ (j : Fin n), optMakespan m p < 3 * p j) : makespan p σ = optMakespan m p

LPT is optimal when every job is longer than a third of the optimal makespan.