Reference · Finite sums

rainbow.math.sums.nonblocking

Finite sumssrc/rainbow/math/sums/nonblocking.clj0 definitions, 4 theorems

An encoded maximum is nonnegative exactly when at least one preference gap is.

Depends onmath.sums.lp-boundsmath.rational.signed.decide-order

signed/nonnegative-difference-implies-order :
  (x y : ℚ)
  (gap : 0 ≤ y + signed/negate x)
  → x ≤ y

signed/order-implies-nonnegative-difference :
  (x y : ℚ)
  (order : x ≤ y)
  → 0 ≤ y + signed/negate x

signed/nonnegative-maximum-gaps-implies-nonblocking :
  (x y z w : ℚ)
  (encoded : 0 ≤ data/Bool.rec (fun x₄ => ℚ) (y + signed/negate x) (w + signed/negate z) (most))
  → proposition/disjunction (x ≤ y) (z ≤ w)
  where most := signed/decide-at-most (y + signed/negate x) (w + signed/negate z)

signed/nonblocking-implies-nonnegative-maximum-gaps :
  (x y z w : ℚ) (preferences : proposition/disjunction (x ≤ y) (z ≤ w))
  → 0 ≤ data/Bool.rec (fun x₄ => ℚ) (y + signed/negate x) (w + signed/negate z) (most)
  where most := signed/decide-at-most (y + signed/negate x) (w + signed/negate z)