Reference · Matrices

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

Matrices src/rainbow/math/linear/matrix/affine_residual_bracket.clj0 definitions, 1 theorems

Nested finite-horizon affine brackets from linear residual certificates. A lower residual upper-bound and upper residual lower-bound, together with nonnegative rows and an initial lower/upper order, produce the full nested certificate `L_base <= L_(extra+base) <= U_(extra+base) <= U_base`. This is the exact finite bounded-value-iteration enclosure used to tighten lower and upper Bellman certificates. Theorem-only, kernel-checked, and axiom-free on D63.

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

matrix/affine-iterate-residual-nested-bracket

TheoremFor all inputsNo axiomsSource, line 47

matrix/affine-iterate-residual-nested-bracket :
  (rows : List (List ℚ)) (offset lower upper : List ℚ)
  (rows-positive : matrix/at-most (matrix/zero-like rows) rows)
  (lower-image-shape : vector/same-shape lower (matrix/vector-multiply rows lower))
  (upper-image-shape : vector/same-shape upper (matrix/vector-multiply rows upper))
  (lower-residual-upper : vector/at-most (subtract) offset)
  (upper-residual-lower : vector/at-most offset (subtract₃))
  (lower-upper : vector/at-most lower upper) (base extra : ℕ)
  → proposition/conjunction (most) (conjunction)
  where conjunction := proposition/conjunction (vector/at-most (matrix/affine-iterate rows offset (algebra/nat-add extra base) lower) (matrix/affine-iterate rows offset (algebra/nat-add extra base) upper)) (vector/at-most (matrix/affine-iterate rows offset (algebra/nat-add extra base) upper) (matrix/affine-iterate rows offset base upper))
  where most := vector/at-most (matrix/affine-iterate rows offset base lower) (matrix/affine-iterate rows offset (algebra/nat-add extra base) lower)
  where subtract := vector/subtract lower (matrix/vector-multiply rows lower)
  where subtract₃ := vector/subtract upper (matrix/vector-multiply rows upper)

List = data/Listℕ = data/Natℚ = signed/SignedRational