Reference · Non-negative rationals

rainbow.math.rational.nnrat.convex-normalized

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

The normalized two-point convex bracket over nonnegative rationals. Given weights whose total is equivalent to the structurally positive rational `s = nnrat/make (data/succ sp) sdp`, the weighted average lies between its two inputs: min(x,y) <= (w0*x+w1*y)/s <= max(x,y). The proofs transport the scaled bounds from nnrat-convex-two-point from the coefficient `w0+w1` to `s`, then use the forward directions of the positive coefficient normalization equivalences from nnrat-order-scale. Native, non-vacuous, and axiom-free on D63.

Depends onmath.rational.nnrat.convex-two-point

nnrat/two-point-normalized-at-least-min :
  (w0 w1 x y : ℚ≥0) (sp sdp : ℕ)
  (total-positive : w0 + w1 = nnrat/make (data/succ sp) sdp)
  → minmax/min x y ≤ nnrat/divide (w0 · x + w1 · y) (nnrat/make (data/succ sp) sdp)

nnrat/two-point-normalized-at-most-max :
  (w0 w1 x y : ℚ≥0) (sp sdp : ℕ)
  (total-positive : w0 + w1 = nnrat/make (data/succ sp) sdp)
  → nnrat/divide (w0 · x + w1 · y) (nnrat/make (data/succ sp) sdp) ≤ minmax/max x y