Reference · Non-negative rationals

rainbow.math.rational.nnrat.lp-multi-constraint-duality

Non-negative rationalssrc/rainbow/math/rational/nnrat/lp_multi_constraint_duality.clj2 definitions, 5 theorems

Finite positive-constraint, one-variable LP duality over nnrat. A constraint is stored as ((ap,adp),(bp,bdp)) and denotes make(succ ap,adp) * x <= make(succ bp,bdp). Thus positivity of both coefficients is structural. A non-empty family is represented by one constraint's four parameters and a list of remaining constraints. Its canonical primal point is the `min-ub` fold of all b/a ratios. We prove that point feasible, largest among feasible points, and objective-optimal for every nonnegative objective coefficient. The final theorem additionally accepts evidence that the head constraint is binding. It constructs the concentrated dual weight c/a at that constraint, proves dual feasibility and zero gap, and packages primal strong duality. This is the explicit-binding-index form of finite multi-constraint strong duality; extracting such an index from the fold is deliberately separate. Every declaration is native proof data and axiom-free on D63.

Depends onmath.rational.nnrat.lp-strong-duality-general

nnrat/lp-positive-constraint-ratios :
  (x₁ : List (data/Product (data/Product ℕ ℕ) (data/Product ℕ ℕ)))
  → List ℚ≥0

nnrat/lp-positive-constraints-feasible :
  (x₁ : List (data/Product (data/Product ℕ ℕ) (data/Product ℕ ℕ))) (x₂ : ℚ≥0)
  → Prop

nnrat/lp-positive-constraints-normalize-upper :
  (constraints : List (data/Product (data/Product ℕ ℕ) (data/Product ℕ ℕ)))
  (value : ℚ≥0)
  → proposition/conjunction (feasible → data/List.rec ℚ≥0 (fun x₂₃ => Prop) proposition/truth (fun upper => fun x₂₄ => fun ih => proposition/conjunction (value ≤ upper) ih) (nnrat/lp-positive-constraint-ratios constraints)) (data/List.rec ℚ≥0 (fun x₃₁ => Prop) proposition/truth (fun upper => fun x₃₂ => fun ih => proposition/conjunction (value ≤ upper) ih) (nnrat/lp-positive-constraint-ratios constraints) → feasible)
  where feasible := nnrat/lp-positive-constraints-feasible constraints value

nnrat/lp-positive-multi-primal-feasible :
  (ap adp bp bdp : ℕ) (tail : List (data/Product (data/Product ℕ ℕ) (data/Product ℕ ℕ)))
  → proposition/conjunction (nnrat/make (data/succ ap) adp · nnrat/min-ub (nnrat/divide (nnrat/make (data/succ bp) bdp) (nnrat/make (data/succ ap) adp)) (nnrat/lp-positive-constraint-ratios tail) ≤ nnrat/make (data/succ bp) bdp) (feasible)
  where feasible := nnrat/lp-positive-constraints-feasible tail (nnrat/min-ub (nnrat/divide (nnrat/make (data/succ bp) bdp) (nnrat/make (data/succ ap) adp)) (nnrat/lp-positive-constraint-ratios tail))

nnrat/lp-positive-multi-primal-largest :
  (ap adp bp bdp : ℕ) (tail : List (data/Product (data/Product ℕ ℕ) (data/Product ℕ ℕ)))
  (value : ℚ≥0)
  (feasible : proposition/conjunction (nnrat/make (data/succ ap) adp · value ≤ nnrat/make (data/succ bp) bdp) (feasible))
  → value ≤ nnrat/min-ub (divide) (nnrat/lp-positive-constraint-ratios tail)
  where divide := nnrat/divide (nnrat/make (data/succ bp) bdp) (nnrat/make (data/succ ap) adp)
  where feasible := nnrat/lp-positive-constraints-feasible tail value

nnrat/lp-positive-multi-primal-optimal :
  (ap adp bp bdp : ℕ) (tail : List (data/Product (data/Product ℕ ℕ) (data/Product ℕ ℕ)))
  (c alternative : ℚ≥0)
  (alternative-feasible : proposition/conjunction (nnrat/make (data/succ ap) adp · alternative ≤ nnrat/make (data/succ bp) bdp) (feasible))
  → c · alternative ≤ c · nnrat/min-ub (divide) (nnrat/lp-positive-constraint-ratios tail)
  where divide := nnrat/divide (nnrat/make (data/succ bp) bdp) (nnrat/make (data/succ ap) adp)
  where feasible := nnrat/lp-positive-constraints-feasible tail alternative

nnrat/lp-positive-multi-head-binding-strong-duality :
  (ap adp bp bdp : ℕ) (tail : List (data/Product (data/Product ℕ ℕ) (data/Product ℕ ℕ)))
  (c : ℚ≥0)
  (binding : nnrat/divide (nnrat/make (data/succ bp) bdp) (nnrat/make (data/succ ap) adp) = nnrat/min-ub (nnrat/divide (nnrat/make (data/succ bp) bdp) (nnrat/make (data/succ ap) adp)) (nnrat/lp-positive-constraint-ratios tail))
  → proposition/conjunction (conjunction₁) (conjunction)
  where conjunction := proposition/conjunction (c ≤ nnrat/make (data/succ ap) adp · nnrat/divide c (nnrat/make (data/succ ap) adp)) (proposition/conjunction (c · nnrat/min-ub (nnrat/divide (nnrat/make (data/succ bp) bdp) (nnrat/make (data/succ ap) adp)) (nnrat/lp-positive-constraint-ratios tail) = nnrat/make (data/succ bp) bdp · nnrat/divide c (nnrat/make (data/succ ap) adp)) (∀ (alternative : ℚ≥0), ∀ (alternative-feasible : proposition/conjunction (nnrat/make (data/succ ap) adp · alternative ≤ nnrat/make (data/succ bp) bdp) (nnrat/lp-positive-constraints-feasible tail alternative)), c · alternative ≤ c · nnrat/min-ub (nnrat/divide (nnrat/make (data/succ bp) bdp) (nnrat/make (data/succ ap) adp)) (nnrat/lp-positive-constraint-ratios tail)))
  where conjunction₁ := proposition/conjunction (nnrat/make (data/succ ap) adp · nnrat/min-ub (nnrat/divide (nnrat/make (data/succ bp) bdp) (nnrat/make (data/succ ap) adp)) (nnrat/lp-positive-constraint-ratios tail) ≤ nnrat/make (data/succ bp) bdp) (nnrat/lp-positive-constraints-feasible tail (nnrat/min-ub (nnrat/divide (nnrat/make (data/succ bp) bdp) (nnrat/make (data/succ ap) adp)) (nnrat/lp-positive-constraint-ratios tail)))