GrahamScaled

Scaling and relabeling of instances, and the sufficiency half of Dósa's theorem: every positive multiple of Graham's instance in any order attains the bound. Helpers carry the prefix gs_.

theorem GrahamLPT.gs_loadBefore_smul {m n : ℕ} (p : Fin n → ℝ) (a : ℝ) (σ : Fin n → Fin m) (k : ℕ) (i : Fin m) : loadBefore (fun (j : Fin n) => a * p j) σ k i = a * loadBefore p σ k i

Scaling the lengths by a ≥ 0 scales the loads before k.

theorem GrahamLPT.gs_load_smul {m n : ℕ} (p : Fin n → ℝ) (a : ℝ) (σ : Fin n → Fin m) (i : Fin m) : load (fun (j : Fin n) => a * p j) σ i = a * load p σ i

Scaling the lengths by a scales every load.

theorem GrahamLPT.gs_makespan_smul {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (a : ℝ) (ha : 0 ≤ a) (σ : Fin n → Fin m) : makespan (fun (j : Fin n) => a * p j) σ = a * makespan p σ

Scaling the lengths by a ≥ 0 scales the makespan.

theorem GrahamLPT.gs_optMakespan_smul {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (a : ℝ) (ha : 0 ≤ a) : (optMakespan m fun (j : Fin n) => a * p j) = a * optMakespan m p

Scaling the lengths by a ≥ 0 scales the optimal makespan.

theorem GrahamLPT.gs_isListSchedule_smul_iff {m n : ℕ} (p : Fin n → ℝ) (a : ℝ) (ha : 0 < a) (σ : Fin n → Fin m) : IsListSchedule (fun (j : Fin n) => a * p j) σ ↔ IsListSchedule p σ

A list schedule of p is a list schedule of a · p for a > 0, and conversely.

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

Relabeling the jobs by a permutation preserves the optimal makespan.

theorem GrahamLPT.lpt_eq_bound_of_graham {m n : ℕ} [NeZero m] (p : Fin n → ℝ) (a : ℝ) (ha : 0 < a) (e : Fin n ≃ Fin (2 * m + 1)) (he : ∀ (j : Fin n), p j = a * grahamJobs m (e j)) (σ : Fin n → Fin m) (hσ : IsLPTSchedule p σ) : 3 * ↑m * makespan p σ = (4 * ↑m - 1) * optMakespan m p

Every positive multiple of Graham's instance, in any order, attains the bound: every LPT schedule σ satisfies 3m · C(σ) = (4m − 1) · optMakespan.