Reference · Matrices

rainbow.math.linear.matrix.affine-approximate-offset-stability

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

Robust stability for approximate solutions under offset perturbation. For the same nonnegative contractive rows, let x approximately solve `x = b + A*x` and y approximately solve `y = c + A*y`. Then d(x,y) <= 2 * (d(x,b+A*x) + (d(b,c) + d(c+A*y,y))). Thus disagreement is controlled jointly by the two independently checkable solver residuals and the input/reward perturbation. The threshold theorem accepts a separate bound for each contribution. No exact fixed point is assumed. Native, kernel-checked, and axiom-free on D63.

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

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

matrix/affine-nnrat-approximate-offset-threshold-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-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 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-threshold offset-threshold right-threshold : ℚ)
  (left-residual-bound : vector/sup-distance left (action₁) ≤ left-threshold)
  (offset-distance-bound : vector/sup-distance left-offset right-offset ≤ offset-threshold)
  (right-residual-bound : vector/sup-distance (action) right ≤ right-threshold)
  → vector/sup-distance left right ≤ left-threshold + (offset-threshold + right-threshold) + (left-threshold + (offset-threshold + right-threshold))
  where action := matrix/affine-action rows right-offset right
  where action₁ := matrix/affine-action rows left-offset left