Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-value-iteration-converges

Finite types, distributions and Markov chainssrc/rainbow/math/finite/bellman_value_iteration_converges.clj1 definitions, 15 theorems

Uniform additive convergence bounds for finite Bellman value iteration. Bellman optimality and iteration stay opaque. Fixed-point transport uses the two-sided contraction theorem; iteration transport uses only propositional unfold theorems and equality substitution. Native and axiom-free on D63.

Depends onmath.rational.nnrat.archimedeanmath.finite.bellman-optimalitymath.finite.bellman-backup-contractionmath.finite.bellman-iterate-monotonemath.rational.nnrat.general-contraction

value/nnrat-vi-error-radius :
  (x₁ x₂ : ℚ≥0) (x₃ : ℕ)
  → ℚ≥0

value/nnrat-function-additive-upper-transport.{u} :
  (S : Type u) (left right : S → ℚ≥0)
  (same : left = right)
  (upper : S → ℚ≥0) (epsilon : ℚ≥0) (state : S)
  (ordered : left state ≤ upper state + epsilon)
  → right state ≤ upper state + epsilon

value/nnrat-function-additive-lower-transport.{u} :
  (S : Type u) (left right : S → ℚ≥0)
  (same : left = right)
  (lower : S → ℚ≥0) (epsilon : ℚ≥0) (state : S)
  (ordered : lower state ≤ left state + epsilon)
  → lower state ≤ right state + epsilon

value/nnrat-optimality-step-fixed-point-contraction.{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)
  (fixed-value : S → ℚ≥0)
  (fixed-point : ∀ (state : S), value/nnrat-optimality-step S A actions fallback (bellman/nnrat-action-backup S A states transition reward discount) fixed-value state = fixed-value state)
  (left-value : S → ℚ≥0) (epsilon : ℚ≥0)
  (left-pointwise : ∀ (state : S), left-value state ≤ fixed-value state + epsilon)
  (right-pointwise : ∀ (state : S), fixed-value state ≤ left-value state + epsilon)
  (state : S)
  → proposition/conjunction (step ≤ fixed-value state + discount · epsilon) (fixed-value state ≤ step + discount · epsilon)
  where step := value/nnrat-optimality-step S A actions fallback (bellman/nnrat-action-backup S A states transition reward discount) left-value state

value/nnrat-optimality-fixed-point-additive-advance.{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)
  (fixed-value : S → ℚ≥0)
  (fixed-point : ∀ (state : S), value/nnrat-optimality-step S A actions fallback (bellman/nnrat-action-backup S A states transition reward discount) fixed-value state = fixed-value state)
  (candidate : S → ℚ≥0) (epsilon : ℚ≥0)
  (close : ∀ (state : S), proposition/conjunction (candidate state ≤ fixed-value state + epsilon) (fixed-value state ≤ candidate state + epsilon))
  (state : S)
  → proposition/conjunction ((fun state₁ => step state₁) state ≤ fixed-value state + discount · epsilon) (fixed-value state ≤ (fun state₁ => step state₁) state + discount · epsilon)
  where step := value/nnrat-optimality-step S A actions fallback (bellman/nnrat-action-backup S A states transition reward discount) candidate

value/nnrat-iterate-successor-additive-upper.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (initial : S → ℚ≥0) (steps : ℕ) (upper : S → ℚ≥0)
  (epsilon : ℚ≥0) (state : S)
  (step-bound : (fun state₁ => value/nnrat-optimality-step S A actions fallback backup (iterate) state₁) state ≤ upper state + epsilon)
  → value/nnrat-iterate S A actions fallback backup (data/succ steps) initial state ≤ upper state + epsilon
  where iterate := value/nnrat-iterate S A actions fallback backup steps initial

value/nnrat-iterate-successor-additive-lower.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (initial : S → ℚ≥0) (steps : ℕ) (lower : S → ℚ≥0)
  (epsilon : ℚ≥0) (state : S)
  (step-bound : lower state ≤ (fun state₁ => value/nnrat-optimality-step S A actions fallback backup (iterate) state₁) state + epsilon)
  → lower state ≤ value/nnrat-iterate S A actions fallback backup (data/succ steps) initial state + epsilon
  where iterate := value/nnrat-iterate S A actions fallback backup steps initial

value/nnrat-iterate-successor-additively-close.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (initial : S → ℚ≥0) (steps : ℕ)
  (fixed-value : S → ℚ≥0) (epsilon : ℚ≥0)
  (step-close : ∀ (state : S), proposition/conjunction (step state ≤ fixed-value state + epsilon) (fixed-value state ≤ step state + epsilon))
  (state : S)
  → proposition/conjunction (iterate ≤ fixed-value state + epsilon) (fixed-value state ≤ iterate + epsilon)
  where iterate := value/nnrat-iterate S A actions fallback backup (data/succ steps) initial state
  where step := value/nnrat-optimality-step S A actions fallback backup (value/nnrat-iterate S A actions fallback backup steps initial)

value/nnrat-iterate-zero-additively-close.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (initial fixed-value : S → ℚ≥0) (epsilon : ℚ≥0)
  (initial-close : ∀ (state : S), proposition/conjunction (initial state ≤ fixed-value state + epsilon) (fixed-value state ≤ initial state + epsilon))
  (state : S)
  → proposition/conjunction (iterate ≤ fixed-value state + epsilon) (fixed-value state ≤ iterate + epsilon)
  where iterate := value/nnrat-iterate S A actions fallback backup 0 initial state

value/nnrat-iterate-fixed-point-additive-radius.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (discount : ℚ≥0) (fixed-value initial : S → ℚ≥0)
  (initial-error : ℚ≥0)
  (initial-close : ∀ (state : S), proposition/conjunction (initial state ≤ fixed-value state + initial-error) (fixed-value state ≤ initial state + initial-error))
  (advance : ∀ (candidate : S → ℚ≥0), ∀ (epsilon : ℚ≥0), ∀ (close : ∀ (state : S), proposition/conjunction (candidate state ≤ fixed-value state + epsilon) (fixed-value state ≤ candidate state + epsilon)), ∀ (state : S), proposition/conjunction ((fun state₁ => step candidate state₁) state ≤ fixed-value state + discount · epsilon) (fixed-value state ≤ (fun state₁ => step candidate state₁) state + discount · epsilon))
  (steps : ℕ) (state : S)
  → proposition/conjunction (iterate ≤ fixed-value state + radius) (fixed-value state ≤ iterate + radius)
  where iterate := value/nnrat-iterate S A actions fallback backup steps initial state
  where radius := value/nnrat-vi-error-radius discount initial-error steps
  where step := value/nnrat-optimality-step S A actions fallback backup

analysis/nnrat-vi-error-radius-rate-null :
  (ap gp : ℕ) (initial-error : ℚ≥0)
  (initial-bound : radius 0 ≤ nnrat/general-harmonic ap gp 0)
  → analysis/rate-null (radius) (fun k => nat/multiply (data/succ ap) k)
  where radius := value/nnrat-vi-error-radius (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))) initial-error

value/nnrat-optimality-iterate-fixed-point-converges.{u, v} :
  (ap gp : ℕ) (S : Type u) (A : Type v) (states : Finset S) (actions : Finset A)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ≥0) (fallback : S → A)
  (fallback-admissible : ∀ (state : S), fallback state ∈ actions)
  (normalized : markov/nnrat-rows-normalized S A states transition)
  (fixed-value : S → ℚ≥0)
  (fixed-point : ∀ (state : S), value/nnrat-optimality-step S A actions fallback (bellman/nnrat-action-backup S A states transition reward (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp)))) fixed-value state = fixed-value state)
  (initial : S → ℚ≥0) (initial-error : ℚ≥0)
  (initial-bound : value/nnrat-vi-error-radius (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))) initial-error 0 ≤ nnrat/general-harmonic ap gp 0)
  (initial-close : ∀ (state : S), proposition/conjunction (initial state ≤ fixed-value state + initial-error) (fixed-value state ≤ initial state + initial-error))
  → proposition/conjunction (null) (∀ (steps : ℕ), ∀ (state : S), proposition/conjunction (iterate steps initial state ≤ fixed-value state + value/nnrat-vi-error-radius (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))) initial-error steps) (fixed-value state ≤ iterate steps initial state + value/nnrat-vi-error-radius (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))) initial-error steps))
  where iterate := value/nnrat-iterate S A actions fallback (bellman/nnrat-action-backup S A states transition reward (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))))
  where null := analysis/rate-null (value/nnrat-vi-error-radius (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))) initial-error) (fun k => nat/multiply (data/succ ap) k)

analysis/nnrat-at-most-of-rate-null-upper-bounds :
  (error : ℕ → ℚ≥0) (modulus : ℕ → ℕ) (x y : ℚ≥0)
  (null : analysis/rate-null error modulus)
  (bounded : ∀ (steps : ℕ), x ≤ y + error steps)
  → x ≤ y

value/nnrat-bellman-fixed-point-dominates-post-fixed-value.{u, v} :
  (ap gp : ℕ) (S : Type u) (A : Type v) (states : Finset S) (actions : Finset A)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ≥0) (fallback : S → A)
  (fallback-admissible : ∀ (state : S), fallback state ∈ actions)
  (normalized : markov/nnrat-rows-normalized S A states transition)
  (fixed-value : S → ℚ≥0)
  (fixed-point : ∀ (state : S), step fixed-value state = fixed-value state)
  (post-fixed-value : S → ℚ≥0)
  (below-step : ∀ (state : S), post-fixed-value state ≤ step post-fixed-value state)
  (initial-error : ℚ≥0)
  (initial-bound : value/nnrat-vi-error-radius (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))) initial-error 0 ≤ nnrat/general-harmonic ap gp 0)
  (initial-close : ∀ (state : S), proposition/conjunction (post-fixed-value state ≤ fixed-value state + initial-error) (fixed-value state ≤ post-fixed-value state + initial-error))
  (state : S)
  → post-fixed-value state ≤ fixed-value state
  where step := value/nnrat-optimality-step S A actions fallback (bellman/nnrat-action-backup S A states transition reward (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))))

value/nnrat-policy-fixed-point-below-optimality-step.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ≥0) → S → A → ℚ≥0) (value : S → ℚ≥0) (policy : S → A)
  (policy-admissible : ∀ (state : S), policy state ∈ actions)
  (policy-fixed-point : ∀ (state : S), value state = backup value state (policy state))
  (state : S)
  → value state ≤ value/nnrat-optimality-step S A actions fallback backup value state

value/nnrat-policy-value-below-bellman-fixed-point.{u, v} :
  (ap gp : ℕ) (S : Type u) (A : Type v) (states : Finset S) (actions : Finset A)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ≥0) (fallback : S → A)
  (fallback-admissible : ∀ (state : S), fallback state ∈ actions)
  (normalized : markov/nnrat-rows-normalized S A states transition)
  (fixed-value : S → ℚ≥0)
  (fixed-point : ∀ (state : S), value/nnrat-optimality-step S A actions fallback (backup) fixed-value state = fixed-value state)
  (policy : S → A)
  (policy-admissible : ∀ (state : S), policy state ∈ actions)
  (policy-value : S → ℚ≥0)
  (policy-fixed-point : ∀ (state : S), policy-value state = backup policy-value state (policy state))
  (initial-error : ℚ≥0)
  (initial-bound : value/nnrat-vi-error-radius (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))) initial-error 0 ≤ nnrat/general-harmonic ap gp 0)
  (initial-close : ∀ (state : S), proposition/conjunction (policy-value state ≤ fixed-value state + initial-error) (fixed-value state ≤ policy-value state + initial-error))
  (state : S)
  → policy-value state ≤ fixed-value state
  where backup := bellman/nnrat-action-backup S A states transition reward (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp)))