Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-optimality

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

Bellman optimality, operator level: the optimal (greedy / max-over-actions) Bellman backup dominates every fixed-policy backup. value/nnrat-optimality-step-dominates-policy : for any admissible policy pi (pi : S -> A with pi s in actions for all s), backup(V, s, pi s) <= optimality-step(backup, V, s) i.e. T_pi V <= T* V pointwise -- the foundational operator inequality of Bellman optimality: no single-step policy backup can exceed the optimal (argmax) backup. It lifts the per-ACTION argmax dominance (value/nnrat-optimality-step-dominates, quantified over candidate actions) to a per-POLICY statement by instantiating the candidate at the policy's chosen action pi(s), whose admissibility is the policy-admissibility hypothesis. Combined with value/nnrat-optimality-step-unfold (optimality-step = backup at the greedy action), this says the greedy policy attains T* and dominates every other policy's one-step backup. The remaining step to full value-function Bellman optimality (V^pi <= V* for the fixed-point values) is the monotone iteration of T* to its fixed point (needs T*-monotonicity + convergence). Native and axiom-free; chains finite-value-iteration on the d21 checkpoint.

Depends onmath.finite.value-iteration

value/nnrat-optimality-step-dominates-policy.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (value : S → ℚ≥0) (policy : S → A)
  (policy-admissible : ∀ (s : S), policy s ∈ actions)
  (state : S)
  → backup value state (policy state) ≤ value/nnrat-optimality-step S A actions fallback backup value state

value/nnrat-greedy-dominates-policy.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (value : S → ℚ≥0) (policy : S → A)
  (policy-admissible : ∀ (s : S), policy s ∈ actions)
  (state : S)
  → backup value state (policy state) ≤ backup value state (value/nnrat-greedy-action S A actions fallback backup value state)