Reference · Matrices

rainbow.math.linear.matrix.affine-general-rate-sensitivity

Matricessrc/rainbow/math/linear/matrix/affine_general_rate_sensitivity.clj0 definitions, 4 theorems

Sharp robustness certificates for arbitrary-rate affine problem drift. Let the reference rows A have canonical rational contraction rate `a/(a+g)`, where `a=ap+1` and `g=gp+1`. This module specializes bridged inverse-gap stability to two independently checkable perturbation models: * operator drift, comparing `b+A*x` with `b+B*y`; * full drift, comparing `b+A*x` with `c+B*y`. The resulting factor is the sharp `(a+g)/g`, not the half-rate-only factor two. The comparison rows B need not contract and neither candidate must be an exact fixed point. Exact-distance and separate-threshold forms are theorem-only, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-inverse-gap-stability

matrix/affine-general-rate-row-perturbation-threshold-certificate :
  (left-rows right-rows : List (List ℚ)) (offset left right : List ℚ) (ap gp : ℕ)
  (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 (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))))
  (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 ≤ signed/from-nnrat (nnrat/make (add) gp) · (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
  where add := algebra/nat-add (data/succ ap) (data/succ gp)

matrix/affine-general-rate-row-perturbation-stability :
  (left-rows right-rows : List (List ℚ)) (offset left right : List ℚ) (ap gp : ℕ)
  (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 (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))))
  → vector/sup-distance left right ≤ signed/from-nnrat (nnrat/make (add) gp) · (vector/sup-distance left (action₂) + (vector/sup-distance (matrix/vector-multiply left-rows right) (matrix/vector-multiply right-rows right) + vector/sup-distance (action) right))
  where action := matrix/affine-action right-rows offset right
  where action₂ := matrix/affine-action left-rows offset left
  where add := algebra/nat-add (data/succ ap) (data/succ gp)

matrix/affine-general-rate-problem-perturbation-threshold-certificate :
  (left-rows right-rows : List (List ℚ)) (left-offset right-offset left right : List ℚ)
  (ap gp : ℕ) (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 (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))))
  (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 ≤ signed/from-nnrat (nnrat/make (add) gp) · (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
  where add := algebra/nat-add (data/succ ap) (data/succ gp)

matrix/affine-general-rate-problem-perturbation-stability :
  (left-rows right-rows : List (List ℚ)) (left-offset right-offset left right : List ℚ)
  (ap gp : ℕ) (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 (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))))
  → vector/sup-distance left right ≤ signed/from-nnrat (nnrat/make (add) gp) · (vector/sup-distance left (action₁) + (vector/sup-distance left-offset right-offset + vector/sup-distance (matrix/vector-multiply left-rows right) (matrix/vector-multiply right-rows right) + vector/sup-distance (action) right))
  where action := matrix/affine-action right-rows right-offset right
  where action₁ := matrix/affine-action left-rows left-offset left
  where add := algebra/nat-add (data/succ ap) (data/succ gp)