LPTBound

Graham's 1969 bound for LPT.

theorem GrahamLPT.lb2_bound_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) : 3 * ↑m * makespan p σ ≤ (4 * ↑m - 1) * makespan p τ

The sorted form of lpt_bound.

theorem GrahamLPT.lpt_bound {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) : 3 * ↑m * makespan p σ ≤ (4 * ↑m - 1) * makespan p τ

Graham's bound for LPT: for nonnegative lengths, every LPT schedule σ and every assignment τ satisfy 3m · C(σ) ≤ (4m − 1) · C(τ).

theorem GrahamLPT.lpt_le_optMakespan {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 ≤ p j) (σ : Fin n → Fin m) (hσ : IsLPTSchedule p σ) : makespan p σ ≤ (4 / 3 - 1 / (3 * ↑m)) * optMakespan m p

Every LPT schedule is within the factor 4/3 − 1/(3m) of the optimum.