Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-signed-policy-sensitivity

Finite types, distributions and Markov chains src/rainbow/math/finite/bellman_signed_policy_sensitivity.clj0 definitions, 1 theorems

Robustness of signed fixed-policy Bellman evaluations under model drift. The reference discounted-transition matrix is a canonical rational contraction. The comparison matrix need not contract. Two possibly approximate value vectors are separated by their own Bellman residuals, signed reward-vector distance, and the transition-operator discrepancy at the comparison value. The sharp inverse-gap factor turns those independently checkable quantities into one value-function sensitivity certificate. This is a fixed-policy finite-matrix result, not signed Bellman optimality. Theorem-only, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-general-rate-sensitivity

bellman/signed-policy-problem-perturbation-stability

TheoremFor all inputsNo axiomsSource, line 111

bellman/signed-policy-problem-perturbation-stability :
  (left-rows right-rows : List (List ℚ)) (left-reward right-reward left right : List ℚ)
  (ap gp : ℕ) (shape : vector/same-shape left right)
  (left-residual-shape : vector/same-shape left (action₁))
  (right-residual-shape : vector/same-shape (action) right)
  (left-reward-shape : vector/same-shape left-reward (matrix/vector-multiply left-rows left))
  (right-reward-shape : vector/same-shape right-reward (matrix/vector-multiply right-rows right))
  (action-bridge-shape : vector/same-shape (matrix/vector-multiply left-rows right) (matrix/vector-multiply right-rows right))
  (positive-left-rows : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) left-rows row), vector/at-most (vector/zero-like row) row)
  (bounded-left-sums : ∀ (row : List ℚ), ∀ (member : list/membership (List ℚ) left-rows row), vector/sum row ≤ signed/from-nnrat (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))))
  → vector/sup-distance left right ≤ signed/from-nnrat (nnrat/make (add) gp) · (vector/sup-distance left (action₁) + (vector/sup-distance left-reward right-reward + vector/sup-distance (matrix/vector-multiply left-rows right) (matrix/vector-multiply right-rows right) + vector/sup-distance (action) right))
  where action := matrix/affine-action right-rows right-reward right
  where action₁ := matrix/affine-action left-rows left-reward left
  where add := algebra/nat-add (data/succ ap) (data/succ gp)

+ = signed/addList = data/List· = signed/multiplyℕ = data/Natℚ = signed/SignedRational≤ = signed/at-most