Reference · Matrices

rainbow.math.linear.matrix.affine-offset-sensitivity

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

Sensitivity of contractive affine fixed points to offset perturbations. If the same nonnegative matrix has row sums at most one half, fixed points of `b + A*x` and `c + A*y` satisfy d(x,y) <= 2 * d(b,c). The proof combines contraction in the value argument with exact translation invariance in the offset argument, then applies additive half cancellation. A practical NNRAT gamma <= 1/2 wrapper and a threshold certificate expose the result to solver/reward perturbation analyses. Native, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-residual-certificate

matrix/affine-half-row-offset-fixed-point-sensitivity :
  (rows : List (List ℚ)) (left-offset right-offset left right : List ℚ)
  (shape : vector/same-shape left right)
  (left-offset-shape : vector/same-shape left-offset (matrix/vector-multiply rows left))
  (right-offset-shape : vector/same-shape right-offset (matrix/vector-multiply rows 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 ≤ signed/from-nnrat nnrat/half)
  (left-fixed : vector/equivalent (action₂) left)
  (right-fixed : vector/equivalent (action) right)
  → vector/sup-distance left right ≤ distance + distance
  where action := matrix/affine-action rows right-offset right
  where action₂ := matrix/affine-action rows left-offset left
  where distance := vector/sup-distance left-offset right-offset

matrix/affine-nnrat-offset-fixed-point-sensitivity :
  (rows : List (List ℚ)) (left-offset right-offset left right : List ℚ) (gamma : ℚ≥0)
  (gamma-at-most-half : gamma ≤ nnrat/half)
  (shape : vector/same-shape left right)
  (left-offset-shape : vector/same-shape left-offset (matrix/vector-multiply rows left))
  (right-offset-shape : vector/same-shape right-offset (matrix/vector-multiply rows 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 ≤ signed/from-nnrat gamma)
  (left-fixed : vector/equivalent (action₂) left)
  (right-fixed : vector/equivalent (action) right)
  → vector/sup-distance left right ≤ distance + distance
  where action := matrix/affine-action rows right-offset right
  where action₂ := matrix/affine-action rows left-offset left
  where distance := vector/sup-distance left-offset right-offset

matrix/affine-nnrat-offset-threshold-sensitivity-certificate :
  (rows : List (List ℚ)) (left-offset right-offset left right : List ℚ) (gamma : ℚ≥0)
  (gamma-at-most-half : gamma ≤ nnrat/half)
  (shape : vector/same-shape left right)
  (left-offset-shape : vector/same-shape left-offset (matrix/vector-multiply rows left))
  (right-offset-shape : vector/same-shape right-offset (matrix/vector-multiply rows 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 ≤ signed/from-nnrat gamma)
  (left-fixed : vector/equivalent (action₁) left)
  (right-fixed : vector/equivalent (action) right) (threshold : ℚ)
  (offset-distance-bound : vector/sup-distance left-offset right-offset ≤ threshold)
  → vector/sup-distance left right ≤ threshold + threshold
  where action := matrix/affine-action rows right-offset right
  where action₁ := matrix/affine-action rows left-offset left