Reference · Non-negative rationals

rainbow.math.rational.nnrat.convex

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

The convex-combination bound -- the capstone of the nnrat monotonicity + algebra foundation: convex-at-most-max : (w0 + w1) ~ 1 -> w0*v0 + w1*v1 <= max v0 v1 (all w0 w1 v0 v1) A weighted average with weights summing to one never exceeds the larger value -- the universal soundness behind every convex-combination / weighted-average step in the AHoF catalog (interpolation, exponential smoothing, mixing, barycentric updates), which the catalog exercised only on worked instances. Assembly (each piece proved earlier this layer): 1. wsum2-monotone with max-upper-left/right : w0*v0+w1*v1 <= w0*M + w1*M (M = max v0 v1) 2. multiply-distributes-add-right (reversed) : w0*M + w1*M ~ (w0+w1)*M 3. multiply-respects-equivalence with the hyp : (w0+w1)*M ~ 1*M 4. multiply-one-left : 1*M ~ M => w0*M+w1*M ~ M ; transport the bound's right endpoint with at-most-respects-equivalence to conclude <= M. Native and axiom-free; chains rainbow.math.rational.nnrat.weighted-sum (=> multiply/add monotone), rainbow.math.rational.nnrat.minmax, and rainbow.math.rational.nnrat.distributive.

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

nnrat/convex-at-most-max :
  (w0 w1 v0 v1 : ℚ≥0)
  (hw : w0 + w1 = 1)
  → nnrat/wsum2 w0 w1 v0 v1 ≤ minmax/max v0 v1

nnrat/convex-at-least-min :
  (w0 w1 v0 v1 : ℚ≥0)
  (hw : w0 + w1 = 1)
  → minmax/min v0 v1 ≤ nnrat/wsum2 w0 w1 v0 v1