Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-value-optimality-theorem

Finite types, distributions and Markov chainssrc/rainbow/math/finite/bellman_value_optimality_theorem.clj0 definitions, 4 theorems

Abstract, reduction-safe capstones for finite Bellman value iteration. The sequence and its error radius are parameters: no theorem statement asks the kernel to reduce Bellman optimality, finite argmax, or the concrete iterate definition. The Bellman-specific predecessor lemmas provide the initial/advance and below-sequence hypotheses. Native and axiom-free on D63.

Depends onmath.finite.bellman-value-iteration-converges

value/nnrat-abstract-value-iteration-converges.{u} :
  (ap gp : ℕ) (S : Type u) (sequence : ℕ → S → ℚ≥0) (fixed-value : S → ℚ≥0)
  (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 ≤ fixed-value state + error 0) (fixed-value state ≤ sequence 0 state + error 0))
  (advance-close : ∀ (steps : ℕ), ∀ (previous-close : ∀ (state : S), proposition/conjunction (sequence steps state ≤ fixed-value state + error steps) (fixed-value state ≤ sequence steps state + error steps)), ∀ (state : S), proposition/conjunction (sequence (data/succ steps) state ≤ fixed-value state + error (data/succ steps)) (fixed-value state ≤ sequence (data/succ steps) state + error (data/succ steps)))
  → proposition/conjunction (null) (∀ (k : ℕ), ∀ (steps : ℕ), ∀ (late : (fun k₁ => nat/multiply (data/succ ap) k₁) k ≤ steps), ∀ (state : S), proposition/conjunction (sequence steps state ≤ fixed-value state + nnrat/make 1 k) (fixed-value state ≤ sequence steps state + nnrat/make 1 k))
  where null := analysis/rate-null error (fun k => nat/multiply (data/succ ap) k)

value/nnrat-rate-limit-dominates-below-iterates.{u} :
  (S : Type u) (sequence : ℕ → S → ℚ≥0) (limit-value lower-value : S → ℚ≥0)
  (error : ℕ → ℚ≥0) (threshold : ℕ → ℕ)
  (error-null : analysis/rate-null error threshold)
  (below-sequence : ∀ (steps : ℕ), ∀ (state : S), lower-value state ≤ sequence steps state)
  (sequence-upper : ∀ (steps : ℕ), ∀ (state : S), sequence steps state ≤ limit-value state + error steps)
  (state : S)
  → lower-value state ≤ limit-value state

value/nnrat-abstract-post-fixed-value-below-sequence.{u} :
  (S : Type u) (operator : (S → ℚ≥0) → S → ℚ≥0) (sequence : ℕ → S → ℚ≥0)
  (value : S → ℚ≥0)
  (below-operator : ∀ (state : S), value state ≤ operator value state)
  (operator-monotone : ∀ (left : S → ℚ≥0), ∀ (right : S → ℚ≥0), ∀ (ordered : ∀ (state : S), left state ≤ right state), ∀ (state : S), operator left state ≤ operator right state)
  (sequence-zero : sequence 0 = value)
  (sequence-successor : ∀ (steps : ℕ), sequence (data/succ steps) = operator (sequence steps))
  (steps : ℕ) (state : S)
  → value state ≤ sequence steps state

value/nnrat-abstract-bellman-policy-optimality.{u} :
  (ap gp : ℕ) (S : Type u) (operator : (S → ℚ≥0) → S → ℚ≥0) (sequence : ℕ → S → ℚ≥0)
  (optimal-value policy-value policy-update : S → ℚ≥0)
  (policy-fixed-point : ∀ (state : S), policy-value state = policy-update state)
  (operator-dominates-policy : ∀ (state : S), policy-update state ≤ operator policy-value state)
  (operator-monotone : ∀ (left : S → ℚ≥0), ∀ (right : S → ℚ≥0), ∀ (ordered : ∀ (state : S), left state ≤ right state), ∀ (state : S), operator left state ≤ operator right state)
  (sequence-zero : sequence 0 = policy-value)
  (sequence-successor : ∀ (steps : ℕ), sequence (data/succ steps) = operator (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 ≤ optimal-value state + error 0) (optimal-value state ≤ sequence 0 state + error 0))
  (advance-close : ∀ (steps : ℕ), ∀ (previous-close : ∀ (state : S), proposition/conjunction (sequence steps state ≤ optimal-value state + error steps) (optimal-value state ≤ sequence steps state + error steps)), ∀ (state : S), proposition/conjunction (sequence (data/succ steps) state ≤ optimal-value state + error (data/succ steps)) (optimal-value state ≤ sequence (data/succ steps) state + error (data/succ steps)))
  (state : S)
  → policy-value state ≤ optimal-value state