Reference · Matrices

rainbow.math.linear.matrix.affine-inverse-gap-certificate

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

Sharp residual certificates for arbitrary strict contraction rates. The scalar theorem abstracts the exact algebra needed beyond the special half-rate case. If `rate + gap ~ 1`, `inverse * gap ~ 1`, inverse is nonnegative, and distance <= residual + rate*distance, then `distance <= inverse*residual`. Affine matrix theorems derive that self-bound from row-sum Lipschitz contraction and expose a stopping certificate. Instantiating inverse with `(1-rate)^-1` gives the sharp a-posteriori factor for any rational rate below one. Theorem-only, kernel-checked, and axiom-free on D63.

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

signed/inverse-gap-residual-bound :
  (distance residual rate gap inverse : ℚ)
  (inverse-nonnegative : 0 ≤ inverse)
  (rate-plus-gap-one : rate + gap = 1)
  (inverse-times-gap-one : inverse · gap = 1)
  (self-bound : distance ≤ residual + rate · distance)
  → distance ≤ inverse · residual

matrix/affine-inverse-gap-fixed-point-residual-bound :
  (rows : List (List ℚ)) (offset approximate fixed-point : List ℚ)
  (rate gap inverse : ℚ)
  (rate-nonnegative : 0 ≤ rate)
  (inverse-nonnegative : 0 ≤ inverse)
  (rate-plus-gap-one : rate + gap = 1)
  (inverse-times-gap-one : inverse · gap = 1)
  (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 ≤ rate)
  (fixed : vector/equivalent (action) fixed-point)
  → vector/sup-distance approximate fixed-point ≤ inverse · vector/sup-distance approximate (action₁)
  where action := matrix/affine-action rows offset fixed-point
  where action₁ := matrix/affine-action rows offset approximate

matrix/affine-inverse-gap-stopping-certificate :
  (rows : List (List ℚ)) (offset approximate fixed-point : List ℚ)
  (rate gap inverse : ℚ)
  (rate-nonnegative : 0 ≤ rate)
  (inverse-nonnegative : 0 ≤ inverse)
  (rate-plus-gap-one : rate + gap = 1)
  (inverse-times-gap-one : inverse · gap = 1)
  (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 ≤ rate)
  (fixed : vector/equivalent (action) fixed-point) (threshold : ℚ)
  (residual-at-most-threshold : vector/sup-distance approximate (action₁) ≤ threshold)
  → vector/sup-distance approximate fixed-point ≤ inverse · threshold
  where action := matrix/affine-action rows offset fixed-point
  where action₁ := matrix/affine-action rows offset approximate