Reference · Matrices

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

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

A posteriori stability of approximate affine fixed points. For a half-contractive affine map F, two arbitrary candidates x and y obey d(x,y) <= 2 * (d(x,Fx) + d(y,Fy)). Unlike fixed-point uniqueness, this theorem needs no exact fixed point and is directly usable by independently implemented solvers: their computable residual certificates bound their disagreement. The practical theorem accepts an NNRAT row bound gamma <= 1/2 and separate residual thresholds. Theorem-only, kernel-checked, and axiom-free on D63.

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

matrix/affine-half-row-approximate-fixed-points-stable :
  (rows : List (List ℚ)) (offset left right : List ℚ)
  (shape : vector/same-shape left right)
  (left-residual-shape : vector/same-shape left (matrix/affine-action rows offset left))
  (right-residual-shape : vector/same-shape (matrix/affine-action rows offset right) 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 nnrat/half)
  → vector/sup-distance left right ≤ distance₁ + distance + (distance₁ + distance)
  where distance := vector/sup-distance (matrix/affine-action rows offset right) right
  where distance₁ := vector/sup-distance left (matrix/affine-action rows offset left)

matrix/affine-nnrat-approximate-fixed-points-stable :
  (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 (matrix/affine-action rows offset left))
  (right-residual-shape : vector/same-shape (matrix/affine-action rows offset right) 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)
  where distance := vector/sup-distance (matrix/affine-action rows offset right) right
  where distance₁ := vector/sup-distance left (matrix/affine-action rows offset left)

matrix/affine-nnrat-two-threshold-stability-certificate :
  (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 (matrix/affine-action rows offset left))
  (right-residual-shape : vector/same-shape (matrix/affine-action rows offset right) 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-threshold right-threshold : ℚ)
  (left-residual-bound : vector/sup-distance left (matrix/affine-action rows offset left) ≤ left-threshold)
  (right-residual-bound : vector/sup-distance (matrix/affine-action rows offset right) right ≤ right-threshold)
  → vector/sup-distance left right ≤ left-threshold + right-threshold + (left-threshold + right-threshold)