Reference · Matrices

rainbow.math.linear.matrix.row-sum-lipschitz

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

Sup-Lipschitz bounds for nonnegative row-sum-bounded affine matrices. Premises quantify over the rows actually present in the matrix: every member row is componentwise nonnegative and has signed sum at most `rate`. The sharp row theorem bounds each dot-product distance by row mass times input sup distance; monotonic scaling replaces row mass by `rate`; the structural matrix lift takes the output maximum. Common-offset cancellation gives the affine theorem with the same rate. A later strict-rate certificate can use this as the contraction premise. Native, kernel-checked, and axiom-free on D63.

Depends onmath.linear.vector.row-sum-lipschitzmath.linear.matrix.action-sup-boundmath.linear.matrix.affine-sup-distancemath.rational.signed.multiply-monotonemath.rational.signed.multiply-ordermath.rational.signed.vector-sup-distance

matrix/vector-multiply-row-sum-lipschitz :
  (rows : List (List ℚ)) (left right : List ℚ) (rate : ℚ)
  (rate-nonnegative : 0 ≤ rate)
  (shape : vector/same-shape left right)
  (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 ≤ rate)
  → vector/sup-distance (matrix/vector-multiply rows left) (matrix/vector-multiply rows right) ≤ rate · vector/sup-distance left right

matrix/affine-action-row-sum-lipschitz :
  (rows : List (List ℚ)) (offset left right : List ℚ) (rate : ℚ)
  (rate-nonnegative : 0 ≤ rate)
  (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 ≤ rate)
  → vector/sup-distance (matrix/affine-action rows offset left) (matrix/affine-action rows offset right) ≤ rate · vector/sup-distance left right