Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-backup-contraction

Finite types, distributions and Markov chainssrc/rainbow/math/finite/bellman_backup_contraction.clj0 definitions, 2 theorems

Discount-scaled contraction of finite NNRAT Bellman backups and T*. A normalized transition row transports two-sided additive epsilon-closeness of value functions to two-sided additive (discount*epsilon)-closeness of a fixed action backup. With every transition row normalized, finite argmax nonexpansiveness lifts the same estimate to the Bellman optimality step. The optimality proof treats value/nnrat-optimality-step as opaque: all argmax reasoning stays behind its propositional nonexpansiveness theorem. Native and axiom-free on D63.

bellman/nnrat-action-backup-contraction.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (transition : S → A → S → ℚ≥0)
  (reward : S → A → ℚ≥0) (discount : ℚ≥0) (left-value right-value : S → ℚ≥0)
  (epsilon : ℚ≥0)
  (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-normalized : probability/nnrat-total-mass S states (transition state action) = 1)
  → proposition/conjunction (backup₁ ≤ backup + discount · epsilon) (backup ≤ backup₁ + discount · epsilon)
  where backup := bellman/nnrat-action-backup S A states transition reward discount right-value state action
  where backup₁ := bellman/nnrat-action-backup S A states transition reward discount left-value state action

value/nnrat-optimality-step-sup-contraction.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (actions : Finset A)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ≥0) (discount : ℚ≥0)
  (fallback : S → A)
  (fallback-admissible : ∀ (current : S), fallback current ∈ actions)
  (left-value right-value : S → ℚ≥0) (epsilon : ℚ≥0)
  (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)
  (normalized : markov/nnrat-rows-normalized S A states transition) (state : S)
  → proposition/conjunction (step₁ ≤ step + discount · epsilon) (step ≤ step₁ + discount · epsilon)
  where step := value/nnrat-optimality-step S A actions fallback (bellman/nnrat-action-backup S A states transition reward discount) right-value state
  where step₁ := value/nnrat-optimality-step S A actions fallback (bellman/nnrat-action-backup S A states transition reward discount) left-value state