Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-iterate-monotone

Finite types, distributions and Markov chainssrc/rainbow/math/finite/bellman_iterate_monotone.clj0 definitions, 5 theorems

A post-fixed nnrat value function lies below every finite iterate of the Bellman optimality operator. Native and axiom-free on the D63 checkpoint.

Depends onmath.finite.bellman-monotone

value/nnrat-value-below-optimality-iterate-zero.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (value : S → ℚ≥0) (state : S)
  → value state ≤ value/nnrat-iterate S A actions fallback backup 0 value state

value/nnrat-value-below-optimality-iterate-successor.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (value : S → ℚ≥0) (previous : ℕ)
  (below-successor : ∀ (state : S), value state ≤ value/nnrat-optimality-step S A actions fallback backup (iterate) state)
  (state : S)
  → value state ≤ value/nnrat-iterate S A actions fallback backup (data/succ previous) value state
  where iterate := value/nnrat-iterate S A actions fallback backup previous value

value/nnrat-value-below-optimality-iterate-rec.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (value : S → ℚ≥0)
  (base : (fun steps => ∀ (state : S), value state ≤ iterate steps value state) 0)
  (successor-step : ∀ (previous : ℕ), ∀ (induction-hypothesis : (fun steps => ∀ (state : S), value state ≤ iterate steps value state) previous), (fun steps => ∀ (state : S), value state ≤ iterate steps value state) (data/succ previous))
  (steps : ℕ) (state : S)
  → value state ≤ iterate steps value state
  where iterate := value/nnrat-iterate S A actions fallback backup

value/nnrat-value-below-optimality-iterate-generic.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (value : S → ℚ≥0)
  (below-step : ∀ (state : S), value state ≤ step value state)
  (step-monotone : ∀ (lower-value : S → ℚ≥0), ∀ (upper-value : S → ℚ≥0), ∀ (pointwise : ∀ (state : S), lower-value state ≤ upper-value state), ∀ (state : S), step lower-value state ≤ step upper-value state)
  (steps : ℕ) (state : S)
  → value state ≤ value/nnrat-iterate S A actions fallback backup steps value state
  where step := value/nnrat-optimality-step S A actions fallback backup

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