Reference · Finite types, distributions and Markov chains

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

Finite types, distributions and Markov chainssrc/rainbow/math/finite/bellman_signed_value_iteration.clj2 definitions, 5 theorems

Finite-horizon signed Bellman value-iteration envelopes. A generic signed iterate and exact recursive error radius are defined over the runtime finite-action optimality operator. A structural induction lifts any two-sided one-step additive contraction through every finite horizon. The concrete capstone instantiates that induction with an ordinary normalized nnrat transition kernel, arbitrary signed rewards and values, and an assumed signed Bellman fixed point. This proves finite-horizon error propagation only. Fixed-point existence and convergence of the radius remain separate obligations. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.bellman-signed-transition-bridge

value/signed-iterate.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ) → S → A → ℚ) (x₁ : ℕ) (x₂ : S → ℚ) (x₃ : S)
  → ℚ

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

value/signed-iterate-zero.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ) → S → A → ℚ) (initial : S → ℚ)
  → value/signed-iterate S A actions fallback backup 0 initial = initial

value/signed-iterate-successor.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ) → S → A → ℚ) (steps : ℕ) (initial : S → ℚ)
  → iterate (data/succ steps) initial = (fun x₁ => fun value => fun state => value/signed-optimality-step S A actions fallback backup value state) steps (iterate steps initial)
  where iterate := value/signed-iterate S A actions fallback backup

value/signed-iterate-additive-radius.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ) → S → A → ℚ) (discount : ℚ) (fixed-value initial : S → ℚ)
  (initial-error : ℚ)
  (initial-close : ∀ (state : S), proposition/conjunction (initial state ≤ fixed-value state + initial-error) (fixed-value state ≤ initial state + initial-error))
  (advance : ∀ (candidate : S → ℚ), ∀ (epsilon : ℚ), ∀ (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/signed-iterate S A actions fallback backup steps initial state
  where radius := value/signed-vi-error-radius discount initial-error steps
  where step := value/signed-optimality-step S A actions fallback backup

value/nnrat-transition-signed-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 → ℚ) (discount : ℚ≥0)
  (fallback : S → A)
  (fallback-admissible : ∀ (state : S), fallback state ∈ actions)
  (normalized : ∀ (state : S), ∀ (action : A), probability/nnrat-total-mass S states (transition state action) = 1)
  (fixed-value : S → ℚ)
  (fixed-point : ∀ (state : S), value/signed-optimality-step S A actions fallback (fun value => fun state₁ => fun action => bellman/signed-action-backup S A states (fun state₂ => fun action₁ => fun next-state => signed/from-nnrat (transition state₂ action₁ next-state)) reward (signed/from-nnrat discount) value state₁ action) fixed-value state = fixed-value state)
  (candidate : S → ℚ) (epsilon : ℚ)
  (candidate-close-left : ∀ (state : S), candidate state ≤ fixed-value state + epsilon)
  (candidate-close-right : ∀ (state : S), fixed-value state ≤ candidate state + epsilon)
  (state : S)
  → proposition/conjunction (step ≤ fixed-value state + signed/from-nnrat discount · epsilon) (fixed-value state ≤ step + signed/from-nnrat discount · epsilon)
  where step := value/signed-optimality-step S A actions fallback (fun value => fun state₁ => fun action => bellman/signed-action-backup S A states (fun state₂ => fun action₁ => fun next-state => signed/from-nnrat (transition state₂ action₁ next-state)) reward (signed/from-nnrat discount) value state₁ action) candidate state

value/nnrat-transition-signed-iterate-fixed-point-additive-radius.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (actions : Finset A)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ) (discount : ℚ≥0)
  (fallback : S → A)
  (fallback-admissible : ∀ (state : S), fallback state ∈ actions)
  (normalized : ∀ (state : S), ∀ (action : A), probability/nnrat-total-mass S states (transition state action) = 1)
  (fixed-value : S → ℚ)
  (fixed-point : ∀ (state : S), value/signed-optimality-step S A actions fallback (fun value => fun state₁ => fun action => bellman/signed-action-backup S A states (fun state₂ => fun action₁ => fun next-state => signed/from-nnrat (transition state₂ action₁ next-state)) reward (signed/from-nnrat discount) value state₁ action) fixed-value state = fixed-value state)
  (initial : S → ℚ) (initial-error : ℚ)
  (initial-close : ∀ (state : S), proposition/conjunction (initial state ≤ fixed-value state + initial-error) (fixed-value state ≤ initial state + initial-error))
  (steps : ℕ) (state : S)
  → proposition/conjunction (iterate ≤ fixed-value state + radius) (fixed-value state ≤ iterate + radius)
  where iterate := value/signed-iterate S A actions fallback (fun value => fun state₁ => fun action => bellman/signed-action-backup S A states (fun state₂ => fun action₁ => fun next-state => signed/from-nnrat (transition state₂ action₁ next-state)) reward (signed/from-nnrat discount) value state₁ action) steps initial state
  where radius := value/signed-vi-error-radius (signed/from-nnrat discount) initial-error steps