Reference · Finite types, distributions and Markov chains

rainbow.math.finite.policy-improvement

Finite types, distributions and Markov chainssrc/rainbow/math/finite/policy_improvement.clj0 definitions, 1 theorems

Policy-iteration monotonic improvement (Q-score level): the greedy-improved policy's action-score dominates the current policy's at every state. policy/nnrat-improve-dominates-current : for admissible current policy and any score (Q-function), score(s, current s) <= score(s, improve(actions,current,score) s) for all s. I.e. improving a policy never lowers any state's chosen-action score -- the monotonic-improvement guarantee that makes policy iteration climb toward the optimum. It is policy/nnrat-improve-dominates instantiated at the admissible candidate = current(s): the argmax that defines the improved policy scores at least as high as the incumbent action. With a fixed-policy value V^pi consistent in Q-form (V^pi(s) = score(s, current s)) this reads V^pi(s) <= score(s, improved s) = T_{pi'} V^pi(s), the entry point of the policy-improvement value dominance V^pi <= V^{pi'}. Native and axiom-free; chains finite-policy-iteration on the d21 checkpoint.

Depends onmath.finite.policy-iteration

policy/nnrat-improve-dominates-current.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (current : S → A) (score : S → A → ℚ≥0)
  (current-admissible : ∀ (s : S), current s ∈ actions)
  (state : S)
  → score state (current state) ≤ score state (policy/nnrat-improve S A actions current score state)