Reference · Lemmas behind operations-research checks

rainbow.math.lemmas.ufl-gap

Lemmas behind operations-research checkssrc/rainbow/math/lemmas/ufl_gap.clj0 definitions, 5 theorems

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

signed/positive-part-upper :
  (t : ℚ)
  → t ≤ data/Bool.rec (fun x₄ => ℚ) 0 t (signed/decide-at-most 0 t)

signed/positive-part-nonneg :
  (t : ℚ)
  → 0 ≤ data/Bool.rec (fun x₄ => ℚ) 0 t (signed/decide-at-most 0 t)

signed/rect-double-sum-row-weights :
  (w : ℕ → ℚ) (X : ℕ → ℕ → ℚ) (m n : ℕ)
  (hrows : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx m), 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) m = signed/expr-sum-value (fun wi => w wi) m

signed/rect-double-sum-add :
  (X Y : ℕ → ℕ → ℚ) (m 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) m = signed/expr-sum-value (fun i => signed/expr-sum-value (fun column-index => X i column-index) n) m + signed/expr-sum-value (fun i => signed/expr-sum-value (fun column-index => Y i column-index) n) m

signed/ufl-weak-duality :
  (f : ℕ → ℚ) (c : ℕ → ℕ → ℚ) (v Y : ℕ → ℚ) (X : ℕ → ℕ → ℚ) (m n : ℕ)
  (hdual : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), signed/expr-sum-value (fun ui => data/Bool.rec (fun x₂ => ℚ) 0 (v ui + signed/negate (c ui idx)) (signed/decide-at-most 0 (v ui + signed/negate (c ui idx)))) m ≤ f idx)
  (y0 : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ Y idx)
  (x0 : ∀ (ai : ℕ), ∀ (ai-bound : nat/strict-below ai m), ∀ (aj : ℕ), ∀ (aj-bound : nat/strict-below aj n), 0 ≤ X ai aj)
  (xy : ∀ (ai : ℕ), ∀ (ai-bound : nat/strict-below ai m), ∀ (aj : ℕ), ∀ (aj-bound : nat/strict-below aj n), X ai aj ≤ Y aj)
  (hrows : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx m), signed/expr-sum-value (fun rj => X idx rj) n = 1)
  → signed/expr-sum-value (fun wi => v wi) m ≤ signed/expr-sum-value (fun oj => f oj · Y oj) n + signed/expr-sum-value (fun i => signed/expr-sum-value (fun column-index => (fun si => fun sj => c si sj · X si sj) i column-index) n) m