Reference · Lemmas behind operations-research checks

rainbow.math.lemmas.cpm-makespan

Lemmas behind operations-research checks src/rainbow/math/lemmas/cpm_makespan.clj0 definitions, 9 theorems

General lemmas: cpm makespan. The mathematical facts the corresponding checks rest on, each checked by the kernel.

signed/at-most-negate

TheoremFor all inputsNo axiomsSource

signed/at-most-negate :
  (x y : ℚ)
  (h : x ≤ y)
  → signed/negate y ≤ signed/negate x

ℚ = signed/SignedRational≤ = signed/at-most

signed/cpm-rearrange-upper

TheoremFor all inputsNo axiomsSource

signed/cpm-rearrange-upper :
  (x y z : ℚ)
  (h : x + signed/negate (y + z) ≤ 0)
  → x + signed/negate y ≤ z

+ = signed/add0 = signed/zeroℚ = signed/SignedRational≤ = signed/at-most

signed/cpm-rearrange-lower

TheoremFor all inputsNo axiomsSource

signed/cpm-rearrange-lower :
  (x y z : ℚ)
  (h : y + z ≤ x)
  → z ≤ x + signed/negate y

+ = signed/addℚ = signed/SignedRational≤ = signed/at-most

signed/cpm-drop-nonpositive

TheoremFor all inputsNo axiomsSource

signed/cpm-drop-nonpositive :
  (a b c : ℚ)
  (h : a + signed/negate b ≤ c)
  (hb : b ≤ 0)
  → a ≤ c

+ = signed/add0 = signed/zeroℚ = signed/SignedRational≤ = signed/at-most

signed/cpm-drop-nonnegative

TheoremFor all inputsNo axiomsSource

signed/cpm-drop-nonnegative :
  (a b c : ℚ)
  (h : c ≤ a + signed/negate b)
  (hb : 0 ≤ b)
  → c ≤ a

+ = signed/add0 = signed/zeroℚ = signed/SignedRational≤ = signed/at-most

signed/expr-sum-value-negate

TheoremFor all inputsNo axiomsSource

signed/expr-sum-value-negate :
  (G : ℕ → ℚ) (n : ℕ)
  → signed/expr-sum-value (fun ng => signed/negate (G ng)) n = signed/negate (signed/expr-sum-value G n)

= = signed/equivalent: equality of rational valuesℕ = data/Natℚ = signed/SignedRational

signed/cpm-slack-expand

TheoremFor all inputsNo axiomsSource

signed/cpm-slack-expand :
  (a b g h : ℕ → ℚ) (n : ℕ)
  (ha1 : signed/expr-sum-value (fun sa => a sa) n = 1)
  (hb1 : signed/expr-sum-value (fun sb => b sb) n = 1)
  → signed/expr-sum-value (fun su => a su · signed/expr-sum-value (fun sv => b sv · (fun mu => fun mv => g mv + (signed/negate (g mu) + signed/negate (h mu))) su sv) n) n = signed/expr-sum-value (fun qu => b qu · g qu) n + signed/negate (signed/expr-sum-value (fun qu => a qu · g qu) n + signed/expr-sum-value (fun qu => a qu · h qu) n)

+ = signed/add1 = signed/one= = signed/equivalent: equality of rational values· = signed/multiplyℕ = data/Natℚ = signed/SignedRational

signed/cpm-schedule-step

TheoremFor all inputsNo axiomsSource

signed/cpm-schedule-step :
  (a b : ℕ → ℚ) (E : ℕ → ℕ → ℚ) (d S : ℕ → ℚ) (n : ℕ)
  (ha0 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ a idx)
  (hb0 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ b idx)
  (ha1 : signed/expr-sum-value (fun sa => a sa) n = 1)
  (hb1 : signed/expr-sum-value (fun sb => b sb) n = 1)
  (hE : ∀ (eu : ℕ), ∀ (eu-lt : nat/strict-below eu n), ∀ (ev : ℕ), ∀ (ev-lt : nat/strict-below ev n), E eu ev · (1 + signed/negate (E eu ev)) = 0)
  (hstep : signed/expr-sum-value (fun su => a su · signed/expr-sum-value (fun sv => b sv · E su sv) n) n = 1)
  (hprec : ∀ (su : ℕ), ∀ (su-lt : nat/strict-below su n), ∀ (sv : ℕ), ∀ (sv-lt : nat/strict-below sv n), ∀ (se : E su sv = 1), S su + d su ≤ S sv)
  → signed/expr-sum-value (fun qu => a qu · S qu) n + signed/expr-sum-value (fun qu => a qu · d qu) n ≤ signed/expr-sum-value (fun qu => b qu · S qu) n

+ = signed/add0 = signed/zero1 = signed/one= = signed/equivalent: equality of rational values· = signed/multiplyℕ = data/Natℚ = signed/SignedRational≤ = signed/at-most

signed/cpm-makespan-lower-bound

TheoremFor all inputsNo axiomsSource

signed/cpm-makespan-lower-bound :
  (P E : ℕ → ℕ → ℚ) (d ES S : ℕ → ℚ) (T C : ℚ) (n L : ℕ)
  (hP0 : ∀ (ht : ℕ), ∀ (ht-lt : nat/strict-below ht (data/succ L)), ∀ (hu : ℕ), ∀ (hu-lt : nat/strict-below hu n), 0 ≤ P ht hu)
  (hrow : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx (data/succ L)), signed/expr-sum-value (fun rw => P idx rw) n = 1)
  (hE : ∀ (eu : ℕ), ∀ (eu-lt : nat/strict-below eu n), ∀ (ev : ℕ), ∀ (ev-lt : nat/strict-below ev n), E eu ev · (1 + signed/negate (E eu ev)) = 0)
  (hstep : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx L), signed/expr-sum-value (fun su => (fun rw => P idx rw) su · signed/expr-sum-value (fun sv => (fun rw => P (data/succ idx) rw) sv · E su sv) n) n = 1)
  (htight : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx L), signed/expr-sum-value (fun su => (fun rw => P idx rw) su · signed/expr-sum-value (fun sv => (fun rw => P (data/succ idx) rw) sv · (fun mu => fun mv => ES mv + (…⟨1⟩ …⟨3⟩ + …⟨1⟩ …⟨3⟩)) su sv) n) n ≤ 0)
  (hstart : signed/expr-sum-value (fun qu => (fun rw => P 0 rw) qu · ES qu) n ≤ 0)
  (hend : T ≤ signed/expr-sum-value (fun qu => (fun rw => P L rw) qu · (fun fu => ES fu + d fu) qu) n)
  (hS0 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ S idx)
  (hprec : ∀ (su : ℕ), ∀ (su-lt : nat/strict-below su n), ∀ (sv : ℕ), ∀ (sv-lt : nat/strict-below sv n), ∀ (se : E su sv = 1), S su + d su ≤ S sv)
  (hfin : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), S idx + d idx ≤ C)
  → T ≤ C

+ = signed/add0 = signed/zero1 = signed/one= = signed/equivalent: equality of rational values· = signed/multiplyℕ = data/Natℚ = signed/SignedRational≤ = signed/at-most