Reference · Vectors

rainbow.math.linear.vector.convex-combination

Vectorssrc/rainbow/math/linear/vector/convex_combination.clj1 definitions, 10 theorems

Normalized two-point convex combinations preserve vector intervals.

Depends onmath.linear.vector.add-ordermath.rational.signed.scale-order

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

signed/scale-additive-rate :
  (w0 w1 : ℚ≥0) (value : ℚ)
  → signed/scale w0 value + signed/scale w1 value = signed/scale (w0 + w1) value

signed/scale-one :
  (value : ℚ)
  → signed/scale 1 value = value

signed/scale-respects-rate-equivalence :
  (left-rate right-rate : ℚ≥0) (value : ℚ)
  (same-rate : left-rate = right-rate)
  → signed/scale left-rate value = signed/scale right-rate value

vector/scale-additive-rate :
  (w0 w1 : ℚ≥0) (values : List ℚ)
  → vector/equivalent (add) (vector/scale (w0 + w1) values)
  where add := vector/add (vector/scale w0 values) (vector/scale w1 values)

vector/scale-one :
  (values : List ℚ)
  → vector/equivalent (vector/scale 1 values) values

vector/scale-respects-rate-equivalence :
  (left-rate right-rate : ℚ≥0) (values : List ℚ)
  (same-rate : left-rate = right-rate)
  → vector/equivalent (vector/scale left-rate values) (vector/scale right-rate values)

vector/nnrat-wsum2-monotone :
  (w0 w1 : ℚ≥0) (left left-prime right right-prime : List ℚ)
  (left-ordered : vector/at-most left left-prime)
  (right-ordered : vector/at-most right right-prime)
  → vector/at-most (vector/nnrat-wsum2 w0 w1 left right) (wsum2)
  where wsum2 := vector/nnrat-wsum2 w0 w1 left-prime right-prime

vector/nnrat-wsum2-normalized-repeated :
  (w0 w1 : ℚ≥0) (values : List ℚ)
  (normalized : w0 + w1 = 1)
  → vector/equivalent (vector/nnrat-wsum2 w0 w1 values values) values

vector/nnrat-convex-lower-bound :
  (w0 w1 : ℚ≥0) (lower left right : List ℚ)
  (normalized : w0 + w1 = 1)
  (lower-left : vector/at-most lower left) (lower-right : vector/at-most lower right)
  → vector/at-most lower (vector/nnrat-wsum2 w0 w1 left right)

vector/nnrat-convex-upper-bound :
  (w0 w1 : ℚ≥0) (left right upper : List ℚ)
  (normalized : w0 + w1 = 1)
  (left-upper : vector/at-most left upper) (right-upper : vector/at-most right upper)
  → vector/at-most (vector/nnrat-wsum2 w0 w1 left right) upper