Reference · Finite sums

rainbow.math.sums.lp-bounds

Finite sumssrc/rainbow/math/sums/lp_bounds.clj0 definitions, 4 theorems

Finite covering duality and certificate-gap arithmetic, reusing the existing list-backed LP theorem. No integrality, positivity of matrix data, or nonempty dimension is assumed. Store families supply their exact feasibility premises.

Depends onmath.lemmas.lp-dualitymath.sums.flow-cut

signed/expr-sum-covering-weak-duality :
  (A : ℕ → ℕ → ℚ) (b c x y : ℕ → ℚ) (m n : ℕ)
  (primal : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx m), b idx ≤ signed/expr-sum-value (fun j => A idx j · x j) n)
  (xn : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), 0 ≤ x idx)
  (yn : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx m), 0 ≤ y idx)
  (dual : ∀ (idx : ℕ), ∀ (bound : nat/strict-below idx n), signed/expr-sum-value (fun i => A i idx · y i) m ≤ c idx)
  → signed/expr-sum-value (fun z => b z · y z) m ≤ signed/expr-sum-value (fun z => c z · x z) n

signed/expr-sum-column-commute :
  (A : ℕ → ℕ → ℚ) (y : ℕ → ℚ) (m j : ℕ)
  → signed/expr-sum-value (fun i => y i · A i j) m = signed/expr-sum-value (fun i => A i j · y i) m

signed/expr-sum-unit-objective :
  (x : ℕ → ℚ) (n : ℕ)
  → signed/expr-sum-value (fun z => (fun x₂ => 1) z · x z) n = signed/expr-sum-value x n

signed/certificate-gap-upper-bound :
  (primal dual eps : ℚ)
  (gap : dual + signed/negate primal ≤ eps)
  → dual ≤ primal + eps