Reference · Non-negative rationals

rainbow.math.rational.nnrat.weighted-dot

Non-negative rationalssrc/rainbow/math/rational/nnrat/weighted_dot.clj1 definitions, 1 theorems

Weighted sum (dot product) of nonnegative-rational coordinate functions over an index list, and its monotonicity in the value coordinates: nnrat/weighted-sum A c x is = sum_i (c i) * (x i) over is : List A nnrat/weighted-sum-monotone : (forall i, x i <= x' i) -> weighted-sum c x is <= weighted-sum c x' is This is the LP objective-bound engine: with nonnegative weights c, dominating the values coordinatewise (x <= x') dominates the weighted total -- the monotone direction behind c.x <= c.x' and, composed with a feasibility substitution, weak duality c.x <= b.y. Proof: nnrat/map-sum-monotone applied to the composite terms (c i)*(x i), whose termwise domination is nnrat/multiply-monotone (nonneg weight preserves <=). Polymorphic in the index type A. Native and axiom-free; chains nnrat-list-sum and nnrat-multiply-monotone on d63.

Depends onmath.rational.nnrat.list-summath.rational.nnrat.multiply-monotone

nnrat/weighted-sum.{u} :
  (A : Type u) (c x : A → ℚ≥0) (x₁ : List A)
  → ℚ≥0

nnrat/weighted-sum-monotone.{u} :
  (A : Type u) (c x x-hi : A → ℚ≥0)
  (hx : ∀ (i : A), x i ≤ x-hi i)
  (is : List A)
  → nnrat/weighted-sum A c x is ≤ nnrat/weighted-sum A c x-hi is