Reference · Matrices

rainbow.math.linear.matrix.affine-invariant-interval

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

Invariant intervals for finite signed affine value iteration. Under a nonnegative matrix, a Bellman subsolution lies below every iterate started from itself and a supersolution lies above every iterate started from itself. Monotonicity then proves that any initial value between those two certificates remains trapped between them at every finite step. Theorem-only, kernel-checked, and axiom-free on D63.

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

matrix/affine-iterate-above-subsolution :
  (rows : List (List ℚ)) (offset subsolution : List ℚ)
  (rows-positive : matrix/at-most (matrix/zero-like rows) rows)
  (post-fixed : vector/at-most subsolution (action)) (steps : ℕ)
  → vector/at-most subsolution (iterate)
  where action := matrix/affine-action rows offset subsolution
  where iterate := matrix/affine-iterate rows offset steps subsolution

matrix/affine-iterate-below-supersolution :
  (rows : List (List ℚ)) (offset supersolution : List ℚ)
  (rows-positive : matrix/at-most (matrix/zero-like rows) rows)
  (pre-fixed : vector/at-most (action) supersolution) (steps : ℕ)
  → vector/at-most (iterate) supersolution
  where action := matrix/affine-action rows offset supersolution
  where iterate := matrix/affine-iterate rows offset steps supersolution

matrix/affine-iterate-invariant-interval :
  (rows : List (List ℚ)) (offset lower initial upper : List ℚ)
  (rows-positive : matrix/at-most (matrix/zero-like rows) rows)
  (lower-post-fixed : vector/at-most lower (matrix/affine-action rows offset lower))
  (upper-pre-fixed : vector/at-most (matrix/affine-action rows offset upper) upper)
  (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)