Reference · Non-negative rationals

rainbow.math.rational.nnrat.lp-weak-duality

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

LP weak duality over nonnegative rationals -- the frontier-OR capstone: primal max c.x s.t. A x <= b, x >= 0 (x : cols -> nnrat) dual min b.y s.t. Aᵀy >= c, y >= 0 (y : rows -> nnrat) nnrat/lp-weak-duality : (forall i, (A x)_i <= b_i) -- primal feasibility -> (forall j, c_j <= (Aᵀy)_j) -- dual feasibility -> c.x <= b.y Nonnegativity of x, y is automatic (nnrat). Dot products are map-sum over the index lists. This is the verified, axiom-free weak-duality bound: any dual feasible objective bounds any primal feasible objective from above -- the soundness core of every LP relaxation / bound certificate in OR. Proof (all products in a fixed order, one per-term reorder): c.x = sum_j c_j x_j <= sum_j (Aᵀy)_j x_j [map-sum-monotone + multiply-right-monotone, dual feas] ~ sum_j sum_i (A_ij y_i) x_j [map-sum-scale-right under map-sum-respects] ~ sum_i sum_j (A_ij y_i) x_j [Fubini map-sum-swap] ~ sum_i sum_j (A_ij x_j) y_i [per-term reorder: assoc+comm+mult-respects] ~ sum_i (A x)_i y_i [map-sum-scale-right backwards, under map-sum-respects] <= sum_i b_i y_i = b.y [map-sum-monotone + multiply-right-monotone, primal feas] the ~ chain bridged to <= by at-most-respects-equivalence + at-most-transitive. Native and axiom-free; chains the finite-sum toolkit (list-sum monotone, map-sum respects/scale-right, Fubini) plus multiply right-monotone/associative/ commutative(standalone) and d63 multiply-respects/at-most-respects.

Depends onmath.rational.nnrat.list-summath.rational.nnrat.map-sum-respectsmath.rational.nnrat.map-sum-scalemath.rational.nnrat.fubinimath.rational.nnrat.multiply-right-monotonemath.rational.nnrat.multiply-commutemath.rational.nnrat.product-reassociation

nnrat/lp-weak-duality.{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)
  → nnrat/map-sum ColT (fun j => c j · x j) cols ≤ nnrat/map-sum RowT (fun i => b i · y i) rows