Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-greedy-policy-optimal

Finite types, distributions and Markov chainssrc/rainbow/math/finite/bellman_greedy_policy_optimal.clj0 definitions, 3 theorems

Fully concrete greedy-policy extraction for exact finite NNRAT Bellman models. The selected policy is the existing finite greedy action function at an optimal fixed value. It is admissible, and any value satisfying its policy Bellman equation is pointwise equivalent to the optimal value. The latter discharges the abstract fixed-policy uniqueness premise with the exact residual-based theorem. The combined theorem packages legality and value attainment as a constructive optimal-policy certificate. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.bellman-policy-residual-certificate

value/nnrat-greedy-bellman-policy-is-admissible.{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 : ∀ (state : S), fallback state ∈ actions)
  (optimal-value : S → ℚ≥0) (state : S)
  → (fun state₁ => value/nnrat-greedy-action S A actions fallback (backup) optimal-value state₁) state ∈ actions
  where backup := bellman/nnrat-action-backup S A states transition reward discount

value/nnrat-greedy-bellman-policy-value-is-optimal.{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 : ∀ (state : S), fallback state ∈ actions)
  (normalized : markov/nnrat-rows-normalized S A states transition)
  (state-covered : ∀ (state : S), state ∈ states)
  (optimal-value : S → ℚ≥0)
  (optimal-fixed-point : ∀ (state : S), value/nnrat-optimality-step S A actions fallback (backup) optimal-value state = optimal-value state)
  (policy-value : S → ℚ≥0)
  (policy-value-fixed : ∀ (state : S), backup policy-value state ((fun state₁ => value/nnrat-greedy-action S A actions fallback (backup) optimal-value state₁) state) = policy-value state)
  (gap inverse : ℚ≥0)
  (discount-plus-gap-one : discount + gap = 1)
  (inverse-times-gap-one : inverse · gap = 1)
  (state : S)
  → policy-value state = optimal-value state
  where backup := bellman/nnrat-action-backup S A states transition reward discount

value/nnrat-greedy-bellman-policy-optimal-certificate.{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 : ∀ (state : S), fallback state ∈ actions)
  (normalized : markov/nnrat-rows-normalized S A states transition)
  (state-covered : ∀ (state : S), state ∈ states)
  (optimal-value : S → ℚ≥0)
  (optimal-fixed-point : ∀ (state : S), value/nnrat-optimality-step S A actions fallback (bellman/nnrat-action-backup S A states transition reward discount) optimal-value state = optimal-value state)
  (policy-value : S → ℚ≥0)
  (policy-value-fixed : ∀ (state : S), bellman/nnrat-action-backup S A states transition reward discount policy-value state ((fun state₁ => action state₁) state) = policy-value state)
  (gap inverse : ℚ≥0)
  (discount-plus-gap-one : discount + gap = 1)
  (inverse-times-gap-one : inverse · gap = 1)
  → proposition/conjunction (∀ (state : S), (fun state₁ => action state₁) state ∈ actions) (∀ (state : S), policy-value state = optimal-value state)
  where action := value/nnrat-greedy-action S A actions fallback (bellman/nnrat-action-backup S A states transition reward discount) optimal-value