Reference · Matrices

rainbow.math.linear.matrix.interval-order

Matricessrc/rainbow/math/linear/matrix/interval_order.clj0 definitions, 10 theorems

Interval propagation for signed vectors and native finite matrices. Monotone and antitone dot, action, and product maps send an explicit pointwise interval to the corresponding endpoint interval. Nonnegative fixed operands preserve endpoint orientation; nonpositive fixed operands reverse it. These paired bounds are reusable certificates for Bellman enclosures and bounded OR trajectories. Theorem-only and axiom-free on D63.

Depends onmath.linear.matrix.antitone

vector/dot-bounds-nonnegative-weights :
  (lower value upper weights : List ℚ)
  (weights-positive : vector/at-most (vector/zero-like weights) weights)
  (lower-ordered : vector/at-most lower value)
  (upper-ordered : vector/at-most value upper)
  → proposition/conjunction (vector/dot lower weights ≤ vector/dot value weights) (vector/dot value weights ≤ vector/dot upper weights)

vector/dot-bounds-nonpositive-weights :
  (lower value upper weights : List ℚ)
  (weights-negative : vector/at-most weights (vector/zero-like weights))
  (lower-ordered : vector/at-most lower value)
  (upper-ordered : vector/at-most value upper)
  → proposition/conjunction (vector/dot upper weights ≤ vector/dot value weights) (vector/dot value weights ≤ vector/dot lower weights)

matrix/vector-multiply-bounds-nonnegative-rows :
  (rows : List (List ℚ)) (lower value upper : List ℚ)
  (rows-positive : matrix/at-most (matrix/zero-like rows) rows)
  (lower-ordered : vector/at-most lower value)
  (upper-ordered : vector/at-most value upper)
  → proposition/conjunction (most) (most₁)
  where most := vector/at-most (matrix/vector-multiply rows lower) (matrix/vector-multiply rows value)
  where most₁ := vector/at-most (matrix/vector-multiply rows value) (matrix/vector-multiply rows upper)

matrix/vector-multiply-bounds-nonpositive-rows :
  (rows : List (List ℚ)) (lower value upper : List ℚ)
  (rows-negative : matrix/at-most rows (matrix/zero-like rows))
  (lower-ordered : vector/at-most lower value)
  (upper-ordered : vector/at-most value upper)
  → proposition/conjunction (most₁) (most)
  where most := vector/at-most (matrix/vector-multiply rows value) (matrix/vector-multiply rows lower)
  where most₁ := vector/at-most (matrix/vector-multiply rows upper) (matrix/vector-multiply rows value)

matrix/vector-multiply-bounds-nonnegative-values :
  (lower value upper : List (List ℚ)) (values : List ℚ)
  (values-positive : vector/at-most (vector/zero-like values) values)
  (lower-ordered : matrix/at-most lower value)
  (upper-ordered : matrix/at-most value upper)
  → proposition/conjunction (most) (most₁)
  where most := vector/at-most (matrix/vector-multiply lower values) (matrix/vector-multiply value values)
  where most₁ := vector/at-most (matrix/vector-multiply value values) (matrix/vector-multiply upper values)

matrix/vector-multiply-bounds-nonpositive-values :
  (lower value upper : List (List ℚ)) (values : List ℚ)
  (values-negative : vector/at-most values (vector/zero-like values))
  (lower-ordered : matrix/at-most lower value)
  (upper-ordered : matrix/at-most value upper)
  → proposition/conjunction (most₁) (most)
  where most := vector/at-most (matrix/vector-multiply value values) (matrix/vector-multiply lower values)
  where most₁ := vector/at-most (matrix/vector-multiply upper values) (matrix/vector-multiply value values)

matrix/multiply-bounds-left-nonnegative-factor :
  (lower value upper factor : List (List ℚ))
  (factor-positive : matrix/at-most (matrix/zero-like factor) factor)
  (lower-ordered : matrix/at-most lower value)
  (upper-ordered : matrix/at-most value upper)
  → proposition/conjunction (most₁) (most)
  where most := matrix/at-most (matrix/multiply value factor) (matrix/multiply upper factor)
  where most₁ := matrix/at-most (matrix/multiply lower factor) (matrix/multiply value factor)

matrix/multiply-bounds-left-nonpositive-factor :
  (lower value upper factor : List (List ℚ))
  (factor-negative : matrix/at-most factor (matrix/zero-like factor))
  (lower-ordered : matrix/at-most lower value)
  (upper-ordered : matrix/at-most value upper)
  → proposition/conjunction (most₁) (most)
  where most := matrix/at-most (matrix/multiply value factor) (matrix/multiply lower factor)
  where most₁ := matrix/at-most (matrix/multiply upper factor) (matrix/multiply value factor)

matrix/multiply-bounds-right-nonnegative-factor :
  (factor lower value upper : List (List ℚ))
  (factor-positive : matrix/at-most (matrix/zero-like factor) factor)
  (lower-ordered : matrix/at-most lower value)
  (upper-ordered : matrix/at-most value upper)
  → proposition/conjunction (most) (most₁)
  where most := matrix/at-most (matrix/multiply factor lower) (matrix/multiply factor value)
  where most₁ := matrix/at-most (matrix/multiply factor value) (matrix/multiply factor upper)

matrix/multiply-bounds-right-nonpositive-factor :
  (factor lower value upper : List (List ℚ))
  (factor-negative : matrix/at-most factor (matrix/zero-like factor))
  (lower-ordered : matrix/at-most lower value)
  (upper-ordered : matrix/at-most value upper)
  → proposition/conjunction (most) (most₁)
  where most := matrix/at-most (matrix/multiply factor upper) (matrix/multiply factor value)
  where most₁ := matrix/at-most (matrix/multiply factor value) (matrix/multiply factor lower)