Reference · Finite types, distributions and Markov chains

rainbow.math.finite.policy-value-dominance

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

Abstract, reduction-safe policy-improvement value dominance for finite nnrat MDPs. A fixed-policy step selects one already-fixed action at each state, so its monotonicity is exactly Bellman action-backup monotonicity. Consequently a post-fixed value lies below every term of an abstract fixed-policy recurrence. If that recurrence converges to the improved policy's value, the current policy's value is pointwise below the improved value. No concrete iterate or finite argmax occurs in a theorem statement. Native and axiom-free on D63.

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

value/nnrat-fixed-policy-post-fixed-below-sequence.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (transition : S → A → S → ℚ≥0)
  (reward : S → A → ℚ≥0) (discount : ℚ≥0) (policy : S → A) (sequence : ℕ → S → ℚ≥0)
  (value : S → ℚ≥0)
  (below-step : ∀ (state : S), value state ≤ (fun candidate => fun state₁ => backup candidate state₁ (policy state₁)) value state)
  (sequence-zero : sequence 0 = value)
  (sequence-successor : ∀ (steps : ℕ), sequence (data/succ steps) = (fun candidate => fun state => backup candidate state (policy state)) (sequence steps))
  (steps : ℕ) (state : S)
  → value state ≤ sequence steps state
  where backup := bellman/nnrat-action-backup S A states transition reward discount

value/nnrat-policy-improvement-value-dominates.{u, v} :
  (ap gp : ℕ) (S : Type u) (A : Type v) (states : Finset S)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ≥0) (discount : ℚ≥0)
  (improved-policy : S → A) (sequence : ℕ → S → ℚ≥0)
  (improved-value current-value : S → ℚ≥0)
  (one-step-dominance : ∀ (state : S), current-value state ≤ (fun candidate => fun state₁ => backup candidate state₁ (improved-policy state₁)) current-value state)
  (sequence-zero : sequence 0 = current-value)
  (sequence-successor : ∀ (steps : ℕ), sequence (data/succ steps) = (fun candidate => fun state => backup candidate state (improved-policy state)) (sequence steps))
  (error : ℕ → ℚ≥0)
  (initial-error-bound : error 0 ≤ nnrat/general-harmonic ap gp 0)
  (error-contracts : ∀ (steps : ℕ), error (data/succ steps) ≤ nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp)) · error steps)
  (initial-close : ∀ (state : S), proposition/conjunction (sequence 0 state ≤ improved-value state + error 0) (improved-value state ≤ sequence 0 state + error 0))
  (advance-close : ∀ (steps : ℕ), ∀ (previous-close : ∀ (state : S), proposition/conjunction (sequence steps state ≤ improved-value state + error steps) (improved-value state ≤ sequence steps state + error steps)), ∀ (state : S), proposition/conjunction (sequence (data/succ steps) state ≤ improved-value state + error (data/succ steps)) (improved-value state ≤ sequence (data/succ steps) state + error (data/succ steps)))
  (state : S)
  → current-value state ≤ improved-value state
  where backup := bellman/nnrat-action-backup S A states transition reward discount