Basic

Loads, makespans, the existence of list and LPT schedules, the attained optimum, relabeling.

theorem GrahamLPT.sum_prefix_succ {M : Type u_1} [AddCommMonoid M] {m n : ℕ} (f : Fin n → M) (σ : Fin n → Fin m) (k : Fin n) (i : Fin m) : ∑ j : Fin n with ↑j < ↑k + 1 ∧ σ j = i, f j = ∑ j : Fin n with ↑j < ↑k ∧ σ j = i, f j + if σ k = i then f k else 0

Adding one job to a prefix sum, for arbitrary commutative additive values.

theorem GrahamLPT.sum_prefix_fiber {M : Type u_1} [AddCommMonoid M] {m n : ℕ} (f : Fin n → M) (σ : Fin n → Fin m) (k : ℕ) : ∑ i : Fin m, ∑ j : Fin n with ↑j < k ∧ σ j = i, f j = ∑ j : Fin n with ↑j < k, f j

Summing the machine fibers recovers the total prefix weight.

theorem GrahamLPT.bs_loadBefore_zero {m n : ℕ} (p : Fin n → ℝ) (σ : Fin n → Fin m) (i : Fin m) : loadBefore p σ 0 i = 0

No job has index below 0.

theorem GrahamLPT.bs_loadBefore_succ {m n : ℕ} (p : Fin n → ℝ) (σ : Fin n → Fin m) (k : Fin n) (i : Fin m) : loadBefore p σ (↑k + 1) i = loadBefore p σ (↑k) i + if σ k = i then p k else 0

Adding the job k.

theorem GrahamLPT.bs_loadBefore_of_le {m n : ℕ} (p : Fin n → ℝ) (σ : Fin n → Fin m) (k : ℕ) (hk : n ≤ k) (i : Fin m) : loadBefore p σ k i = load p σ i

At or beyond the last index, loadBefore is the load.

theorem GrahamLPT.load_le_loadBefore_add {m n : ℕ} (p : Fin n → ℝ) (σ : Fin n → Fin m) (k : ℕ) (ε : ℝ) (hε : 0 ≤ ε) (htail : ∀ (j : Fin n), k ≤ ↑j → p j ≤ ε) (i : Fin m) : load p σ i ≤ loadBefore p σ k i + ↑n * ε

If every later job has length at most ε ≥ 0, a full load exceeds its prefix by at most nε.

theorem GrahamLPT.loadBefore_restrict {m n N : ℕ} (h : n ≤ N) (p : Fin N → ℝ) (σ : Fin N → Fin m) (k : ℕ) (hk : k ≤ n) (i : Fin m) : loadBefore (p ∘ Fin.castLE h) (σ ∘ Fin.castLE h) k i = loadBefore p σ k i

Restricting a job vector and assignment preserves every load in the retained prefix.

theorem GrahamLPT.IsListSchedule.restrict {m n N : ℕ} (h : n ≤ N) (p : Fin N → ℝ) (σ : Fin N → Fin m) (hσ : IsListSchedule p σ) : IsListSchedule (p ∘ Fin.castLE h) (σ ∘ Fin.castLE h)

A list schedule restricts to a list schedule of any initial segment of the jobs.

theorem GrahamLPT.bs_sum_loadBefore {m n : ℕ} (p : Fin n → ℝ) (σ : Fin n → Fin m) (k : ℕ) : ∑ i : Fin m, loadBefore p σ k i = ∑ j : Fin n with ↑j < k, p j

The loads before k sum to the lengths of the jobs before k.

theorem GrahamLPT.bs_sum_load {m n : ℕ} (p : Fin n → ℝ) (σ : Fin n → Fin m) : ∑ i : Fin m, load p σ i = ∑ j : Fin n, p j

The loads sum to the total length.

theorem GrahamLPT.bs_sum_filter_add_le {n : ℕ} (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 ≤ p j) (k : Fin n) : ∑ j : Fin n with ↑j < ↑k, p j + p k ≤ ∑ j : Fin n, p j

The lengths of the jobs before k, plus p k, are at most the total (nonnegative lengths).

theorem GrahamLPT.bs_loadBefore_mono {m n : ℕ} (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 ≤ p j) (σ : Fin n → Fin m) {k k' : ℕ} (h : k ≤ k') (i : Fin m) : loadBefore p σ k i ≤ loadBefore p σ k' i

theorem GrahamLPT.bs_loadBefore_le_load {m n : ℕ} (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 ≤ p j) (σ : Fin n → Fin m) (k : ℕ) (i : Fin m) : loadBefore p σ k i ≤ load p σ i

theorem GrahamLPT.bs_load_eq_zero {m n : ℕ} (p : Fin n → ℝ) (σ : Fin n → Fin m) (i : Fin m) (h : ∀ (j : Fin n), σ j ≠ i) : load p σ i = 0

The load of a machine with no job is 0.

theorem GrahamLPT.bs_exists_last_job_before {m n : ℕ} (p : Fin n → ℝ) (σ : Fin n → Fin m) (c : ℕ) (i : Fin m) (h : ∃ (j : Fin n), ↑j < c ∧ σ j = i) : ∃ (k : Fin n), ↑k < c ∧ σ k = i ∧ loadBefore p σ c i = loadBefore p σ (↑k) i + p k

With a cutoff c: a machine with a job of index below c has a last such job.

theorem GrahamLPT.bs_exists_last_job {m n : ℕ} (p : Fin n → ℝ) (σ : Fin n → Fin m) (i : Fin m) (h : ∃ (j : Fin n), σ j = i) : ∃ (k : Fin n), σ k = i ∧ load p σ i = loadBefore p σ (↑k) i + p k

A machine with a job has a last job k, and its load is the load before k plus p k.

theorem GrahamLPT.bs_loadBefore_eq_zero {m n : ℕ} (p : Fin n → ℝ) (σ : Fin n → Fin m) (c : ℕ) (i : Fin m) (h : ∀ (j : Fin n), ↑j < c → σ j ≠ i) : loadBefore p σ c i = 0

A machine with no job of index below c has load 0 before c.

theorem GrahamLPT.bs_mul_loadBefore_le {m n : ℕ} (p : Fin n → ℝ) (σ : Fin n → Fin m) (hσ : IsListSchedule p σ) (k : Fin n) : ↑m * loadBefore p σ (↑k) (σ k) ≤ ∑ j : Fin n with ↑j < ↑k, p j

In a list schedule, m times the least load before k is at most the total length of the jobs before k.

theorem GrahamLPT.bs_makespan_le_iff {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (σ : Fin n → Fin m) (c : ℝ) : makespan p σ ≤ c ↔ ∀ (i : Fin m), load p σ i ≤ c

theorem GrahamLPT.bs_exists_load_eq_makespan {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (σ : Fin n → Fin m) : ∃ (i : Fin m), load p σ i = makespan p σ

theorem GrahamLPT.load_le_makespan {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (σ : Fin n → Fin m) (i : Fin m) : load p σ i ≤ makespan p σ

Every machine load is at most the makespan.

theorem GrahamLPT.bs_makespan_nonneg {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 ≤ p j) (σ : Fin n → Fin m) : 0 ≤ makespan p σ

theorem GrahamLPT.bs_load_comp {m n : ℕ} (p : Fin n → ℝ) (σ : Fin n → Fin m) (π : Equiv.Perm (Fin n)) (i : Fin m) : load (p ∘ ⇑π) (σ ∘ ⇑π) i = load p σ i

Relabeling the jobs by a permutation changes no load.

theorem GrahamLPT.sum_le_mul_makespan {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (σ : Fin n → Fin m) : ∑ j : Fin n, p j ≤ ↑m * makespan p σ

The total length is at most m times the makespan.

theorem GrahamLPT.exists_makespan_eq_optMakespan {m n : ℕ} [NeZero m] (p : Fin n → ℝ) : ∃ (τ : Fin n → Fin m), makespan p τ = optMakespan m p

The optimal makespan is attained.

noncomputable def GrahamLPT.leastLoadedMachine {m : ℕ} [NeZero m] (L : Fin m → ℝ) : Fin m

A least-loaded machine of a load vector (the greedy choice).

Equations

• GrahamLPT.leastLoadedMachine L = Classical.choose ⋯

theorem GrahamLPT.bs_argmin_le {m : ℕ} [NeZero m] (L : Fin m → ℝ) (i : Fin m) : L (leastLoadedMachine L) ≤ L i

noncomputable def GrahamLPT.greedyLoads {m n : ℕ} [NeZero m] (p : Fin n → ℝ) : ℕ → Fin m → ℝ

The greedy loads after the first k jobs.

Equations

• GrahamLPT.greedyLoads p 0 = fun (x : Fin m) => 0
• GrahamLPT.greedyLoads p k.succ = fun (i : Fin m) => GrahamLPT.greedyLoads p k i + if i = GrahamLPT.leastLoadedMachine (GrahamLPT.greedyLoads p k) then if h : k < n then p ⟨k, h⟩ else 0 else 0

theorem GrahamLPT.bs_loadBefore_greedy {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (k : ℕ) : k ≤ n → ∀ (i : Fin m), loadBefore p (fun (j : Fin n) => leastLoadedMachine (greedyLoads p ↑j)) k i = greedyLoads p k i

theorem GrahamLPT.exists_isListSchedule {m n : ℕ} [NeZero m] (p : Fin n → ℝ) : ∃ (σ : Fin n → Fin m), IsListSchedule p σ

A list schedule exists.

theorem GrahamLPT.exists_isLPTSchedule {m n : ℕ} [NeZero m] (p : Fin n → ℝ) : ∃ (σ : Fin n → Fin m), IsLPTSchedule p σ

An LPT schedule exists.

theorem GrahamLPT.optMakespan_le {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (τ : Fin n → Fin m) : optMakespan m p ≤ makespan p τ

The optimal makespan is at most the makespan of every assignment.

theorem GrahamLPT.le_makespan_of_nonneg {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 ≤ p j) (σ : Fin n → Fin m) (j : Fin n) : p j ≤ makespan p σ

For nonnegative lengths every job is at most the makespan.

theorem GrahamLPT.makespan_comp {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (σ : Fin n → Fin m) (π : Equiv.Perm (Fin n)) : makespan (p ∘ ⇑π) (σ ∘ ⇑π) = makespan p σ

Relabeling the jobs by a permutation does not change the makespan.