Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-monotone

Finite types, distributions and Markov chainssrc/rainbow/math/finite/bellman_monotone.clj0 definitions, 4 theorems

Monotonicity of finite nnrat expectations, Bellman action backups, and the Bellman optimality operator. Native and axiom-free on the D63 checkpoint.

list/nnrat-map-sum-monotone.{u} :
  (A : Type u) (lower upper : A → ℚ≥0)
  (pointwise : ∀ (x : A), lower x ≤ upper x)
  (source : List A)
  → nnrat/map-sum A lower source ≤ nnrat/map-sum A upper source

probability/nnrat-expectation-monotone.{u} :
  (A : Type u) (source : Finset A) (mass lower-value upper-value : A → ℚ≥0)
  (pointwise : ∀ (state : A), lower-value state ≤ upper-value state)
  → expectation lower-value ≤ expectation upper-value
  where expectation := probability/nnrat-expectation A source mass

bellman/nnrat-action-backup-monotone.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (transition : S → A → S → ℚ≥0)
  (reward : S → A → ℚ≥0) (discount : ℚ≥0) (lower-value upper-value : S → ℚ≥0)
  (pointwise : ∀ (next-state : S), lower-value next-state ≤ upper-value next-state)
  (state : S) (action : A)
  → backup lower-value state action ≤ backup upper-value state action
  where backup := bellman/nnrat-action-backup S A states transition reward discount

value/nnrat-optimality-step-monotone.{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)
  (lower-value upper-value : S → ℚ≥0)
  (pointwise : ∀ (next-state : S), lower-value next-state ≤ upper-value next-state)
  (state : S)
  → step lower-value state ≤ step upper-value state
  where step := value/nnrat-optimality-step S A actions fallback (bellman/nnrat-action-backup S A states transition reward discount)