Reference · Non-negative rationals

rainbow.math.rational.nnrat.weighted-sum

Non-negative rationalssrc/rainbow/math/rational/nnrat/weighted_sum.clj1 definitions, 1 theorems

Universal monotonicity of a two-term nonnegative-rational weighted sum in its values -- the first composite guarantee assembled from the monotonicity foundation (nnrat/multiply-monotone + nnrat/add-monotone): wsum2 w0 w1 v0 v1 = w0*v0 + w1*v1 wsum2-monotone : v0 <= v0' -> v1 <= v1' -> wsum2 w0 w1 v0 v1 <= wsum2 w0 w1 v0' v1' (all w0 w1 v..) i.e. raising either input value (weights fixed) never lowers the aggregate: the weighted sum respects dominance. This universally upgrades the weighted-sum / weighted-average catalog family (composite metric, GP posterior mean, EKF/particle filter updates, Monte-Carlo mean), which the AHoF catalog exercised only on worked instances. Proof is a direct composition: scale each term by its weight with nnrat/multiply-monotone, then combine the two ordered terms with the two-sided nnrat/add-monotone. Native and axiom-free; chains rainbow.math.rational.nnrat.multiply-monotone and rainbow.math.rational.nnrat.add-monotone (both on the d63 base).

Depends onmath.rational.nnrat.multiply-monotonemath.rational.nnrat.add-monotone

nnrat/wsum2 :
  (x₁ x₂ x₃ x₄ : ℚ≥0)
  → ℚ≥0

nnrat/wsum2-monotone :
  (w0 w1 v0 v0-hi v1 v1-hi : ℚ≥0)
  (h0 : v0 ≤ v0-hi)
  (h1 : v1 ≤ v1-hi)
  → nnrat/wsum2 w0 w1 v0 v1 ≤ nnrat/wsum2 w0 w1 v0-hi v1-hi