Documentation

LeanPool.GrahamLPT.Ratio

Ratio #

The least constants, 2 − 1/m and 4/3 − 1/(3m).

theorem GrahamLPT.isLeast_listSchedule_ratio (m : ℕ) [NeZero m] :
IsLeast {c : ℝ | ∀ (n : ℕ) (p : Fin n → ℝ) (σ τ : Fin n → Fin m), (∀ (j : Fin n), 0 ≤ p j) → IsListSchedule p σ → makespan p σ ≤ c * makespan p τ} (2 - 1 / ↑m)

2 − 1/m is the least constant c with C(σ) ≤ c · C(τ) for every list schedule σ of every nonnegative instance on m machines and every assignment τ.

theorem GrahamLPT.isLeast_lpt_ratio (m : ℕ) [NeZero m] :
IsLeast {c : ℝ | ∀ (n : ℕ) (p : Fin n → ℝ) (σ τ : Fin n → Fin m), (∀ (j : Fin n), 0 ≤ p j) → IsLPTSchedule p σ → makespan p σ ≤ c * makespan p τ} (4 / 3 - 1 / (3 * ↑m))

4/3 − 1/(3m) is the least constant c with C(σ) ≤ c · C(τ) for every LPT schedule σ of every nonnegative instance on m machines and every assignment τ.