Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-signed-policy-optimal

Finite types, distributions and Markov chainssrc/rainbow/math/finite/bellman_signed_policy_optimal.clj0 definitions, 8 theorems

Concrete signed greedy-policy optimality for finite Bellman models. Ordinary normalized nnrat transition rows are embedded into signed rationals. For any fixed state-to-action policy, the resulting signed action-backup operator is additively contractive. The finite signed sup metric and exact inverse-gap certificate therefore make its fixed point unique. Applying that result to the finite signed argmax policy proves that any separately supplied fixed-policy value is pointwise equivalent to the assumed Bellman optimal fixed value. Fixed-point existence and executable policy evaluation remain premises or open implementation obligations. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.bellman-signed-fixed-point-uniqueness

value/nnrat-transition-signed-policy-step-additively-contractive.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (transition : S → A → S → ℚ≥0)
  (reward : S → A → ℚ) (discount : ℚ≥0)
  (normalized : ∀ (state : S), ∀ (action : A), probability/nnrat-total-mass S states (transition state action) = 1)
  (policy : S → A) (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 ((fun value => fun state₁ => (fun value₁ => fun state₂ => fun action => backup value₁ state₂ action) value state₁ (policy state₁)) left-value state ≤ (fun value => fun state₁ => (fun value₁ => fun state₂ => fun action => backup₁ value₁ state₂ action) value state₁ (policy state₁)) right-value state + signed/from-nnrat discount · epsilon) ((fun value => fun state₁ => (fun value₁ => fun state₂ => fun action => backup value₁ state₂ action) value state₁ (policy state₁)) right-value state ≤ (fun value => fun state₁ => (fun value₁ => fun state₂ => fun action => backup₁ value₁ state₂ action) value state₁ (policy state₁)) left-value state + signed/from-nnrat discount · epsilon)
  where backup := bellman/signed-action-backup S A states (fun state₃ => fun action₁ => fun next-state => signed/from-nnrat (…⟨1⟩ …⟨1⟩ …⟨1⟩ …⟨1⟩)) reward (signed/from-nnrat discount)
  where backup₁ := bellman/signed-action-backup S A states (fun state₃ => fun action₁ => fun next-state => …⟨1⟩ …⟨7⟩) reward (signed/from-nnrat discount)

value/nnrat-transition-signed-policy-fixed-point-sup-distance-self-bound.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S)
  (state-covered : ∀ (state : S), state ∈ states)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ) (discount : ℚ≥0)
  (normalized : ∀ (state : S), ∀ (action : A), probability/nnrat-total-mass S states (transition state action) = 1)
  (policy : S → A) (fixed-value : S → ℚ)
  (fixed-point : ∀ (state : S), (fun value => fun state₁ => (fun value₁ => fun state₂ => fun action => bellman/signed-action-backup S A states (fun state₃ => fun action₁ => fun next-state => signed/from-nnrat (…⟨1⟩ …⟨1⟩ …⟨1⟩ …⟨1⟩)) reward (signed/from-nnrat discount) value₁ state₂ action) value state₁ (policy state₁)) fixed-value state = fixed-value state)
  (candidate : S → ℚ)
  → distance ≤ metric/finite-signed-sup-distance S states candidate ((fun value => fun state => (fun value₁ => fun state₁ => fun action => backup value₁ state₁ action) value state (policy state)) candidate) + signed/from-nnrat discount · distance
  where backup := bellman/signed-action-backup S A states (fun state₂ => fun action₁ => fun next-state => …⟨1⟩ …⟨7⟩) reward (signed/from-nnrat discount)
  where distance := metric/finite-signed-sup-distance S states candidate fixed-value

value/nnrat-transition-signed-policy-fixed-point-residual-bound.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S)
  (state-covered : ∀ (state : S), state ∈ states)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ) (discount : ℚ≥0)
  (normalized : ∀ (state : S), ∀ (action : A), probability/nnrat-total-mass S states (transition state action) = 1)
  (policy : S → A) (fixed-value : S → ℚ)
  (fixed-point : ∀ (state : S), (fun value => fun state₁ => (fun value₁ => fun state₂ => fun action => bellman/signed-action-backup S A states (fun state₃ => fun action₁ => fun next-state => signed/from-nnrat (…⟨1⟩ …⟨1⟩ …⟨1⟩ …⟨1⟩)) reward (signed/from-nnrat discount) value₁ state₂ action) value state₁ (policy state₁)) fixed-value state = fixed-value state)
  (candidate : S → ℚ) (gap inverse : ℚ)
  (inverse-nonnegative : 0 ≤ inverse)
  (discount-plus-gap-one : signed/from-nnrat discount + gap = 1)
  (inverse-times-gap-one : inverse · gap = 1)
  → distance fixed-value ≤ inverse · distance ((fun value => fun state => (fun value₁ => fun state₁ => fun action => backup value₁ state₁ action) value state (policy state)) candidate)
  where backup := bellman/signed-action-backup S A states (fun state₂ => fun action₁ => fun next-state => …⟨1⟩ …⟨7⟩) reward (signed/from-nnrat discount)
  where distance := metric/finite-signed-sup-distance S states candidate

value/nnrat-transition-signed-policy-fixed-point-stopping-certificate.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S)
  (state-covered : ∀ (state : S), state ∈ states)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ) (discount : ℚ≥0)
  (normalized : ∀ (state : S), ∀ (action : A), probability/nnrat-total-mass S states (transition state action) = 1)
  (policy : S → A) (fixed-value : S → ℚ)
  (fixed-point : ∀ (state : S), (fun value => fun state₁ => (fun value₁ => fun state₂ => fun action => bellman/signed-action-backup S A states (fun state₃ => fun action₁ => fun next-state => signed/from-nnrat (…⟨1⟩ …⟨1⟩ …⟨1⟩ …⟨1⟩)) reward (signed/from-nnrat discount) value₁ state₂ action) value state₁ (policy state₁)) fixed-value state = fixed-value state)
  (candidate : S → ℚ) (gap inverse : ℚ)
  (inverse-nonnegative : 0 ≤ inverse)
  (discount-plus-gap-one : signed/from-nnrat discount + gap = 1)
  (inverse-times-gap-one : inverse · gap = 1)
  (threshold : ℚ)
  (residual-at-most-threshold : distance ((fun value => fun state => (fun value₁ => fun state₁ => fun action => backup value₁ state₁ action) value state (policy state)) candidate) ≤ threshold)
  → distance fixed-value ≤ inverse · threshold
  where backup := bellman/signed-action-backup S A states (fun state₂ => fun action₁ => fun next-state => signed/from-nnrat (…⟨1⟩ …⟨1⟩ …⟨1⟩ …⟨1⟩)) reward (signed/from-nnrat discount)
  where distance := metric/finite-signed-sup-distance S states candidate

value/nnrat-transition-signed-policy-fixed-points-unique.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S)
  (state-covered : ∀ (state : S), state ∈ states)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ) (discount : ℚ≥0)
  (normalized : ∀ (state : S), ∀ (action : A), probability/nnrat-total-mass S states (transition state action) = 1)
  (policy : S → A) (left : S → ℚ)
  (left-fixed : ∀ (state : S), (fun value => fun state₁ => (fun value₁ => fun state₂ => fun action => backup value₁ state₂ action) value state₁ (policy state₁)) left state = left state)
  (right : S → ℚ)
  (right-fixed : ∀ (state : S), (fun value => fun state₁ => (fun value₁ => fun state₂ => fun action => backup value₁ state₂ action) value state₁ (policy state₁)) right state = right state)
  (gap inverse : ℚ)
  (inverse-nonnegative : 0 ≤ inverse)
  (discount-plus-gap-one : signed/from-nnrat discount + gap = 1)
  (inverse-times-gap-one : inverse · gap = 1)
  (state : S)
  → left state = right state
  where backup := bellman/signed-action-backup S A states (fun state₃ => fun action₁ => fun next-state => signed/from-nnrat (…⟨1⟩ …⟨1⟩ …⟨1⟩ …⟨1⟩)) reward (signed/from-nnrat discount)

value/nnrat-transition-signed-greedy-policy-value-is-optimal.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S)
  (state-covered : ∀ (state : S), state ∈ states)
  (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)
  (optimal-value : S → ℚ)
  (optimal-fixed : ∀ (state : S), (fun value => fun state₁ => value/signed-optimality-step S A actions fallback (fun value₁ => fun state₂ => fun action => backup value₁ state₂ action) value state₁) optimal-value state = optimal-value state)
  (policy-value : S → ℚ)
  (policy-value-fixed : ∀ (state : S), (fun value => fun state₁ => (fun value₁ => fun state₂ => fun action => backup value₁ state₂ action) value state₁ ((fun state₂ => value/signed-greedy-action S A actions fallback (fun value₁ => fun state₃ => fun action => backup₁ value₁ state₃ action) optimal-value state₂) state₁)) policy-value state = policy-value state)
  (gap inverse : ℚ)
  (inverse-nonnegative : 0 ≤ inverse)
  (discount-plus-gap-one : signed/from-nnrat discount + gap = 1)
  (inverse-times-gap-one : inverse · gap = 1)
  (state : S)
  → policy-value state = optimal-value state
  where backup := bellman/signed-action-backup S A states (fun state₃ => fun action₁ => fun next-state => signed/from-nnrat (…⟨1⟩ …⟨1⟩ …⟨1⟩ …⟨1⟩)) reward (signed/from-nnrat discount)
  where backup₁ := bellman/signed-action-backup S A states (fun state₄ => fun action₁ => …⟨11⟩) reward (signed/from-nnrat discount)

value/nnrat-transition-signed-greedy-policy-optimal-certificate.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S)
  (state-covered : ∀ (state : S), state ∈ states)
  (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)
  (optimal-value : S → ℚ)
  (optimal-fixed : ∀ (state : S), (fun value => fun state₁ => value/signed-optimality-step S A actions fallback (fun value₁ => fun state₂ => fun action => bellman/signed-action-backup S A states (fun state₃ => fun action₁ => fun next-state => signed/from-nnrat (…⟨1⟩ …⟨1⟩ …⟨1⟩ …⟨1⟩)) reward (signed/from-nnrat discount) value₁ state₂ action) value state₁) optimal-value state = optimal-value state)
  (policy-value : S → ℚ)
  (policy-value-fixed : ∀ (state : S), (fun value => fun state₁ => (fun value₁ => fun state₂ => fun action => bellman/signed-action-backup S A states (fun state₃ => fun action₁ => fun next-state => signed/from-nnrat (…⟨1⟩ …⟨1⟩ …⟨1⟩ …⟨1⟩)) reward (signed/from-nnrat discount) value₁ state₂ action) value state₁ ((fun state₂ => value/signed-greedy-action S A actions fallback (fun value₁ => fun state₃ => fun action => backup value₁ state₃ action) optimal-value state₂) state₁)) policy-value state = policy-value state)
  (gap inverse : ℚ)
  (inverse-nonnegative : 0 ≤ inverse)
  (discount-plus-gap-one : signed/from-nnrat discount + gap = 1)
  (inverse-times-gap-one : inverse · gap = 1)
  → proposition/conjunction (∀ (state : S), (fun state₁ => action state₁) state ∈ actions) (∀ (state : S), policy-value state = optimal-value state)
  where action := value/signed-greedy-action S A actions fallback (fun value => fun state₂ => fun action => bellman/signed-action-backup S A states (fun state₃ => fun action₁ => fun next-state => signed/from-nnrat (…⟨1⟩ …⟨1⟩ …⟨1⟩ …⟨1⟩)) reward (signed/from-nnrat discount) value state₂ action) optimal-value
  where backup := bellman/signed-action-backup S A states (fun state₄ => fun action₁ => …⟨11⟩) reward (signed/from-nnrat discount)

value/nnrat-transition-signed-stationary-policy-value-is-optimal.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S)
  (state-covered : ∀ (state : S), state ∈ states)
  (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)
  (policy : S → A)
  (policy-admissible : ∀ (state : S), policy state ∈ actions)
  (policy-value : S → ℚ)
  (policy-value-fixed : ∀ (state : S), (fun value => fun state₁ => fun action => 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 state₁ action) policy-value state (policy state) = policy-value state)
  (greedy-consistent : ∀ (state : S), (fun value => fun state₁ => fun action => 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 state₁ action) policy-value state (policy state) = step policy-value state)
  (optimal-value : S → ℚ)
  (optimal-fixed : ∀ (state : S), step optimal-value state = optimal-value state)
  (gap inverse : ℚ)
  (inverse-nonnegative : 0 ≤ inverse)
  (discount-plus-gap-one : signed/from-nnrat discount + gap = 1)
  (inverse-times-gap-one : inverse · gap = 1)
  (state : S)
  → policy-value state = optimal-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 (fun state₂ => fun action₁ => fun next-state => signed/from-nnrat (transition state₂ action₁ next-state)) reward (signed/from-nnrat discount) value state₁ action)