Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-signed-approximate-optimality

Finite types, distributions and Markov chainssrc/rainbow/math/finite/bellman_signed_approximate_optimality.clj0 definitions, 2 theorems

Constructive approximate fixed points of signed Bellman optimality. Successive iterates of any two-sided additively contractive operator inherit the geometric error radius of the initial residual. A rate-null certificate for that radius therefore turns the iterate at its explicit modulus into an approximate fixed point. The Bellman capstone applies this interface to the actual runtime finite max-over-actions iterate for any signed action backup carrying its two-sided contraction certificate. The existing normalized nnrat-transition theorem supplies exactly that certificate. No exact fixed point is assumed or constructed. The witness is the actual finite Bellman iterate, and its residual guarantee holds pointwise over the entire state type. Native, kernel-checked, and axiom-free on D63.

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

value/signed-abstract-successive-iterate-additive-radius.{u} :
  (S : Type u) (operator : (S → ℚ) → S → ℚ) (sequence : ℕ → S → ℚ)
  (discount initial-error : ℚ)
  (successor-equivalent : ∀ (steps : ℕ), ∀ (state : S), sequence (data/succ steps) state = operator (sequence steps) state)
  (initial-close : ∀ (state : S), proposition/conjunction (sequence 0 state ≤ sequence 1 state + initial-error) (sequence 1 state ≤ sequence 0 state + initial-error))
  (advance : ∀ (left : S → ℚ), ∀ (right : S → ℚ), ∀ (epsilon : ℚ), ∀ (close : ∀ (state : S), proposition/conjunction (left state ≤ right state + epsilon) (right state ≤ left state + epsilon)), ∀ (state : S), proposition/conjunction (operator left state ≤ operator right state + discount · epsilon) (operator right state ≤ operator left state + discount · epsilon))
  (steps : ℕ) (state : S)
  → proposition/conjunction (sequence steps state ≤ sequence (data/succ steps) state + radius) (sequence (data/succ steps) state ≤ sequence steps state + radius)
  where radius := value/signed-vi-error-radius discount initial-error steps

value/signed-rate-certificate-approximate-fixed-point.{u} :
  (S : Type u) (operator : (S → ℚ) → S → ℚ) (sequence : ℕ → S → ℚ) (radius : ℕ → ℚ)
  (modulus : ℕ → ℕ)
  (successor-equivalent : ∀ (n : ℕ), ∀ (state : S), sequence (data/succ n) state = operator (sequence n) state)
  (successive-close : ∀ (n : ℕ), ∀ (state : S), proposition/conjunction (sequence n state ≤ sequence (data/succ n) state + radius n) (sequence (data/succ n) state ≤ sequence n state + radius n))
  (radius-null : analysis/signed-rate-null radius modulus) (index : ℕ) (state : S)
  → proposition/conjunction (sequence (modulus index) state ≤ operator (sequence (modulus index)) state + signed/from-nnrat (nnrat/harmonic index)) (operator (sequence (modulus index)) state ≤ sequence (modulus index) state + signed/from-nnrat (nnrat/harmonic index))