rainbow.math.rational.nnrat.lp-separable-two-var

Non-negative rationals src/rainbow/math/rational/nnrat/lp_separable_two_var.clj0 definitions, 1 theorems

Strong duality for the sum of two decoupled scalar nnrat LPs. Each coordinate uses the canonical witnesses x_i=b_i/a_i and y_i=c_i/a_i from lp-single-positive-constraint-strong-duality. Adding the two scalar zero-gap equivalences proves equality of the summed objectives.

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

nnrat/lp-separable-two-var-zero-gap

TheoremFor all inputsNo axiomsSource, line 114

nnrat/lp-separable-two-var-zero-gap :
  (a1p a1dp b1p b1dp : ℕ) (c1 : ℚ≥0) (a2p a2dp b2p b2dp : ℕ) (c2 : ℚ≥0)
  → c1 · nnrat/divide (nnrat/make (data/succ b1p) b1dp) (nnrat/make (data/succ a1p) a1dp) + c2 · nnrat/divide (nnrat/make (data/succ b2p) b2dp) (nnrat/make (data/succ a2p) a2dp) = nnrat/make (data/succ b1p) b1dp · nnrat/divide c1 (nnrat/make (data/succ a1p) a1dp) + nnrat/make (data/succ b2p) b2dp · nnrat/divide c2 (nnrat/make (data/succ a2p) a2dp)

+ = nnrat/add= = nnrat/equivalent: equality of rational values· = nnrat/multiplyℕ = data/Natℚ≥0 = nnrat/NonnegativeRational