Reference · Non-negative rationals

rainbow.math.rational.nnrat.lp-gap

Non-negative rationalssrc/rainbow/math/rational/nnrat/lp_gap.clj0 definitions, 1 theorems

LP duality-gap decomposition over nonnegative rationals -- the identity behind complementary slackness. Because nnrat has no subtraction, feasibility is stated as equality with an explicit nonnegative slack: primal: (A x)_i + s_i ~ b_i (s : slacks, rows -> nnrat) dual: c_j + r_j ~ (Aᵀy)_j (r : reduced costs, cols -> nnrat) nnrat/lp-gap-decomposition : b.y ~ c.x + ( sum_j r_j x_j + sum_i s_i y_i ) The dual objective exceeds the primal objective by exactly the total complementary-slackness term (a sum of nonnegative products r_j x_j and s_i y_i). Combined with nnrat/add-zero-split + map-sum-zero-at-split, a zero gap forces every r_j x_j and s_i y_i to 0 -- complementary slackness. Proof: expand b.y termwise via the primal slack equality (dist-right + map-sum-add), swap the double sum (scale-right + Fubini map-sum-swap + one per-term reorder) to sum_j (Aᵀy)_j x_j, then expand via the dual equality; the three pieces chain and reassociate. Native and axiom-free; chains nnrat-lp-weak-duality (which brings the whole finite-sum toolkit) on d63.

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

nnrat/lp-gap-decomposition.{u} :
  (RowT ColT : Type u) (A : RowT → ColT → ℚ≥0) (b : RowT → ℚ≥0) (c x : ColT → ℚ≥0)
  (y s : RowT → ℚ≥0) (r : ColT → ℚ≥0) (rows : List RowT) (cols : List ColT)
  (hp : ∀ (i : RowT), nnrat/map-sum ColT (fun j => A i j · x j) cols + s i = b i)
  (hd : ∀ (j : ColT), c j + r j = nnrat/map-sum RowT (fun i => A i j · y i) rows)
  → nnrat/map-sum RowT (fun i => b i · y i) rows = nnrat/map-sum ColT (fun j => c j · x j) cols + (nnrat/map-sum ColT (fun j => r j · x j) cols + nnrat/map-sum RowT (fun i => s i · y i) rows)