Reference · Finite types, distributions and Markov chains
rainbow.math.finite.bellman-signed-optimal-contraction
Signed finite Bellman optimality inherits action-backup contraction. This composes the concrete signed reward/transition action backup with the runtime-length signed argmax operator. Explicit nonnegative normalized transition rows and a nonnegative discount turn two-sided pointwise epsilon bounds into two-sided discount*epsilon bounds for the max-over-actions Bellman operator at every state. Native, kernel-checked, and axiom-free on D63.
value/signed-optimality-step-additively-contractive
value/signed-optimality-step-additively-contractive.{u, v} :
(S : Type u) (A : Type v) (states : Finset S) (actions : Finset A)
(transition : S → A → S → ℚ) (reward : S → A → ℚ) (discount : ℚ)
(discount-nonnegative : 0 ≤ discount)
(fallback : S → A)
(fallback-admissible : ∀ (state : S), fallback state ∈ actions)
(transition-nonnegative : ∀ (state : S), ∀ (action : A), ∀ (next-state : S), 0 ≤ transition state action next-state)
(normalized : ∀ (state : S), ∀ (action : A), probability/signed-total-mass S states (transition state action) = 1)
(left-value right-value : S → ℚ) (epsilon : ℚ)
(left-pointwise : ∀ (state : S), left-value state ≤ right-value state + epsilon)
(right-pointwise : ∀ (state : S), right-value state ≤ left-value state + epsilon)
(state : S)
→ proposition/conjunction (step₁ ≤ step + discount · epsilon) (step ≤ step₁ + 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 transition reward discount value state₁ action) right-value state
where step₁ := value/signed-optimality-step S A actions fallback (fun value => fun state₁ => fun action => bellman/signed-action-backup S A states transition reward discount value state₁ action) left-value state+ = signed/add0 = signed/zero1 = signed/one= = signed/equivalent: equality of rational valuesFinset = finset-data/Finset· = signed/multiplyℚ = signed/SignedRational∈ = finset-data/to-set: membership in a finite set≤ = signed/at-most