Reference · Non-negative rationals

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

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

Zero total duality gap for a finite list of decoupled scalar nnrat LPs. The coefficients a, b, and c are functions on a shared index type. Natural predecessor functions ap/adp and bp/bdp witness pointwise that a and b have the positive forms required by scalar strong duality. The scalar zero-gap conjunct is transported along those witnesses and then lifted through the finite sum by map-sum-respects-equivalence. Universe-polymorphic in the index type, native, and axiom-free; chains the scalar strong-duality theorem and the finite-sum congruence on d63.

Depends onmath.rational.nnrat.lp-strong-duality-generalmath.rational.nnrat.map-sum-respects

nnrat/lp-separable-multi-var-zero-gap.{u} :
  (A : Type u) (a b c : A → ℚ≥0) (ap adp bp bdp : A → ℕ)
  (ha : ∀ (i : A), nnrat/make (data/succ (ap i)) (adp i) = a i)
  (hb : ∀ (i : A), nnrat/make (data/succ (bp i)) (bdp i) = b i)
  (idx : List A)
  → nnrat/map-sum A (fun i => c i · nnrat/divide (b i) (a i)) idx = nnrat/map-sum A (fun i => b i · nnrat/divide (c i) (a i)) idx