Reference · Matrices

rainbow.math.linear.matrix.affine-residual-iteration

Matricessrc/rainbow/math/linear/matrix/affine_residual_iteration.clj0 definitions, 3 theorems

Finite value-iteration guarantees from linear residual inequalities. With nonnegative rows, `x - rows*x <= offset` certifies an ascending affine trajectory and `offset <= x - rows*x` certifies a descending one. A lower certificate and an upper certificate therefore form an invariant interval for every finite iterate started between them. Only the value/image shape needed to add the matrix image back is assumed. Theorem-only, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-residual-order

matrix/affine-iterate-residual-upper-ascending :
  (rows : List (List ℚ)) (offset initial : List ℚ)
  (rows-positive : matrix/at-most (matrix/zero-like rows) rows)
  (value-image-shape : vector/same-shape initial (matrix/vector-multiply rows initial))
  (residual-upper : vector/at-most (subtract) offset) (steps : ℕ)
  → vector/at-most (iterate₂) (iterate)
  where iterate := matrix/affine-iterate rows offset (data/succ steps) initial
  where iterate₂ := matrix/affine-iterate rows offset steps initial
  where subtract := vector/subtract initial (matrix/vector-multiply rows initial)

matrix/affine-iterate-residual-lower-descending :
  (rows : List (List ℚ)) (offset initial : List ℚ)
  (rows-positive : matrix/at-most (matrix/zero-like rows) rows)
  (value-image-shape : vector/same-shape initial (matrix/vector-multiply rows initial))
  (residual-lower : vector/at-most offset (subtract)) (steps : ℕ)
  → vector/at-most (iterate) (iterate₂)
  where iterate := matrix/affine-iterate rows offset (data/succ steps) initial
  where iterate₂ := matrix/affine-iterate rows offset steps initial
  where subtract := vector/subtract initial (matrix/vector-multiply rows initial)

matrix/affine-iterate-residual-invariant-interval :
  (rows : List (List ℚ)) (offset lower initial upper : List ℚ)
  (rows-positive : matrix/at-most (matrix/zero-like rows) rows)
  (lower-image-shape : vector/same-shape lower (matrix/vector-multiply rows lower))
  (upper-image-shape : vector/same-shape upper (matrix/vector-multiply rows upper))
  (lower-residual-upper : vector/at-most (subtract) offset)
  (upper-residual-lower : vector/at-most offset (subtract₃))
  (lower-initial : vector/at-most lower initial)
  (initial-upper : vector/at-most initial upper) (steps : ℕ)
  → proposition/conjunction (most₁) (most)
  where most := vector/at-most (matrix/affine-iterate rows offset steps initial) upper
  where most₁ := vector/at-most lower (matrix/affine-iterate rows offset steps initial)
  where subtract := vector/subtract lower (matrix/vector-multiply rows lower)
  where subtract₃ := vector/subtract upper (matrix/vector-multiply rows upper)