Reference · Finite sums

rainbow.math.sums.wspt-order

Finite sumssrc/rainbow/math/sums/wspt_order.clj0 definitions, 5 theorems

WSPT order prerequisites. Strictly positive processing times are caller premises. This module alone does not prove schedule optimality or permutation semantics.

signed/multiply-positive-reflects-order :
  (ws-left ws-right ws-factor : ℚ)
  (ws-positive : 0 < ws-factor)
  (ws-scaled : ws-left · ws-factor ≤ ws-right · ws-factor)
  → ws-left ≤ ws-right

signed/wspt-cross-order-transitive :
  (ws-pa ws-wa ws-pb ws-wb ws-pc ws-wc : ℚ)
  (ws-hpa : 0 < ws-pa)
  (ws-hpb : 0 < ws-pb)
  (ws-hpc : 0 < ws-pc)
  (ws-ab : ws-wb · ws-pa ≤ ws-wa · ws-pb)
  (ws-bc : ws-wc · ws-pb ≤ ws-wb · ws-pc)
  → ws-wc · ws-pa ≤ ws-wa · ws-pc

signed/wspt-min-of-ordered :
  (ws-a ws-b : ℚ)
  (ws-ab : ws-a ≤ ws-b)
  → signed/min ws-a ws-b = ws-a

signed/wspt-adjacent-order-up-to :
  (ws-times ws-weights : ℕ → ℚ) (ws-last : ℕ)
  (ws-pos : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx (data/succ ws-last)), 0 < ws-times idx)
  (ws-adj : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx ws-last), ws-weights (data/succ idx) · ws-times idx ≤ ws-weights idx · ws-times (data/succ idx))
  (ws-first : ℕ)
  (ws-before : ws-first ≤ ws-last)
  → ws-weights ws-last · ws-times ws-first ≤ ws-weights ws-first · ws-times ws-last

signed/wspt-adjacent-implies-pairwise :
  (ws-times ws-weights : ℕ → ℚ) (ws-count-predecessor : ℕ)
  (ws-positive : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx (data/succ ws-count-predecessor)), 0 < ws-times idx)
  (ws-adjacency : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx ws-count-predecessor), ws-weights (data/succ idx) · ws-times idx ≤ ws-weights idx · ws-times (data/succ idx))
  (ws-i ws-j : ℕ)
  (ws-ij : ws-i ≤ ws-j)
  (ws-j-bound : nat/strict-below ws-j (data/succ ws-count-predecessor))
  → ws-weights ws-j · ws-times ws-i ≤ ws-weights ws-i · ws-times ws-j