Reference · Lemmas behind operations-research checks

rainbow.math.lemmas.economic-dispatch

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

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

signed/nonneg-minus-nonpositive

TheoremFor all inputsNo axiomsSource

signed/nonneg-minus-nonpositive :
  (y x : ℚ)
  (hy : 0 ≤ y)
  (hx : x ≤ 0)
  → 0 ≤ y + signed/negate x

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

signed/dispatch-square-shift

TheoremFor all inputsNo axiomsSource

signed/dispatch-square-shift :
  (c p q : ℚ)
  → c · ((q + signed/negate p) · (q + signed/negate p)) + (c + c) · p · (q + signed/negate p) = c · (q · q) + signed/negate (c · (p · p))

+ = signed/add= = signed/equivalent: equality of rational values· = signed/multiplyℚ = signed/SignedRational

signed/dispatch-assemble

TheoremFor all inputsNo axiomsSource

signed/dispatch-assemble :
  (bp cpp bd xd mpd mmd sq cqq bq : ℚ)
  (h1 : bp + bd = bq)
  (h2 : sq + xd = cqq + signed/negate cpp)
  → bp + cpp + (bd + xd + mpd + signed/negate mmd) + (sq + (signed/negate mpd + mmd)) = bq + cqq

+ = signed/add= = signed/equivalent: equality of rational valuesℚ = signed/SignedRational

signed/dispatch-term-bound

TheoremFor all inputsNo axiomsSource

signed/dispatch-term-bound :
  (b c p q l mp mm lo hi : ℚ)
  (hc : 0 ≤ c)
  (hmp : 0 ≤ mp)
  (hmm : 0 ≤ mm)
  (hstat : b + signed/from-nnrat 2 · c · p + mp + signed/negate mm = l)
  (hup : mp · (hi + signed/negate p) ≤ 0)
  (hlow : mm · (p + signed/negate lo) ≤ 0)
  (hloq : lo ≤ q)
  (hqhi : q ≤ hi)
  → b · p + c · (p · p) + l · (q + signed/negate p) ≤ b · q + c · (q · q)

+ = signed/add0 = signed/zero= = signed/equivalent: equality of rational values· = signed/multiplyℚ = signed/SignedRational≤ = signed/at-most

signed/dispatch-cost-optimal

TheoremFor all inputsNo axiomsSource

signed/dispatch-cost-optimal :
  (b c p q mp mm lo hi : ℕ → ℚ) (l D : ℚ) (n : ℕ)
  (hc : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ c idx)
  (hmp : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ mp idx)
  (hmm : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ mm idx)
  (hpD : signed/expr-sum-value (fun ts => p ts) n = D)
  (hstat : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), b idx + signed/from-nnrat 2 · c idx · p idx + mp idx + signed/negate (mm idx) = l)
  (hup : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), mp idx · (hi idx + signed/negate (p idx)) ≤ 0)
  (hlow : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), mm idx · (p idx + signed/negate (lo idx)) ≤ 0)
  (hqD : signed/expr-sum-value (fun ts => q ts) n = D)
  (hloq : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), lo idx ≤ q idx)
  (hqhi : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), q idx ≤ hi idx)
  → signed/expr-sum-value (fun tc => b tc · p tc + c tc · (p tc · p tc)) n ≤ signed/expr-sum-value (fun tc => b tc · q tc + c tc · (q tc · q tc)) n

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