Reference · Matrices

rainbow.math.linear.matrix.affine-iterate

Matricessrc/rainbow/math/linear/matrix/affine_iterate.clj1 definitions, 5 theorems

Finite signed value iteration for affine matrix maps. `matrix/affine-iterate` repeatedly applies `offset + rows·value`. Its native Nat recursor equations, nonnegative-cone invariant, monotonicity in the initial value, and simultaneous data/initial monotonicity are ordinary proof data. The all-parameter theorem carries the exact source/destination cone premises required at every induction step. Native and axiom-free on D63.

Depends onmath.linear.matrix.affine-sign

matrix/affine-iterate :
  (x₁ : List (List ℚ)) (x₂ : List ℚ) (x₃ : ℕ) (x₄ : List ℚ)
  → List ℚ

matrix/affine-iterate-zero :
  (rows : List (List ℚ)) (offset initial : List ℚ)
  → vector/equivalent (iterate) initial
  where iterate := matrix/affine-iterate rows offset 0 initial

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

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

matrix/affine-iterate-monotone-initial :
  (rows : List (List ℚ)) (offset left right : List ℚ)
  (rows-positive : matrix/at-most (matrix/zero-like rows) rows)
  (ordered : vector/at-most left right) (steps : ℕ)
  → vector/at-most (iterate₁) (iterate)
  where iterate := matrix/affine-iterate rows offset steps right
  where iterate₁ := matrix/affine-iterate rows offset steps left

matrix/affine-iterate-monotone-all :
  (source-rows destination-rows : List (List ℚ))
  (source-offset destination-offset source-initial destination-initial : List ℚ)
  (source-rows-positive : matrix/at-most (matrix/zero-like source-rows) source-rows)
  (destination-rows-positive : matrix/at-most (matrix/zero-like destination-rows) destination-rows)
  (source-offset-positive : vector/at-most (vector/zero-like source-offset) source-offset)
  (source-initial-positive : vector/at-most (vector/zero-like source-initial) source-initial)
  (rows-ordered : matrix/at-most source-rows destination-rows)
  (offset-ordered : vector/at-most source-offset destination-offset)
  (initial-ordered : vector/at-most source-initial destination-initial) (steps : ℕ)
  → vector/at-most (iterate₁) (iterate)
  where iterate := matrix/affine-iterate destination-rows destination-offset steps destination-initial
  where iterate₁ := matrix/affine-iterate source-rows source-offset steps source-initial