Reference · Matrices

rainbow.math.linear.matrix.signed-scale-sign

Matricessrc/rainbow/math/linear/matrix/signed_scale_sign.clj0 definitions, 9 theorems

The remaining sign combinations for signed scalar, vector, and matrix scaling. Nonnegative factor times nonpositive value and nonpositive factor times nonnegative value are nonpositive; nonpositive factor times nonpositive value is nonnegative. Scalar proofs use monotonicity/antitonicity against zero and the arbitrary-factor zero law. Two small proof-data generators lift each checked scalar rule structurally to vectors and matrices. Native and axiom-free on D63.

Depends onmath.linear.matrix.signed-scale-positive

signed/scale-difference-nonpositive-of-nonnegative-factor :
  (factor value : ℚ)
  (factor-sign : 0 ≤ factor)
  (value-sign : value ≤ 0)
  → signed/scale (signed/positive factor) value - signed/scale (signed/negative factor) value ≤ 0

signed/scale-difference-nonpositive-of-nonpositive-factor :
  (factor value : ℚ)
  (factor-sign : factor ≤ 0)
  (value-sign : 0 ≤ value)
  → signed/scale (signed/positive factor) value - signed/scale (signed/negative factor) value ≤ 0

signed/scale-difference-nonnegative-of-nonpositive-factor :
  (factor value : ℚ)
  (factor-sign : factor ≤ 0)
  (value-sign : value ≤ 0)
  → 0 ≤ signed/scale (signed/positive factor) value - signed/scale (signed/negative factor) value

vector/signed-scale-nonpositive-of-nonnegative-factor :
  (factor : ℚ) (values : List ℚ)
  (factor-sign : 0 ≤ factor)
  (values-sign : vector/at-most values (vector/zero-like values))
  → vector/at-most (vector/signed-scale factor values) (vector/zero-like (vector/signed-scale factor values))

vector/signed-scale-nonpositive-of-nonpositive-factor :
  (factor : ℚ) (values : List ℚ)
  (factor-sign : factor ≤ 0)
  (values-sign : vector/at-most (vector/zero-like values) values)
  → vector/at-most (vector/signed-scale factor values) (vector/zero-like (vector/signed-scale factor values))

vector/signed-scale-nonnegative-of-nonpositive-factor :
  (factor : ℚ) (values : List ℚ)
  (factor-sign : factor ≤ 0)
  (values-sign : vector/at-most values (vector/zero-like values))
  → vector/at-most (vector/zero-like (vector/signed-scale factor values)) (vector/signed-scale factor values)

matrix/signed-scale-nonpositive-of-nonnegative-factor :
  (factor : ℚ) (rows : List (List ℚ))
  (factor-sign : 0 ≤ factor)
  (rows-sign : matrix/at-most rows (matrix/zero-like rows))
  → matrix/at-most (matrix/signed-scale factor rows) (matrix/zero-like (matrix/signed-scale factor rows))

matrix/signed-scale-nonpositive-of-nonpositive-factor :
  (factor : ℚ) (rows : List (List ℚ))
  (factor-sign : factor ≤ 0)
  (rows-sign : matrix/at-most (matrix/zero-like rows) rows)
  → matrix/at-most (matrix/signed-scale factor rows) (matrix/zero-like (matrix/signed-scale factor rows))

matrix/signed-scale-nonnegative-of-nonpositive-factor :
  (factor : ℚ) (rows : List (List ℚ))
  (factor-sign : factor ≤ 0)
  (rows-sign : matrix/at-most rows (matrix/zero-like rows))
  → matrix/at-most (matrix/zero-like (matrix/signed-scale factor rows)) (matrix/signed-scale factor rows)