Reference · Non-negative rationals

rainbow.math.rational.nnrat.lp-optimality

Non-negative rationalssrc/rainbow/math/rational/nnrat/lp_optimality.clj0 definitions, 2 theorems

LP optimality certificate over nonnegative rationals -- the sellable corollary of weak duality: a matching feasible primal/dual pair PROVES optimality. nnrat/lp-optimality-certificate : (forall i, (A x)_i <= b_i) -- x primal feasible -> (forall j, c_j <= (Aᵀy)_j) -- y dual feasible -> c.x ~ b.y -- zero duality gap (matching objectives) -> (forall x', (forall i, (A x')_i <= b_i) -> c.x' <= c.x) i.e. any primal-feasible x whose objective matches some dual-feasible y's objective is a maximizer of c.x over all primal-feasible points -- the optimality certificate every LP solver emits, here machine-checked. Proof: for any other feasible x', weak duality gives c.x' <= b.y, and the zero-gap hypothesis rewrites b.y to c.x (at-most-respects-equivalence). Native and axiom-free; chains nnrat-lp-weak-duality on d63.

Depends onmath.rational.nnrat.lp-weak-duality

nnrat/lp-optimality-certificate.{u} :
  (RowT ColT : Type u) (A : RowT → ColT → ℚ≥0) (b : RowT → ℚ≥0) (c x : ColT → ℚ≥0)
  (y : RowT → ℚ≥0) (rows : List RowT) (cols : List ColT)
  (hp : ∀ (i : RowT), nnrat/map-sum ColT (fun j => A i j · x j) cols ≤ b i)
  (hd : ∀ (j : ColT), c j ≤ nnrat/map-sum RowT (fun i => A i j · y i) rows)
  (hgap : sum = nnrat/map-sum RowT (fun i => b i · y i) rows)
  (x-alt : ColT → ℚ≥0)
  (hp-alt : ∀ (i : RowT), nnrat/map-sum ColT (fun j => A i j · x-alt j) cols ≤ b i)
  → nnrat/map-sum ColT (fun j => c j · x-alt j) cols ≤ sum
  where sum := nnrat/map-sum ColT (fun j => c j · x j) cols

nnrat/lp-dual-optimality-certificate.{u} :
  (RowT ColT : Type u) (A : RowT → ColT → ℚ≥0) (b : RowT → ℚ≥0) (c x : ColT → ℚ≥0)
  (y : RowT → ℚ≥0) (rows : List RowT) (cols : List ColT)
  (hp : ∀ (i : RowT), nnrat/map-sum ColT (fun j => A i j · x j) cols ≤ b i)
  (hd : ∀ (j : ColT), c j ≤ nnrat/map-sum RowT (fun i => A i j · y i) rows)
  (hgap : nnrat/map-sum ColT (fun j => c j · x j) cols = sum)
  (y-alt : RowT → ℚ≥0)
  (hd-alt : ∀ (j : ColT), c j ≤ nnrat/map-sum RowT (fun i => A i j · y-alt i) rows)
  → sum ≤ nnrat/map-sum RowT (fun i => b i · y-alt i) rows
  where sum := nnrat/map-sum RowT (fun i => b i · y i) rows