Reference · Matrices

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

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

Approximate-solution stability across certified affine-map perturbations. A reusable bridge theorem compares an approximate solution x of a contractive affine map F with a point y certified against any comparison image G(y). A bound on d(F(y),G(y)) converts the comparison certificate into an F-residual and yields d(x,y) <= 2 * (residual-x + (bridge + residual-y)). The row-perturbation specialization takes F(y)=b+A*y and G(y)=b+B*y, reducing the bridge exactly to d(A*y,B*y). This covers transition/model drift while requiring contraction only of the reference rows A. No exact fixed point is assumed. Native, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-approximate-stability

matrix/affine-nnrat-bridged-approximate-threshold-certificate :
  (rows : List (List ℚ)) (offset left right comparison-image : List ℚ) (gamma : ℚ≥0)
  (gamma-at-most-half : gamma ≤ nnrat/half)
  (shape : vector/same-shape left right)
  (left-residual-shape : vector/same-shape left (matrix/affine-action rows offset left))
  (bridge-shape : vector/same-shape (matrix/affine-action rows offset right) comparison-image)
  (comparison-residual-shape : vector/same-shape comparison-image 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-residual-threshold bridge-threshold comparison-residual-threshold : ℚ)
  (left-residual-bound : vector/sup-distance left (matrix/affine-action rows offset left) ≤ left-residual-threshold)
  (bridge-bound : vector/sup-distance (matrix/affine-action rows offset right) comparison-image ≤ bridge-threshold)
  (comparison-residual-bound : vector/sup-distance comparison-image right ≤ comparison-residual-threshold)
  → vector/sup-distance left right ≤ left-residual-threshold + (bridge-threshold + comparison-residual-threshold) + (left-residual-threshold + (bridge-threshold + comparison-residual-threshold))

matrix/affine-nnrat-bridged-approximate-stability :
  (rows : List (List ℚ)) (offset left right comparison-image : List ℚ) (gamma : ℚ≥0)
  (gamma-at-most-half : gamma ≤ nnrat/half)
  (shape : vector/same-shape left right)
  (left-residual-shape : vector/same-shape left (matrix/affine-action rows offset left))
  (bridge-shape : vector/same-shape (matrix/affine-action rows offset right) comparison-image)
  (comparison-residual-shape : vector/same-shape comparison-image 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)
  → vector/sup-distance left right ≤ distance₁ + (distance + distance₂) + (distance₁ + (distance + distance₂))
  where distance := vector/sup-distance (matrix/affine-action rows offset right) comparison-image
  where distance₁ := vector/sup-distance left (matrix/affine-action rows offset left)
  where distance₂ := vector/sup-distance comparison-image right

matrix/affine-nnrat-row-perturbation-threshold-certificate :
  (left-rows right-rows : List (List ℚ)) (offset left right : List ℚ) (gamma : ℚ≥0)
  (gamma-at-most-half : gamma ≤ nnrat/half)
  (shape : vector/same-shape left right)
  (left-residual-shape : vector/same-shape left (action₁))
  (right-residual-shape : vector/same-shape (action) right)
  (left-offset-shape : vector/same-shape offset (matrix/vector-multiply left-rows left))
  (right-offset-shape : vector/same-shape offset (matrix/vector-multiply right-rows right))
  (positive-left-rows : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) left-rows row), vector/at-most (vector/zero-like row) row)
  (bounded-left-sums : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) left-rows row), vector/sum row ≤ signed/from-nnrat gamma)
  (left-residual-threshold operator-threshold right-residual-threshold : ℚ)
  (left-residual-bound : vector/sup-distance left (action₁) ≤ left-residual-threshold)
  (operator-bound : vector/sup-distance (matrix/vector-multiply left-rows right) (matrix/vector-multiply right-rows right) ≤ operator-threshold)
  (right-residual-bound : vector/sup-distance (action) right ≤ right-residual-threshold)
  → vector/sup-distance left right ≤ left-residual-threshold + (operator-threshold + right-residual-threshold) + (left-residual-threshold + (operator-threshold + right-residual-threshold))
  where action := matrix/affine-action right-rows offset right
  where action₁ := matrix/affine-action left-rows offset left