Reference · Finite types, distributions and Markov chains

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

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

Rate-null convergence certificate for signed Bellman value iteration. The signed Bellman error-radius recurrence is pointwise equivalent to the established exact `signed/nnrat-power-scale`. For an nnrat discount at most one half and an initial signed error between zero and one, the existing identity-modulus signed rate-null theorem therefore applies. Combining that certificate with the finite-horizon Bellman envelope yields an explicit convergence package around an assumed fixed point. The one-half restriction comes from the currently available signed geometric library. Fixed-point existence remains a premise. Native, kernel-checked, and axiom-free on D63.

Depends onmath.linear.matrix.affine-nnrat-exact-rate-nullmath.finite.bellman-signed-value-iteration

value/signed-vi-error-radius-is-nnrat-power-scale :
  (discount : ℚ≥0) (initial-error : ℚ) (steps : ℕ)
  → value/signed-vi-error-radius (signed/from-nnrat discount) initial-error steps = signed/nnrat-power-scale discount steps initial-error

analysis/signed-vi-error-radius-rate-null-of-at-most-half :
  (discount : ℚ≥0)
  (discount-at-most-half : discount ≤ nnrat/half)
  (initial-error : ℚ)
  (initial-error-nonnegative : 0 ≤ initial-error)
  (initial-error-at-most-one : initial-error ≤ 1)
  → analysis/signed-rate-null (fun steps => radius steps) (fun index => index)
  where radius := value/signed-vi-error-radius (signed/from-nnrat discount) initial-error

value/nnrat-transition-signed-iterate-fixed-point-converges-at-most-half.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (actions : Finset A)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ) (discount : ℚ≥0)
  (discount-at-most-half : discount ≤ nnrat/half)
  (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 => backup value state₁ action) fixed-value state = fixed-value state)
  (initial : S → ℚ) (initial-error : ℚ)
  (initial-error-nonnegative : 0 ≤ initial-error)
  (initial-error-at-most-one : initial-error ≤ 1)
  (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 + (fun steps₁ => value/signed-vi-error-radius (signed/from-nnrat discount) initial-error steps₁) steps) (fixed-value state ≤ iterate₁ steps initial state + (fun steps₁ => value/signed-vi-error-radius (signed/from-nnrat discount) initial-error steps₁) steps))
  where backup := 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)
  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 (…⟨1⟩ …⟨1⟩ …⟨1⟩ …⟨1⟩)) reward (signed/from-nnrat discount) value state₁ action)
  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 => …⟨1⟩ …⟨7⟩) reward (signed/from-nnrat discount) value state₁ action)
  where null := analysis/signed-rate-null (fun steps => value/signed-vi-error-radius (signed/from-nnrat discount) initial-error steps) (fun index => index)