Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-signed-policy

Finite types, distributions and Markov chainssrc/rainbow/math/finite/bellman_signed_policy.clj2 definitions, 9 theorems

Signed-reward fixed-policy Bellman certificates in finite matrix form. A fixed policy over an explicitly enumerated state vector has the affine Bellman step `T(v) = reward + discounted-transition * v`. The reward vector is fully signed. Because the same reward occurs in both images, it cancels from sup distance; nonnegative transition rows with a canonical rational row-sum bound below one therefore give contraction, a sharp residual certificate, and fixed-point uniqueness. This bridges the signed affine development to Bellman policy evaluation. It does not cover max-over-actions Bellman optimality, fixed-point existence, or an executable solver. Theorem-only, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-general-rate-uniquenessmath.linear.matrix.affine-general-rate-tail-certificate

bellman/signed-policy-step :
  (x₁ : List (List ℚ)) (x₂ x₃ : List ℚ)
  → List ℚ

bellman/signed-policy-iterate :
  (x₁ : List (List ℚ)) (x₂ : List ℚ) (x₃ : ℕ) (x₄ : List ℚ)
  → List ℚ

bellman/signed-policy-step-reward-cancels-distance :
  (rows : List (List ℚ)) (reward left right : List ℚ)
  (reward-shape : vector/same-shape reward (matrix/vector-multiply rows left))
  → vector/sup-distance (step₁) (step) = vector/sup-distance (matrix/vector-multiply rows left) (matrix/vector-multiply rows right)
  where step := bellman/signed-policy-step rows reward right
  where step₁ := bellman/signed-policy-step rows reward left

bellman/signed-policy-step-general-rate-contraction :
  (rows : List (List ℚ)) (reward left right : List ℚ) (ap gp : ℕ)
  (shape : vector/same-shape left right)
  (reward-shape : vector/same-shape reward (matrix/vector-multiply rows left))
  (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 (make))
  → vector/sup-distance (step₂) (step) ≤ signed/from-nnrat (make) · vector/sup-distance left right
  where make := nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))
  where step := bellman/signed-policy-step rows reward right
  where step₂ := bellman/signed-policy-step rows reward left

bellman/signed-policy-fixed-points-unique :
  (rows : List (List ℚ)) (reward left right : List ℚ) (ap gp : ℕ)
  (shape : vector/same-shape left right)
  (reward-shape : vector/same-shape reward (matrix/vector-multiply rows left))
  (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))))
  (left-fixed : vector/equivalent (step₁) left)
  (right-fixed : vector/equivalent (step) right)
  → vector/equivalent left right
  where step := bellman/signed-policy-step rows reward right
  where step₁ := bellman/signed-policy-step rows reward left

bellman/signed-policy-fixed-point-residual-bound :
  (rows : List (List ℚ)) (reward approximate fixed-point : List ℚ) (ap gp : ℕ)
  (shape : vector/same-shape approximate fixed-point)
  (reward-shape : vector/same-shape reward (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 (step) fixed-point)
  → vector/sup-distance approximate fixed-point ≤ signed/from-nnrat (nnrat/make (add) gp) · vector/sup-distance approximate (step₁)
  where add := algebra/nat-add (data/succ ap) (data/succ gp)
  where step := bellman/signed-policy-step rows reward fixed-point
  where step₁ := bellman/signed-policy-step rows reward approximate

bellman/signed-policy-fixed-point-stopping-certificate :
  (rows : List (List ℚ)) (reward approximate fixed-point : List ℚ) (ap gp : ℕ)
  (shape : vector/same-shape approximate fixed-point)
  (reward-shape : vector/same-shape reward (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 (step) fixed-point) (threshold : ℚ)
  (residual-at-most-threshold : vector/sup-distance approximate (step₁) ≤ threshold)
  → vector/sup-distance approximate fixed-point ≤ signed/from-nnrat (nnrat/make (add) gp) · threshold
  where add := algebra/nat-add (data/succ ap) (data/succ gp)
  where step := bellman/signed-policy-step rows reward fixed-point
  where step₁ := bellman/signed-policy-step rows reward approximate

bellman/signed-policy-iterate-error-exact-envelope :
  (rows : List (List ℚ)) (reward approximate fixed-point : List ℚ) (ap gp : ℕ)
  (shape : vector/same-shape approximate fixed-point)
  (reward-shape : vector/same-shape reward (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 (make))
  (fixed : vector/equivalent (step) fixed-point) (steps : ℕ)
  → vector/sup-distance (iterate) fixed-point ≤ signed/from-nnrat (nnrat/make (add) gp) · signed/nnrat-power-scale (make) steps (distance)
  where add := algebra/nat-add (data/succ ap) (data/succ gp)
  where distance := vector/sup-distance approximate (bellman/signed-policy-step rows reward approximate)
  where iterate := bellman/signed-policy-iterate rows reward steps approximate
  where make := nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))
  where step := bellman/signed-policy-step rows reward fixed-point

bellman/signed-policy-iterate-stopping-certificate :
  (rows : List (List ℚ)) (reward approximate fixed-point : List ℚ) (ap gp : ℕ)
  (shape : vector/same-shape approximate fixed-point)
  (reward-shape : vector/same-shape reward (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 (make))
  (fixed : vector/equivalent (step) fixed-point) (steps : ℕ) (threshold : ℚ)
  (envelope-at-most-threshold : signed/from-nnrat (nnrat/make (add) gp) · signed/nnrat-power-scale (make) steps (distance) ≤ threshold)
  → vector/sup-distance (iterate) fixed-point ≤ threshold
  where add := algebra/nat-add (data/succ ap) (data/succ gp)
  where distance := vector/sup-distance approximate (bellman/signed-policy-step rows reward approximate)
  where iterate := bellman/signed-policy-iterate rows reward steps approximate
  where make := nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))
  where step := bellman/signed-policy-step rows reward fixed-point

bellman/signed-policy-iterate-tail-bound :
  (rows : List (List ℚ)) (reward initial : List ℚ) (ap gp : ℕ)
  (step-shape : vector/same-shape initial (bellman/signed-policy-step rows reward initial))
  (reward-shape : vector/same-shape reward (matrix/vector-multiply rows initial))
  (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 (make))
  (left-steps right-steps : ℕ)
  → vector/sup-distance (iterate₃) (iterate) ≤ signed/from-nnrat (nnrat/make (add) gp) · (signed/nnrat-power-scale (make) left-steps (distance) + signed/nnrat-power-scale (make) right-steps (distance))
  where add := algebra/nat-add (data/succ ap) (data/succ gp)
  where distance := vector/sup-distance initial (bellman/signed-policy-step rows reward initial)
  where iterate := bellman/signed-policy-iterate rows reward right-steps initial
  where iterate₃ := bellman/signed-policy-iterate rows reward left-steps initial
  where make := nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))

bellman/signed-policy-iterate-tail-stopping-certificate :
  (rows : List (List ℚ)) (reward initial : List ℚ) (ap gp : ℕ)
  (step-shape : vector/same-shape initial (bellman/signed-policy-step rows reward initial))
  (reward-shape : vector/same-shape reward (matrix/vector-multiply rows initial))
  (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 (make))
  (left-steps right-steps : ℕ) (threshold : ℚ)
  (tail-envelope-at-most-threshold : signed/from-nnrat (nnrat/make (add) gp) · (signed/nnrat-power-scale (make) left-steps (distance) + signed/nnrat-power-scale (make) right-steps (distance)) ≤ threshold)
  → vector/sup-distance (iterate₃) (iterate) ≤ threshold
  where add := algebra/nat-add (data/succ ap) (data/succ gp)
  where distance := vector/sup-distance initial (bellman/signed-policy-step rows reward initial)
  where iterate := bellman/signed-policy-iterate rows reward right-steps initial
  where iterate₃ := bellman/signed-policy-iterate rows reward left-steps initial
  where make := nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))