Reference · Non-negative rationals

rainbow.math.rational.nnrat.map-sum-zero

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

Every term of a vanishing finite nonnegative sum vanishes -- the sum-level form of nonnegativity-forces-zero, stated membership-free by positional split: nnrat/map-sum-zero-at-split : map-sum f (append ps (cons e qs)) ~ 0 -> f e ~ 0 i.e. if a sum over a list is ~ 0, the term at ANY position (identified by writing the list as ps ++ (e :: qs)) is ~ 0. This is the sum-level complementary slackness fact: a zero gap = sum of nonnegative slack terms ~ 0 forces every individual slack to 0. Proof: map-sum-append rewrites the sum to (S ps) + ((f e) + (S qs)); two uses of add-zero-split (right then left) peel off (f e). Polymorphic in the element type. Native and axiom-free; chains nnrat-map-sum-append and nnrat-add-zero-split on d63.

Depends onmath.rational.nnrat.map-sum-appendmath.rational.nnrat.add-zero-split

nnrat/map-sum-zero-at-split.{u} :
  (A : Type u) (f : A → ℚ≥0) (ps : List A) (e : A) (qs : List A)
  (h : nnrat/map-sum A f (list/append A ps (data/cons A e qs)) = 0)
  → f e = 0