Reference · Lemmas behind operations-research checks

rainbow.math.lemmas.mcf-optimal

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

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

signed/reduced-cost-arc-order :
  (rc f g u : ℚ)
  (hg0 : 0 ≤ g)
  (hgu : g ≤ u)
  (hf : rc · f ≤ 0)
  (hs : 0 ≤ rc · (u + signed/negate f))
  → rc · f ≤ rc · g

signed/double-sum-subtract :
  (X Y : ℕ → ℕ → ℚ) (n : ℕ)
  → signed/expr-sum-value (fun i => signed/expr-sum-value (fun column-index => (fun pi-row => fun pi-col => X pi-row pi-col + signed/negate (Y pi-row pi-col)) 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/negate (signed/expr-sum-value (fun i => signed/expr-sum-value (fun column-index => Y i column-index) n) n)

signed/divergence-difference-zero :
  (G F : ℕ → ℕ → ℚ) (b : ℕ → ℚ) (n : ℕ)
  (hG : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), signed/expr-sum-value (fun column-index => G idx column-index) n + signed/negate (signed/expr-sum-value (fun row-index => G row-index idx) n) = b idx)
  (hF : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), signed/expr-sum-value (fun column-index => F idx column-index) n + signed/negate (signed/expr-sum-value (fun row-index => F row-index idx) n) = b idx)
  (i : ℕ) (hi : nat/strict-below i n)
  → signed/expr-sum-value (fun column-index => (fun pi-row => fun pi-col => G pi-row pi-col + signed/negate (F pi-row pi-col)) i column-index) n + signed/negate (signed/expr-sum-value (fun row-index => (fun pi-row => fun pi-col => G pi-row pi-col + signed/negate (F pi-row pi-col)) row-index i) n) = 0

signed/mcf-cost-optimal :
  (c u f g : ℕ → ℕ → ℚ) (pot b : ℕ → ℚ) (n : ℕ)
  (f0 : ∀ (ai : ℕ), ∀ (ai-bound : nat/strict-below ai n), ∀ (aj : ℕ), ∀ (aj-bound : nat/strict-below aj n), 0 ≤ f ai aj)
  (fu : ∀ (ai : ℕ), ∀ (ai-bound : nat/strict-below ai n), ∀ (aj : ℕ), ∀ (aj-bound : nat/strict-below aj n), f ai aj ≤ u ai aj)
  (g0 : ∀ (ai : ℕ), ∀ (ai-bound : nat/strict-below ai n), ∀ (aj : ℕ), ∀ (aj-bound : nat/strict-below aj n), 0 ≤ g ai aj)
  (gu : ∀ (ai : ℕ), ∀ (ai-bound : nat/strict-below ai n), ∀ (aj : ℕ), ∀ (aj-bound : nat/strict-below aj n), g ai aj ≤ u ai aj)
  (fnet : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), signed/expr-sum-value (fun column-index => f idx column-index) n + signed/negate (signed/expr-sum-value (fun row-index => f row-index idx) n) = b idx)
  (gnet : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), signed/expr-sum-value (fun column-index => g idx column-index) n + signed/negate (signed/expr-sum-value (fun row-index => g row-index idx) n) = b idx)
  (hf : ∀ (ai : ℕ), ∀ (ai-bound : nat/strict-below ai n), ∀ (aj : ℕ), ∀ (aj-bound : nat/strict-below aj n), (fun rc-row => fun rc-col => c rc-row rc-col + pot rc-row + signed/negate (pot rc-col)) ai aj · f ai aj ≤ 0)
  (hs : ∀ (ai : ℕ), ∀ (ai-bound : nat/strict-below ai n), ∀ (aj : ℕ), ∀ (aj-bound : nat/strict-below aj n), 0 ≤ (fun rc-row => fun rc-col => c rc-row rc-col + pot rc-row + signed/negate (pot rc-col)) ai aj · (u ai aj + signed/negate (f ai aj)))
  → signed/expr-sum-value (fun i => signed/expr-sum-value (fun column-index => (fun pi-row => fun pi-col => c pi-row pi-col · f pi-row pi-col) i column-index) n) n ≤ signed/expr-sum-value (fun i => signed/expr-sum-value (fun column-index => (fun pi-row => fun pi-col => c pi-row pi-col · g pi-row pi-col) i column-index) n) n