Reference · Lemmas behind operations-research checks

rainbow.math.lemmas.assign-dual

Lemmas behind operations-research checkssrc/rainbow/math/lemmas/assign_dual.clj0 definitions, 4 theorems

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

signed/double-sum-row-weights :
  (w : ℕ → ℚ) (X : ℕ → ℕ → ℚ) (n : ℕ)
  (hrows : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), signed/expr-sum-value (fun rj => X idx rj) n = 1)
  → signed/expr-sum-value (fun i => signed/expr-sum-value (fun column-index => (fun wr => fun wc => w wr · X wr wc) i column-index) n) n = signed/expr-sum-value (fun wi => w wi) n

signed/double-sum-col-weights :
  (w : ℕ → ℚ) (X : ℕ → ℕ → ℚ) (n : ℕ)
  (hcols : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), signed/expr-sum-value (fun ci => X ci idx) n = 1)
  → signed/expr-sum-value (fun i => signed/expr-sum-value (fun column-index => (fun wr => fun wc => w wc · X wr wc) i column-index) n) n = signed/expr-sum-value (fun wi => w wi) n

signed/double-sum-add :
  (X Y : ℕ → ℕ → ℚ) (n : ℕ)
  → signed/expr-sum-value (fun i => signed/expr-sum-value (fun column-index => (fun pr => fun pc => X pr pc + Y pr pc) i column-index) n) n = signed/expr-sum-value (fun i => signed/expr-sum-value (fun column-index => X i column-index) n) n + signed/expr-sum-value (fun i => signed/expr-sum-value (fun column-index => Y i column-index) n) n

signed/assignment-weak-duality :
  (c : ℕ → ℕ → ℚ) (u v : ℕ → ℚ) (X : ℕ → ℕ → ℚ) (n : ℕ)
  (hdual : ∀ (ai : ℕ), ∀ (ai-bound : nat/strict-below ai n), ∀ (aj : ℕ), ∀ (aj-bound : nat/strict-below aj n), u ai + v aj ≤ c ai aj)
  (x0 : ∀ (ai : ℕ), ∀ (ai-bound : nat/strict-below ai n), ∀ (aj : ℕ), ∀ (aj-bound : nat/strict-below aj n), 0 ≤ X ai aj)
  (hrows : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), signed/expr-sum-value (fun rj => X idx rj) n = 1)
  (hcols : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), signed/expr-sum-value (fun ci => X ci idx) n = 1)
  → signed/expr-sum-value (fun wi => u wi) n + signed/expr-sum-value (fun wi => v wi) n ≤ signed/expr-sum-value (fun i => signed/expr-sum-value (fun column-index => (fun ki => fun kj => c ki kj · X ki kj) i column-index) n) n