Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-signed-transition-operator

Finite types, distributions and Markov chainssrc/rainbow/math/finite/bellman_signed_transition_operator.clj2 definitions, 6 theorems

Named concrete signed Bellman operator over ordinary nnrat transitions. A stable name for the concrete operator prevents downstream proofs from repeatedly expanding embedded transitions, signed expectations, action backups and finite argmax. A separate low-arity operator iterator keeps its successor law independent of that expansion. Opaque successor and contraction theorems form the compact proof boundary. This remains a mathematical interface, not an executable solver. Native, kernel-checked, and axiom-free on D63.

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

value/nnrat-transition-signed-optimality-operator.{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) (x₁ : S → ℚ) (x₂ : S)
  → ℚ

value/signed-operator-iterate.{u} :
  (S : Type u) (operator : (S → ℚ) → S → ℚ) (x₁ : ℕ) (x₂ : S → ℚ) (x₃ : S)
  → ℚ

value/nnrat-transition-signed-optimality-operator-unfold.{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) (value : S → ℚ) (state : S)
  → value/nnrat-transition-signed-optimality-operator S A states actions transition reward discount fallback value state = (fun value₁ => fun state₁ => value/signed-optimality-step S A actions fallback (fun value₂ => fun state₂ => fun action => backup value₂ state₂ action) value₁ state₁) value state
  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)

value/signed-operator-iterate-successor.{u} :
  (S : Type u) (operator : (S → ℚ) → S → ℚ) (steps : ℕ) (initial : S → ℚ)
  → iterate (data/succ steps) initial = operator (iterate steps initial)
  where iterate := value/signed-operator-iterate S operator

value/signed-operator-iterate-successor-equivalent.{u} :
  (S : Type u) (operator : (S → ℚ) → S → ℚ) (steps : ℕ) (initial : S → ℚ) (state : S)
  → iterate (data/succ steps) initial state = operator (iterate steps initial) state
  where iterate := value/signed-operator-iterate S operator

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

value/signed-contractive-operator-approximate-fixed-point-general-rate.{u} :
  (ap gp : ℕ) (S : Type u) (operator : (S → ℚ) → S → ℚ) (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 ≤ operator initial state + initial-error) (operator 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 (operator left state ≤ operator right state + signed/from-nnrat (make) · epsilon) (operator right state ≤ operator 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 ≤ operator ((fun steps => iterate steps initial) ((fun index₁ => nat/multiply (data/succ ap) index₁) index)) state + signed/from-nnrat (nnrat/harmonic index)) (operator ((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-operator-iterate S operator
  where make := nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))

value/nnrat-transition-signed-optimality-operator-additively-contractive.{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)
  (left right : S → ℚ) (epsilon : ℚ)
  (close : ∀ (state : S), proposition/conjunction (left state ≤ right state + epsilon) (right state ≤ left state + epsilon))
  (state : S)
  → proposition/conjunction (operator₁ ≤ operator + signed/from-nnrat discount · epsilon) (operator ≤ operator₁ + signed/from-nnrat discount · epsilon)
  where operator := value/nnrat-transition-signed-optimality-operator S A states actions transition reward discount fallback right state
  where operator₁ := value/nnrat-transition-signed-optimality-operator S A states actions transition reward discount fallback left state