Reference · Finite types, distributions and Markov chains

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

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

Approximate fixed points for a certified finite signed Bellman operator. This specializes the abstract successive-iterate proof to Rainbow's actual runtime finite-argmax Bellman iterate while retaining the operator's two-sided additive contraction as an explicit certificate. Existing normalized-transition Bellman theorems produce that certificate; keeping it opaque avoids re-expanding transition sums and argmax during every induction step. For gamma=(a+1)/(a+g+2), the iterate at horizon (a+1)*k is pointwise within 1/(k+1) of its next Bellman image and is packaged as an existential witness. No exact fixed point is assumed or constructed. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.bellman-signed-approximate-optimality

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

value/signed-optimality-approximate-fixed-point-general-rate.{u, v} :
  (ap gp : ℕ) (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ) → S → A → ℚ) (initial : S → ℚ) (initial-error : ℚ)
  (initial-error-nonnegative : 0 ≤ initial-error)
  (initial-bound : initial-error ≤ signed/from-nnrat (nnrat/general-harmonic ap gp 0))
  (initial-close : ∀ (state : S), proposition/conjunction (initial state ≤ (fun value => fun state₁ => step value state₁) initial state + initial-error) ((fun value => fun state₁ => step value state₁) initial state ≤ initial 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 ((fun value => fun state₁ => step value state₁) left state ≤ (fun value => fun state₁ => step value state₁) right state + signed/from-nnrat (make) · epsilon) ((fun value => fun state₁ => step value state₁) right state ≤ (fun value => fun state₁ => step value state₁) left state + signed/from-nnrat (make) · epsilon))
  (index : ℕ) (state : S)
  → proposition/conjunction ((fun steps => iterate steps initial) ((fun index₁ => nat/multiply (data/succ ap) index₁) index) state ≤ (fun value => fun state₁ => step value state₁) ((fun steps => iterate steps initial) ((fun index₁ => nat/multiply (data/succ ap) index₁) index)) state + signed/from-nnrat (nnrat/harmonic index)) ((fun value => fun state₁ => step value state₁) ((fun steps => iterate steps initial) ((fun index₁ => nat/multiply (data/succ ap) index₁) index)) state ≤ (fun steps => iterate steps initial) ((fun index₁ => nat/multiply (data/succ ap) index₁) index) state + signed/from-nnrat (nnrat/harmonic index))
  where iterate := value/signed-iterate S A actions fallback backup
  where make := nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))
  where step := value/signed-optimality-step S A actions fallback backup

value/signed-optimality-approximate-fixed-point-exists-general-rate.{u, v} :
  (ap gp : ℕ) (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ) → S → A → ℚ) (initial : S → ℚ) (initial-error : ℚ)
  (initial-error-nonnegative : 0 ≤ initial-error)
  (initial-bound : initial-error ≤ signed/from-nnrat (nnrat/general-harmonic ap gp 0))
  (initial-close : ∀ (state : S), proposition/conjunction (initial state ≤ (fun value => fun state₁ => step value state₁) initial state + initial-error) ((fun value => fun state₁ => step value state₁) initial state ≤ initial 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 ((fun value => fun state₁ => step value state₁) left state ≤ (fun value => fun state₁ => step value state₁) right state + signed/from-nnrat (make) · epsilon) ((fun value => fun state₁ => step value state₁) right state ≤ (fun value => fun state₁ => step value state₁) left state + signed/from-nnrat (make) · epsilon))
  (index : ℕ)
  → proposition/existence (S → ℚ) (fun candidate => ∀ (state : S), proposition/conjunction (candidate state ≤ (fun value => fun state₁ => step value state₁) candidate state + signed/from-nnrat (nnrat/harmonic index)) ((fun value => fun state₁ => step value state₁) candidate state ≤ candidate state + signed/from-nnrat (nnrat/harmonic index)))
  where make := nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))
  where step := value/signed-optimality-step S A actions fallback backup