Reference · Signed rationals

rainbow.math.rational.signed.midpoint-convexity

Signed rationalssrc/rainbow/math/rational/signed/midpoint_convexity.clj0 definitions, 2 theorems

Midpoint convexity over signed rationals: the midpoint stays in [min, max]. signed/midpoint-at-most-max : (1/2)*v0 + (1/2)*v1 <= max v0 v1 signed/midpoint-at-least-min : min v0 v1 <= (1/2)*v0 + (1/2)*v1 where (1/2)*v = smul (from-nnrat nnrat/half) v. The w0=w1=1/2 case of the two-point convex combination -- but proved directly via signed/half-scale-add-self (1/2 M + 1/2 M ~ M), so it needs no nnrat weight-sum equality. Each 1/2*v_i <= 1/2*(max) by multiply-left-monotone (1/2 = from-nnrat nnrat/half >= 0, v_i <= max); sum; collapse 1/2 M + 1/2 M ~ M. Off the magnitude/reciprocal modulus (no reduction wall). Axiom-free; additive; does not touch the LP checker.

Depends onmath.rational.signed.minmaxmath.rational.signed.multiply-monotonemath.rational.signed.order-monotonemath.linear.matrix.half-row-sum-fixed-point-uniquenessmath.rational.signed.multiply-ordermath.rational.signed.order-respectsmath.rational.nnrat.farkas-elim-list

signed/midpoint-at-most-max :
  (v0 v1 : ℚ)
  → signed/from-nnrat nnrat/half · v0 + signed/from-nnrat nnrat/half · v1 ≤ signed/max v0 v1

signed/midpoint-at-least-min :
  (v0 v1 : ℚ)
  → signed/min v0 v1 ≤ signed/from-nnrat nnrat/half · v0 + signed/from-nnrat nnrat/half · v1