Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-value-optimality

Finite types, distributions and Markov chainssrc/rainbow/math/finite/bellman_value_optimality.clj3 definitions, 7 theorems

Normalized finite NNRAT expectation bounds and Bellman contractions. Transition normalization is expressed directly as equivalence of each finite row total with nnrat/one. All additive estimates are subtraction free. The optimality-step proof delegates finite-argmax transport to the opaque unfold-based nonexpansiveness theorem. Native and axiom-free on D63.

probability/nnrat-total-mass.{u} :
  (A : Type u) (source : Finset A) (mass : A → ℚ≥0)
  → ℚ≥0

markov/nnrat-rows-normalized.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (transition : S → A → S → ℚ≥0)
  → Prop

value/nnrat-contraction-radius :
  (x₁ x₂ : ℚ≥0) (x₃ : ℕ)
  → ℚ≥0

nnrat/multiply-distributes-add-left :
  (factor left right : ℚ≥0)
  → factor · (left + right) = factor · left + factor · right

probability/nnrat-expectation-add-constant.{u} :
  (A : Type u) (source : Finset A) (mass value : A → ℚ≥0) (epsilon : ℚ≥0)
  → expectation (fun state => value state + epsilon) = expectation value + probability/nnrat-total-mass A source mass · epsilon
  where expectation := probability/nnrat-expectation A source mass

probability/nnrat-expectation-additive-upper-bound-normalized.{u} :
  (A : Type u) (source : Finset A) (mass : A → ℚ≥0)
  (normalized : probability/nnrat-total-mass A source mass = 1)
  (lower-value upper-value : A → ℚ≥0) (epsilon : ℚ≥0)
  (pointwise : ∀ (state : A), lower-value state ≤ upper-value state + epsilon)
  → expectation lower-value ≤ expectation upper-value + epsilon
  where expectation := probability/nnrat-expectation A source mass

bellman/nnrat-action-backup-additive-upper-bound.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (transition : S → A → S → ℚ≥0)
  (reward : S → A → ℚ≥0) (discount : ℚ≥0) (left-value right-value : S → ℚ≥0)
  (epsilon : ℚ≥0)
  (left-pointwise : ∀ (next-state : S), left-value next-state ≤ right-value next-state + epsilon)
  (state : S) (action : A)
  (row-normalized : probability/nnrat-total-mass S states (transition state action) = 1)
  → backup left-value state action ≤ backup right-value state action + discount · epsilon
  where backup := bellman/nnrat-action-backup S A states transition reward discount

bellman/nnrat-action-backup-additively-contractive.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (transition : S → A → S → ℚ≥0)
  (reward : S → A → ℚ≥0) (discount : ℚ≥0) (left-value right-value : S → ℚ≥0)
  (epsilon : ℚ≥0)
  (left-pointwise : ∀ (next-state : S), left-value next-state ≤ right-value next-state + epsilon)
  (right-pointwise : ∀ (next-state : S), right-value next-state ≤ left-value next-state + epsilon)
  (state : S) (action : A)
  (row-normalized : probability/nnrat-total-mass S states (transition state action) = 1)
  → proposition/conjunction (backup₁ ≤ backup + discount · epsilon) (backup ≤ backup₁ + discount · epsilon)
  where backup := bellman/nnrat-action-backup S A states transition reward discount right-value state action
  where backup₁ := bellman/nnrat-action-backup S A states transition reward discount left-value state action

value/nnrat-optimality-step-additively-contractive.{u, v} :
  (S : Type u) (A : Type v) (states : Finset S) (actions : Finset A)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ≥0) (discount : ℚ≥0)
  (fallback : S → A)
  (fallback-admissible : ∀ (state : S), fallback state ∈ actions)
  (normalized : markov/nnrat-rows-normalized S A states transition)
  (left-value right-value : S → ℚ≥0) (epsilon : ℚ≥0)
  (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/nnrat-optimality-step S A actions fallback (bellman/nnrat-action-backup S A states transition reward discount) right-value state
  where step₁ := value/nnrat-optimality-step S A actions fallback (bellman/nnrat-action-backup S A states transition reward discount) left-value state

analysis/nnrat-contraction-radius-converges :
  (ap gp : ℕ) (initial-error : ℚ≥0)
  (initial-bound : radius 0 ≤ nnrat/general-harmonic ap gp 0)
  → analysis/rate-null (radius) (fun k => nat/multiply (data/succ ap) k)
  where radius := value/nnrat-vi-error-radius (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))) initial-error