Reference · Matrices

rainbow.math.linear.matrix.affine-fixed-point-order

Matricessrc/rainbow/math/linear/matrix/affine_fixed_point_order.clj0 definitions, 2 theorems

Order bounds for finite signed affine iteration around a fixed point. For a nonnegative matrix, affine action is monotone in its value argument. Consequently every finite iterate that starts below a certified fixed point remains below it, and every iterate that starts above remains above it. Theorem-only, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-equivalence

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

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