Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-signed-action-backup

Finite types, distributions and Markov chainssrc/rainbow/math/finite/bellman_signed_action_backup.clj1 definitions, 3 theorems

Concrete signed Bellman action backups and their additive contraction. The backup is reward + discount * expectation over a finite state carrier. Rewards and values may be arbitrary exact signed rationals. Transition weights and discount are signed rationals with explicit nonnegativity; each transition row carries explicit total-mass-one evidence. A normalized row transports two-sided pointwise epsilon-closeness to discount*epsilon-closeness of the corresponding action backups. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.signed-expectation

bellman/signed-action-backup.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (transition : S → A → S → ℚ)
  (reward : S → A → ℚ) (discount : ℚ) (value : S → ℚ) (x₁ : S) (x₂ : A)
  → ℚ

bellman/signed-action-backup-unfold.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (transition : S → A → S → ℚ)
  (reward : S → A → ℚ) (discount : ℚ) (value : S → ℚ) (state : S) (action : A)
  → bellman/signed-action-backup S A states transition reward discount value state action = reward state action + discount · probability/signed-expectation S states (transition state action) value

bellman/signed-action-backup-additive-upper-bound.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (transition : S → A → S → ℚ)
  (reward : S → A → ℚ) (discount : ℚ)
  (discount-nonnegative : 0 ≤ discount)
  (left-value right-value : S → ℚ) (epsilon : ℚ)
  (left-pointwise : ∀ (next-state : S), left-value next-state ≤ right-value next-state + epsilon)
  (state : S) (action : A)
  (row-nonnegative : ∀ (next-state : S), 0 ≤ transition state action next-state)
  (row-normalized : probability/signed-total-mass S states (transition state action) = 1)
  → backup left-value state action ≤ backup right-value state action + discount · epsilon
  where backup := bellman/signed-action-backup S A states transition reward discount

bellman/signed-action-backup-additively-contractive.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (transition : S → A → S → ℚ)
  (reward : S → A → ℚ) (discount : ℚ)
  (discount-nonnegative : 0 ≤ discount)
  (left-value right-value : S → ℚ) (epsilon : ℚ)
  (left-pointwise : ∀ (next-state : S), left-value next-state ≤ right-value next-state + epsilon)
  (right-pointwise : ∀ (next-state : S), right-value next-state ≤ left-value next-state + epsilon)
  (state : S) (action : A)
  (row-nonnegative : ∀ (next-state : S), 0 ≤ transition state action next-state)
  (row-normalized : probability/signed-total-mass S states (transition state action) = 1)
  → proposition/conjunction (backup₁ ≤ backup + discount · epsilon) (backup ≤ backup₁ + discount · epsilon)
  where backup := bellman/signed-action-backup S A states transition reward discount right-value state action
  where backup₁ := bellman/signed-action-backup S A states transition reward discount left-value state action