Reference · Matrices

rainbow.math.linear.matrix.affine-strong-row-contraction

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

User-facing contraction results for any NNRAT row bound gamma <= 1/2. Row sums are signed because matrix entries are signed, while practical discount/rate certificates are nonnegative rationals. The quotient-safe embedding sends `0 <= gamma <= 1/2` into signed order. Transitivity then turns actual-row bounds `sum(row) <= from-nnrat(gamma)` into the half-row premises required by the established uniqueness, finite-horizon rate, and rate-null convergence theorems. Native, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-half-iterate-converges

signed/zero-at-most-from-nnrat :
  (value : ℚ≥0)
  → 0 ≤ signed/from-nnrat value

matrix/nnrat-row-sums-imply-half-bound :
  (rows : List (List ℚ)) (gamma : ℚ≥0)
  (gamma-at-most-half : gamma ≤ nnrat/half)
  (bounded-sums : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) rows row), vector/sum row ≤ signed/from-nnrat gamma)
  (row : List ℚ) (member : list/membership (List ℚ) rows row)
  → vector/sum row ≤ signed/from-nnrat nnrat/half

matrix/affine-nnrat-strong-row-fixed-points-have-zero-sup-distance :
  (rows : List (List ℚ)) (offset left right : List ℚ) (gamma : ℚ≥0)
  (gamma-at-most-half : gamma ≤ nnrat/half)
  (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 gamma)
  (left-fixed : vector/equivalent (matrix/affine-action rows offset left) left)
  (right-fixed : vector/equivalent (matrix/affine-action rows offset right) right)
  → vector/sup-distance left right = 0

matrix/affine-nnrat-strong-row-fixed-points-unique :
  (rows : List (List ℚ)) (offset left right : List ℚ) (gamma : ℚ≥0)
  (gamma-at-most-half : gamma ≤ nnrat/half)
  (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 gamma)
  (left-fixed : vector/equivalent (matrix/affine-action rows offset left) left)
  (right-fixed : vector/equivalent (matrix/affine-action rows offset right) right)
  → vector/equivalent left right

matrix/affine-nnrat-strong-row-iterate-sup-distance-rate :
  (rows : List (List ℚ)) (offset left right : List ℚ) (gamma : ℚ≥0)
  (gamma-at-most-half : gamma ≤ nnrat/half)
  (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 gamma)
  (steps : ℕ)
  → vector/sup-distance (iterate₁) (iterate) ≤ signed/half-power-scale steps (vector/sup-distance left right)
  where iterate := matrix/affine-iterate rows offset steps right
  where iterate₁ := matrix/affine-iterate rows offset steps left

matrix/affine-nnrat-strong-row-iterate-sup-distance-rate-null :
  (rows : List (List ℚ)) (offset left right : List ℚ) (gamma : ℚ≥0)
  (gamma-at-most-half : gamma ≤ nnrat/half)
  (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 gamma)
  (initial-distance-at-most-one : vector/sup-distance left right ≤ 1)
  → analysis/signed-rate-null (fun n => vector/sup-distance (matrix/affine-iterate rows offset n left) (matrix/affine-iterate rows offset n right)) (fun k => k)

matrix/affine-nnrat-strong-row-iterate-converges-to-fixed-point :
  (rows : List (List ℚ)) (offset left fixed-point : List ℚ) (gamma : ℚ≥0)
  (gamma-at-most-half : gamma ≤ nnrat/half)
  (shape : vector/same-shape left fixed-point)
  (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 gamma)
  (initial-distance-at-most-one : vector/sup-distance left fixed-point ≤ 1)
  (fixed : vector/equivalent (action) fixed-point)
  → analysis/signed-rate-null (fun n => vector/sup-distance (matrix/affine-iterate rows offset n left) fixed-point) (fun k => k)
  where action := matrix/affine-action rows offset fixed-point