Reference · Matrices

rainbow.math.linear.matrix.affine-residual-certificate

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

A posteriori error certificates for contractive signed affine systems. A half contraction and the triangle inequality give d(x,x*) <= d(x,Fx) + 1/2 d(x,x*). Additive order cancellation then moves the half-distance to the left, proving `d(x,x*) <= 2 d(x,Fx)`. Thus a solver can certify its current error using the residual it can actually compute, without knowing the fixed point's value. The practical corollaries accept an NNRAT row bound gamma <= 1/2 and actual-row membership premises. Native, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-strong-row-contraction

signed/half-residual-bound :
  (distance residual : ℚ)
  (self-bound : distance ≤ residual + signed/from-nnrat nnrat/half · distance)
  → distance ≤ residual + residual

matrix/affine-half-row-fixed-point-residual-bound :
  (rows : List (List ℚ)) (offset approximate fixed-point : List ℚ)
  (shape : vector/same-shape approximate fixed-point)
  (offset-shape : vector/same-shape offset (matrix/vector-multiply rows approximate))
  (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)
  (fixed : vector/equivalent (action) fixed-point)
  → vector/sup-distance approximate fixed-point ≤ distance + distance
  where action := matrix/affine-action rows offset fixed-point
  where distance := vector/sup-distance approximate (matrix/affine-action rows offset approximate)

matrix/affine-nnrat-strong-row-fixed-point-residual-bound :
  (rows : List (List ℚ)) (offset approximate fixed-point : List ℚ) (gamma : ℚ≥0)
  (gamma-at-most-half : gamma ≤ nnrat/half)
  (shape : vector/same-shape approximate fixed-point)
  (offset-shape : vector/same-shape offset (matrix/vector-multiply rows approximate))
  (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)
  (fixed : vector/equivalent (action) fixed-point)
  → vector/sup-distance approximate fixed-point ≤ distance + distance
  where action := matrix/affine-action rows offset fixed-point
  where distance := vector/sup-distance approximate (matrix/affine-action rows offset approximate)

matrix/affine-nnrat-strong-row-stopping-certificate :
  (rows : List (List ℚ)) (offset approximate fixed-point : List ℚ) (gamma : ℚ≥0)
  (gamma-at-most-half : gamma ≤ nnrat/half)
  (shape : vector/same-shape approximate fixed-point)
  (offset-shape : vector/same-shape offset (matrix/vector-multiply rows approximate))
  (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)
  (fixed : vector/equivalent (action) fixed-point) (threshold : ℚ)
  (residual-at-most-threshold : vector/sup-distance approximate (action₁) ≤ threshold)
  → vector/sup-distance approximate fixed-point ≤ threshold + threshold
  where action := matrix/affine-action rows offset fixed-point
  where action₁ := matrix/affine-action rows offset approximate