Reference · Non-negative rationals

rainbow.math.rational.nnrat.convex-two-point

Non-negative rationalssrc/rainbow/math/rational/nnrat/convex_two_point.clj0 definitions, 2 theorems

The unnormalized two-point convex-combination bracket over nonnegative rationals: (w0+w1)*min(v0,v1) <= w0*v0+w1*v1 <= (w0+w1)*max(v0,v1) The weights are arbitrary nonnegative rationals; they need not sum to one. The two bounds are proved separately so each side can be reused directly: 1. wsum2-monotone lifts min-lower-left/right or max-upper-left/right through multiplication by the nonnegative weights and addition; 2. multiply-distributes-add-right identifies the repeated endpoint sum w0*p+w1*p with (w0+w1)*p up to nnrat equivalence; 3. at-most-respects-equivalence transports the ordered endpoint. Native, non-vacuous, and axiom-free; chains rainbow.math.rational.nnrat.weighted-sum, rainbow.math.rational.nnrat.minmax, and rainbow.math.rational.nnrat.distributive on D63.

Depends onmath.rational.nnrat.weighted-summath.rational.nnrat.minmaxmath.rational.nnrat.distributive

nnrat/two-point-at-least-scaled-min :
  (w0 w1 v0 v1 : ℚ≥0)
  → (w0 + w1) · minmax/min v0 v1 ≤ nnrat/wsum2 w0 w1 v0 v1

nnrat/two-point-at-most-scaled-max :
  (w0 w1 v0 v1 : ℚ≥0)
  → nnrat/wsum2 w0 w1 v0 v1 ≤ (w0 + w1) · minmax/max v0 v1