Reference · Matrices

rainbow.math.linear.matrix.affine-trajectory-order

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

Successive-order laws for finite signed affine value iteration. Iterating once before an arbitrary finite run agrees with taking one more step. For nonnegative matrices this shift law turns a Bellman subsolution `x <= F x` into an ascending trajectory and a supersolution `F x <= x` into a descending trajectory. Theorem-only, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-fixed-point-order

matrix/affine-iterate-shift :
  (rows : List (List ℚ)) (offset initial : List ℚ) (steps : ℕ)
  → vector/equivalent (iterate) (iterate₁)
  where iterate := matrix/affine-iterate rows offset steps (matrix/affine-action rows offset initial)
  where iterate₁ := matrix/affine-iterate rows offset (data/succ steps) initial

matrix/affine-iterate-subsolution-ascending :
  (rows : List (List ℚ)) (offset initial : List ℚ)
  (rows-positive : matrix/at-most (matrix/zero-like rows) rows)
  (subsolution : vector/at-most initial (action)) (steps : ℕ)
  → vector/at-most (iterate₁) (iterate)
  where action := matrix/affine-action rows offset initial
  where iterate := matrix/affine-iterate rows offset (data/succ steps) initial
  where iterate₁ := matrix/affine-iterate rows offset steps initial

matrix/affine-iterate-supersolution-descending :
  (rows : List (List ℚ)) (offset initial : List ℚ)
  (rows-positive : matrix/at-most (matrix/zero-like rows) rows)
  (supersolution : vector/at-most (action) initial) (steps : ℕ)
  → vector/at-most (iterate) (iterate₁)
  where action := matrix/affine-action rows offset initial
  where iterate := matrix/affine-iterate rows offset (data/succ steps) initial
  where iterate₁ := matrix/affine-iterate rows offset steps initial