Reference · Matrices

rainbow.math.linear.matrix.affine-half-iterate-contraction

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

Shape preservation and one-step contraction for half-row affine iteration. Matrix action output length depends only on the row count. Consequently two affine images have the same shape whenever the offset fits one reference action, and equal-shaped initial states remain equal-shaped through every finite iterate. The concrete half-row Lipschitz theorem can therefore be applied at every horizon, proving that successive paired iterates halve their signed sup distance. Native, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.half-row-sum-fixed-point-uniqueness

matrix/affine-action-output-shape :
  (rows : List (List ℚ)) (offset left right : List ℚ)
  (offset-shape : vector/same-shape offset (matrix/vector-multiply rows left))
  → vector/same-shape (matrix/affine-action rows offset left) (matrix/affine-action rows offset right)

matrix/affine-iterate-output-shape :
  (rows : List (List ℚ)) (offset left right : List ℚ)
  (initial-shape : vector/same-shape left right)
  (offset-shape : vector/same-shape offset (matrix/vector-multiply rows left))
  (steps : ℕ)
  → vector/same-shape (iterate₁) (iterate)
  where iterate := matrix/affine-iterate rows offset steps right
  where iterate₁ := matrix/affine-iterate rows offset steps left

matrix/affine-half-iterate-sup-distance-step :
  (rows : List (List ℚ)) (offset left right : List ℚ)
  (initial-shape : vector/same-shape left right)
  (offset-shape : vector/same-shape offset (matrix/vector-multiply rows left))
  (positive-rows : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) rows row), vector/at-most (vector/zero-like row) row)
  (bounded-sums : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) rows row), vector/sum row ≤ signed/from-nnrat nnrat/half)
  (steps : ℕ)
  → vector/sup-distance (iterate₁) (iterate) ≤ signed/from-nnrat nnrat/half · vector/sup-distance (iterate₃) (iterate₂)
  where iterate := matrix/affine-iterate rows offset (data/succ steps) right
  where iterate₁ := matrix/affine-iterate rows offset (data/succ steps) left
  where iterate₂ := matrix/affine-iterate rows offset steps right
  where iterate₃ := matrix/affine-iterate rows offset steps left