Documentation

LeanPool.GrahamLPT.FixedCount

FixedCount #

The supremum of the LPT ratio for a fixed number n ≥ 2m + 1 of jobs: Graham's jobs followed by small jobs. Helpers carry the prefix fc_.

source
noncomputable def GrahamLPT.paddedJobLength (m : ℕ) (ε : ℝ) (j : ℕ) :
ℝ

The lengths by index: Graham's 2m + 1 jobs (2m − 1, 2m − 1, …, m, m, m), then ε.

Equations
Instances For
    source
    noncomputable def GrahamLPT.paddedJobs (m n : ℕ) (ε : ℝ) :
    Fin n → ℝ

    Graham's 2m + 1 jobs followed by n − 2m − 1 jobs of length ε.

    Equations
    Instances For
      source
      theorem GrahamLPT.paddedJobLength_eq_grahamJobs (m : ℕ) (ε : ℝ) (j : Fin (2 * m + 1)) :
      paddedJobLength m ε ↑j = grahamJobs m j

      The unpadded jobs agree with Graham's original instance.

      source
      theorem GrahamLPT.paddedJobs_restrict (m n : ℕ) (ε : ℝ) (hn : 2 * m + 1 ≤ n) :
      paddedJobs m n ε ∘ Fin.castLE hn = grahamJobs m

      Restriction to the original job count removes the small-job tail.

      source
      theorem GrahamLPT.fc_len_lt (m : ℕ) (ε : ℝ) (j : ℕ) (h : j < 2 * m) :
      paddedJobLength m ε j = 2 * ↑m - 1 - ↑(j / 2)
      source
      theorem GrahamLPT.fc_len_two_mul (m : ℕ) (ε : ℝ) :
      paddedJobLength m ε (2 * m) = ↑m
      source
      theorem GrahamLPT.fc_len_gt (m : ℕ) (ε : ℝ) (j : ℕ) (h : 2 * m < j) :
      paddedJobLength m ε j = ε
      source
      theorem GrahamLPT.fc_le_len (m : ℕ) (ε : ℝ) (j : ℕ) (h : j ≤ 2 * m) :
      ↑m ≤ paddedJobLength m ε j

      Each of Graham's jobs is at least m.

      source
      theorem GrahamLPT.fc_len_pos (m : ℕ) (ε : ℝ) (hm : 0 < m) (hε : 0 < ε) (j : ℕ) :
      0 < paddedJobLength m ε j
      source
      theorem GrahamLPT.fc_jobs_pos (m n : ℕ) (ε : ℝ) (hm : 0 < m) (hε : 0 < ε) (j : Fin n) :
      0 < paddedJobs m n ε j
      source
      theorem GrahamLPT.fc_antitone (m n : ℕ) (ε : ℝ) (hε : ε ≤ ↑m) :
      Antitone (paddedJobs m n ε)

      For ε ≤ m the family is listed in nonincreasing order.

      source
      theorem GrahamLPT.fc_pair (m : ℕ) (ε : ℝ) (j : ℕ) (h : j < 2 * m) :
      paddedJobLength m ε j + paddedJobLength m ε (2 * m - 1 - j) = 3 * ↑m - 1

      The pairs j, 2m − 1 − j among the original jobs sum to 3m − 1.

      source
      theorem GrahamLPT.fc_pair' (m : ℕ) (ε : ℝ) (j : ℕ) (h : j < 2 * m - 2) :
      paddedJobLength m ε j + paddedJobLength m ε (2 * m - 3 - j) = 3 * ↑m

      The optimal pairs j, 2m − 3 − j among the original jobs sum to 3m.

      source
      theorem GrahamLPT.fc_sum_lt (m n : ℕ) (ε : ℝ) (hn : 2 * m ≤ n) :
      ∑ j : Fin n with ↑j < 2 * m, paddedJobs m n ε j = 3 * ↑m ^ 2 - ↑m

      The first 2m jobs sum to 3m² − m.

      source
      theorem GrahamLPT.fc_exists_prefix_pairing (m n : ℕ) [NeZero m] (ε : ℝ) (hn : 2 * m ≤ n) :
      ∃ (τ : Fin n → Fin m), ∀ (i : Fin m), loadBefore (paddedJobs m n ε) τ (2 * m) i = 3 * ↑m - 1

      The pairing j ↦ min (j, 2m − 1 − j) of the first 2m jobs has every load 3m − 1 before index 2m.

      source
      theorem GrahamLPT.fc_loadBefore_two_mul (m n : ℕ) [NeZero m] (ε : ℝ) (hn : 2 * m + 1 ≤ n) (σ : Fin n → Fin m) (hσ : IsListSchedule (paddedJobs m n ε) σ) (i : Fin m) :
      loadBefore (paddedJobs m n ε) σ (2 * m) i = 3 * ↑m - 1

      The original prefix loads are unaffected by the lengths of later jobs.

      source
      theorem GrahamLPT.fc_le_makespan_listSchedule (m n : ℕ) [NeZero m] (ε : ℝ) (hε0 : 0 < ε) (hn : 2 * m + 1 ≤ n) (σ : Fin n → Fin m) (hσ : IsListSchedule (paddedJobs m n ε) σ) :
      4 * ↑m - 1 ≤ makespan (paddedJobs m n ε) σ

      Every list schedule of the family in its own order has makespan at least 4m − 1: the job 2m, of length m, lands on a machine of load 3m − 1.

      source
      theorem GrahamLPT.fc_comp_eq (m n : ℕ) (ε : ℝ) (hε1 : ε ≤ ↑m) (π : Equiv.Perm (Fin n)) (h : Antitone (paddedJobs m n ε ∘ ⇑π)) :
      paddedJobs m n ε ∘ ⇑π = paddedJobs m n ε

      An antitone relabeling of the family leaves the lengths unchanged (Tuple.unique_antitone).

      source
      theorem GrahamLPT.fc_le_makespan_lpt (m n : ℕ) [NeZero m] (ε : ℝ) (hε0 : 0 < ε) (hε1 : ε ≤ ↑m) (hn : 2 * m + 1 ≤ n) (σ : Fin n → Fin m) (hσ : IsLPTSchedule (paddedJobs m n ε) σ) :
      4 * ↑m - 1 ≤ makespan (paddedJobs m n ε) σ

      Every LPT schedule of the family has makespan at least 4m − 1.

      source
      theorem GrahamLPT.fc_exists_opt (m n : ℕ) [NeZero m] (ε : ℝ) (hε0 : 0 ≤ ε) (hn : 2 * m + 1 ≤ n) :
      ∃ (τ : Fin n → Fin m), ∀ (i : Fin m), load (paddedJobs m n ε) τ i ≤ 3 * ↑m + ↑n * ε

      Extend an optimal assignment of the original jobs by assigning the small-job tail to machine zero; each load is at most 3m + nε.

      source
      theorem GrahamLPT.fc_optMakespan_le (m n : ℕ) [NeZero m] (ε : ℝ) (hε0 : 0 ≤ ε) (hn : 2 * m + 1 ≤ n) :
      optMakespan m (paddedJobs m n ε) ≤ 3 * ↑m + ↑n * ε

      The optimum of the family is at most 3m + nε.

      source
      theorem GrahamLPT.fc_optMakespan_pos {m n : ℕ} [NeZero m] (hn : 0 < n) (p : Fin n → ℝ) (hp : ∀ (j : Fin n), 0 < p j) :
      0 < optMakespan m p

      A positive instance with a job has a positive optimum.

      source
      theorem GrahamLPT.isLUB_lpt_ratio_of_card {m n : ℕ} [NeZero m] (hn : 2 * m + 1 ≤ n) :
      IsLUB {r : ℝ | ∃ (p : Fin n → ℝ) (σ : Fin n → Fin m), (∀ (j : Fin n), 0 < p j) ∧ IsLPTSchedule p σ ∧ r = makespan p σ / optMakespan m p} (4 / 3 - 1 / (3 * ↑m))

      For every fixed number n ≥ 2m + 1 of jobs, Graham's constant 4/3 − 1/(3m) is still the supremum of C(σ)/optMakespan over the LPT schedules of the positive instances with n jobs (for m ≥ 2 it is attained only at n = 2m + 1, lpt_lt_bound_of_card_ne).