Reference · Matrices

rainbow.math.linear.matrix.affine-equivalence

Matricessrc/rainbow/math/linear/matrix/affine_equivalence.clj0 definitions, 7 theorems

Congruence and fixed-point invariance for signed affine value iteration. Affine action respects matrix, reward-offset, and value equivalence separately and jointly. Nat induction lifts congruence to every finite iterate and shows that an affine fixed point remains equivalent to itself after any number of iterations. Theorem-only, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-iterate

matrix/affine-action-respects-offset-equivalence :
  (rows : List (List ℚ)) (left right values : List ℚ)
  (same : vector/equivalent left right)
  → vector/equivalent (matrix/affine-action rows left values) (matrix/affine-action rows right values)

matrix/affine-action-respects-values-equivalence :
  (rows : List (List ℚ)) (offset left right : List ℚ)
  (same : vector/equivalent left right)
  → vector/equivalent (matrix/affine-action rows offset left) (matrix/affine-action rows offset right)

matrix/affine-action-respects-rows-equivalence :
  (left right : List (List ℚ)) (offset values : List ℚ)
  (same : matrix/equivalent left right)
  → vector/equivalent (matrix/affine-action left offset values) (action)
  where action := matrix/affine-action right offset values

matrix/affine-action-respects-equivalence :
  (left-rows right-rows : List (List ℚ))
  (left-offset right-offset left-values right-values : List ℚ)
  (rows-same : matrix/equivalent left-rows right-rows)
  (offset-same : vector/equivalent left-offset right-offset)
  (values-same : vector/equivalent left-values right-values)
  → vector/equivalent (action₁) (action)
  where action := matrix/affine-action right-rows right-offset right-values
  where action₁ := matrix/affine-action left-rows left-offset left-values

matrix/affine-iterate-respects-initial-equivalence :
  (rows : List (List ℚ)) (offset left right : List ℚ)
  (same : vector/equivalent left right) (steps : ℕ)
  → vector/equivalent (iterate₁) (iterate)
  where iterate := matrix/affine-iterate rows offset steps right
  where iterate₁ := matrix/affine-iterate rows offset steps left

matrix/affine-iterate-respects-equivalence :
  (left-rows right-rows : List (List ℚ))
  (left-offset right-offset left-initial right-initial : List ℚ)
  (rows-same : matrix/equivalent left-rows right-rows)
  (offset-same : vector/equivalent left-offset right-offset)
  (initial-same : vector/equivalent left-initial right-initial) (steps : ℕ)
  → vector/equivalent (iterate₁) (iterate)
  where iterate := matrix/affine-iterate right-rows right-offset steps right-initial
  where iterate₁ := matrix/affine-iterate left-rows left-offset steps left-initial

matrix/affine-iterate-fixed-point :
  (rows : List (List ℚ)) (offset value : List ℚ)
  (fixed : vector/equivalent (matrix/affine-action rows offset value) value) (steps : ℕ)
  → vector/equivalent (iterate) value
  where iterate := matrix/affine-iterate rows offset steps value