Reference · Matrices

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

Matricessrc/rainbow/math/linear/matrix/affine_general_rate_certificate.clj0 definitions, 7 theorems

Sharp affine residual certificates for every canonical rational rate below one. For `a = ap+1` and `g = gp+1`, the existing arbitrary-rate contraction development represents gamma = a/(a+g). This module constructs quotient-safe witnesses for gap = g/(a+g), gamma + gap ~ 1 inverse = (a+g)/g, inverse * gap ~ 1, transports them through `signed/from-nnrat`, and instantiates the generic inverse-gap residual theorem. Consequently an affine solver whose row sums are bounded by gamma gets the sharp a-posteriori certificate d(x,x*) <= ((a+g)/g) * d(x,Fx) for every rational contraction rate below one, without the former `gamma <= 1/2` restriction and without caller-supplied quotient identities. Theorem-only, kernel-checked, and axiom-free on D63.

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

nnrat/general-rate-plus-gap :
  (ap gp : ℕ)
  → nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp)) + nnrat/make (data/succ gp) (algebra/nat-add ap (data/succ gp)) = 1

nnrat/general-inverse-times-gap :
  (ap gp : ℕ)
  → nnrat/make (add) gp · nnrat/make (data/succ gp) (algebra/nat-add ap (data/succ gp)) = 1
  where add := algebra/nat-add (data/succ ap) (data/succ gp)

signed/from-nnrat-add :
  (left right : ℚ≥0)
  → signed/from-nnrat left + signed/from-nnrat right = signed/from-nnrat (left + right)

signed/general-rate-plus-gap-one :
  (ap gp : ℕ)
  → signed/from-nnrat (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))) + signed/from-nnrat (nnrat/make (data/succ gp) (algebra/nat-add ap (data/succ gp))) = 1

signed/general-inverse-times-gap-one :
  (ap gp : ℕ)
  → signed/from-nnrat (nnrat/make (add) gp) · signed/from-nnrat (nnrat/make (data/succ gp) (algebra/nat-add ap (data/succ gp))) = 1
  where add := algebra/nat-add (data/succ ap) (data/succ gp)

matrix/affine-general-rate-fixed-point-residual-bound :
  (rows : List (List ℚ)) (offset approximate fixed-point : List ℚ) (ap gp : ℕ)
  (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/make (data/succ ap) (algebra/nat-add ap (data/succ gp))))
  (fixed : vector/equivalent (action) fixed-point)
  → vector/sup-distance approximate fixed-point ≤ signed/from-nnrat (nnrat/make (add) gp) · vector/sup-distance approximate (action₂)
  where action := matrix/affine-action rows offset fixed-point
  where action₂ := matrix/affine-action rows offset approximate
  where add := algebra/nat-add (data/succ ap) (data/succ gp)

matrix/affine-general-rate-stopping-certificate :
  (rows : List (List ℚ)) (offset approximate fixed-point : List ℚ) (ap gp : ℕ)
  (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/make (data/succ ap) (algebra/nat-add ap (data/succ gp))))
  (fixed : vector/equivalent (action) fixed-point) (threshold : ℚ)
  (residual-at-most-threshold : vector/sup-distance approximate (action₂) ≤ threshold)
  → vector/sup-distance approximate fixed-point ≤ signed/from-nnrat (nnrat/make (add) gp) · threshold
  where action := matrix/affine-action rows offset fixed-point
  where action₂ := matrix/affine-action rows offset approximate
  where add := algebra/nat-add (data/succ ap) (data/succ gp)