Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-signed-optimality

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

Generic finite Bellman optimality over exact signed-rational action scores. The operator is parameterized by an action-backup function. Its greedy action is executable over a runtime-length finite carrier; the certificates prove admissibility, dominance of every admissible action and policy, an explicit unfold equation, and preservation of one- and two-sided additive epsilon bounds supplied pointwise for the backup. This module does not yet prove that a transition-weighted signed Bellman action backup supplies those bounds. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.signed-argmax-nonexpansive

value/signed-greedy-action.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ) → S → A → ℚ) (value : S → ℚ) (x₁ : S)
  → A

value/signed-optimality-step.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ) → S → A → ℚ) (value : S → ℚ) (x₁ : S)
  → ℚ

value/signed-greedy-action-is-admissible.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ) → S → A → ℚ)
  (fallback-admissible : ∀ (current : S), fallback current ∈ actions)
  (value : S → ℚ) (state : S)
  → value/signed-greedy-action S A actions fallback backup value state ∈ actions

value/signed-optimality-step-dominates.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ) → S → A → ℚ) (value : S → ℚ) (state : S) (candidate : A)
  (candidate-member : candidate ∈ actions)
  → backup value state candidate ≤ value/signed-optimality-step S A actions fallback backup value state

value/signed-optimality-step-unfold.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ) → S → A → ℚ) (value : S → ℚ) (state : S)
  → value/signed-optimality-step S A actions fallback backup value state = backup value state (value/signed-greedy-action S A actions fallback backup value state)

value/signed-optimality-step-dominates-policy.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (backup : (S → ℚ) → S → A → ℚ) (value : S → ℚ) (policy : S → A)
  (policy-admissible : ∀ (current : S), policy current ∈ actions)
  (state : S)
  → backup value state (policy state) ≤ value/signed-optimality-step S A actions fallback backup value state

value/signed-optimality-step-additive-upper-bound.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (fallback-admissible : ∀ (current : S), fallback current ∈ actions)
  (backup : (S → ℚ) → S → A → ℚ) (left-value right-value : S → ℚ) (epsilon : ℚ)
  (state : S)
  (pointwise : ∀ (action : A), ∀ (member : action ∈ actions), backup left-value state action ≤ backup right-value state action + epsilon)
  → step left-value state ≤ step right-value state + epsilon
  where step := value/signed-optimality-step S A actions fallback backup

value/signed-optimality-step-additively-nonexpansive.{u, v} :
  (S : Type u) (A : Type v) (actions : Finset A) (fallback : S → A)
  (fallback-admissible : ∀ (current : S), fallback current ∈ actions)
  (backup : (S → ℚ) → S → A → ℚ) (left-value right-value : S → ℚ) (epsilon : ℚ)
  (state : S)
  (left-pointwise : ∀ (action : A), ∀ (member : action ∈ actions), backup left-value state action ≤ backup right-value state action + epsilon)
  (right-pointwise : ∀ (action : A), ∀ (member : action ∈ actions), backup right-value state action ≤ backup left-value state action + epsilon)
  → proposition/conjunction (step₁ ≤ step + epsilon) (step ≤ step₁ + epsilon)
  where step := value/signed-optimality-step S A actions fallback backup right-value state
  where step₁ := value/signed-optimality-step S A actions fallback backup left-value state