Reference · Signed rationals

rainbow.math.rational.signed.lp-duality-on

Signed rationalssrc/rainbow/math/rational/signed/lp_duality_on.clj0 definitions, 3 theorems

LP weak duality and the optimality certificate, quantified over the rows and columns an instance actually has. These are the same three theorems as `rainbow.math.rational.signed.lp-duality`, with every feasibility hypothesis stated as `signed/all-at-most` over the row or column LIST rather than over the whole index type. That is the difference between a theorem and a checker: on an index type like `data/Nat` a hypothesis `forall i : Nat, (Mx)_i <= b_i` is false for any real program, because the program has no eight-thousandth constraint. Only a finite index type escapes it, and fixing the index type fixes the instance size. With the list form, an instance of ANY size is checked by folding one decided comparison per row and per column -- work a generator emits in a loop -- and handing the resulting conjunctions to `optimization/signed-lp-optimality-certificate-on`. The proofs are the parametric ones with two substitutions: monotonicity through `signed/map-sum-monotone-on` instead of `signed/map-sum-monotone`, and the per-index bound lemmas carried across the list by `signed/all-at-most-combine` instead of being applied at an arbitrary index. Nothing about the mathematics changes; the quantifier does. Native and axiom-free on D63.

Depends onmath.rational.signed.lp-dualitymath.rational.signed.pointwise-order

optimization/signed-double-counting-weak-duality-on.{u} :
  (A B : Type u) (T : A → B → ℚ) (primal : B → ℚ) (dual : A → ℚ) (is : List A)
  (js : List B)
  (column : ∀ j ∈ js, primal j ≤ Σ i∈is, T i j)
  (row : ∀ i ∈ is, Σ j∈js, T i j ≤ dual i)
  → Σ j∈js, primal j ≤ Σ j∈is, dual j

optimization/signed-lp-weak-duality-on.{u} :
  (A B : Type u) (M : A → B → ℚ) (b : A → ℚ) (c x : B → ℚ) (y : A → ℚ) (rows : List A)
  (cols : List B)
  (primal-feasible : ∀ i ∈ rows, Σ j∈cols, M i j · x j ≤ b i)
  (dual-feasible : ∀ j ∈ cols, c j ≤ Σ i∈rows, M i j · y i)
  (x-nonnegative : ∀ i ∈ cols, 0 ≤ x i)
  (y-nonnegative : ∀ i ∈ rows, 0 ≤ y i)
  → Σ j∈cols, c j · x j ≤ Σ i∈rows, b i · y i

optimization/signed-lp-optimality-certificate-on.{u} :
  (A B : Type u) (M : A → B → ℚ) (b : A → ℚ) (c x : B → ℚ) (y : A → ℚ) (rows : List A)
  (cols : List B)
  (primal-feasible : ∀ i ∈ rows, Σ j∈cols, M i j · x j ≤ b i)
  (dual-feasible : ∀ j ∈ cols, c j ≤ Σ i∈rows, M i j · y i)
  (x-nonnegative : ∀ i ∈ cols, 0 ≤ x i)
  (y-nonnegative : ∀ i ∈ rows, 0 ≤ y i)
  (gap : Σ i∈rows, b i · y i = Σ j∈cols, c j · x j)
  (candidate : B → ℚ)
  (candidate-feasible : ∀ i ∈ rows, Σ j∈cols, M i j · candidate j ≤ b i)
  (candidate-nonnegative : ∀ i ∈ cols, 0 ≤ candidate i)
  → Σ j∈cols, c j · candidate j ≤ Σ j∈cols, c j · x j