Reference · Matrices

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

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

End-to-end robustness for approximate affine optimization problems. Compare x certified for `b + A*x` with y certified for `c + B*y`. If A is contractive, the total disagreement is bounded by twice the sum of four independently checkable quantities: x's residual, offset/reward drift, operator/transition drift at y, and y's residual. d(x,y) <= 2 * (r_x + ((d(b,c) + d(A*y,B*y)) + r_y)). No contraction premise is imposed on B and no exact fixed point is assumed. The exact-distance theorem and separate four-threshold certificate are theorem-only, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-operator-sensitivity

matrix/affine-nnrat-problem-perturbation-threshold-certificate :
  (left-rows right-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-residual-shape : vector/same-shape left (action₁))
  (right-residual-shape : vector/same-shape (action) right)
  (left-offset-shape : vector/same-shape left-offset (matrix/vector-multiply left-rows left))
  (right-offset-shape : vector/same-shape right-offset (matrix/vector-multiply right-rows right))
  (action-bridge-shape : vector/same-shape (matrix/vector-multiply left-rows right) (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 offset-threshold operator-threshold right-residual-threshold : ℚ)
  (left-residual-bound : vector/sup-distance left (action₁) ≤ left-residual-threshold)
  (offset-bound : vector/sup-distance left-offset right-offset ≤ offset-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 + (offset-threshold + operator-threshold + right-residual-threshold) + (left-residual-threshold + (offset-threshold + operator-threshold + right-residual-threshold))
  where action := matrix/affine-action right-rows right-offset right
  where action₁ := matrix/affine-action left-rows left-offset left

matrix/affine-nnrat-problem-perturbation-stability :
  (left-rows right-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-residual-shape : vector/same-shape left (matrix/affine-action left-rows left-offset left))
  (right-residual-shape : vector/same-shape (matrix/affine-action right-rows right-offset right) right)
  (left-offset-shape : vector/same-shape left-offset (matrix/vector-multiply left-rows left))
  (right-offset-shape : vector/same-shape right-offset (matrix/vector-multiply right-rows right))
  (action-bridge-shape : vector/same-shape (matrix/vector-multiply left-rows right) (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)
  → vector/sup-distance left right ≤ distance₂ + (distance₃ + distance + distance₁) + (distance₂ + (distance₃ + distance + distance₁))
  where distance := vector/sup-distance (matrix/vector-multiply left-rows right) (matrix/vector-multiply right-rows right)
  where distance₁ := vector/sup-distance (matrix/affine-action right-rows right-offset right) right
  where distance₂ := vector/sup-distance left (matrix/affine-action left-rows left-offset left)
  where distance₃ := vector/sup-distance left-offset right-offset