Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-signed-transition-approximate-optimality

Finite types, distributions and Markov chainssrc/rainbow/math/finite/bellman_signed_transition_approximate_optimality.clj0 definitions, 4 theorems

Constructive approximate optimality for normalized finite signed MDPs. The witness is the actual generic iterate of the named concrete Bellman optimality operator. For discount gamma=(a+1)/(a+g+2), an initial residual bounded by the corresponding general-harmonic radius yields, at horizon (a+1)*k, a pointwise Bellman residual at most 1/(k+1). A finite-sup theorem turns that whole-carrier result into a scalar certificate over the supplied finite state source. No exact fixed point or choice principle is assumed. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.bellman-signed-approximate-optimalitymath.finite.bellman-signed-transition-operatormath.finite.signed-approximate-fixed-point-sup

value/nnrat-transition-signed-optimality-successive-iterate-additive-radius.{u, v} :
  (discount : ℚ≥0) (S : Type u) (A : Type v) (states : Finset S) (actions : Finset A)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ) (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)
  (initial : S → ℚ) (initial-error : ℚ)
  (initial-close : ∀ (state : S), proposition/conjunction (initial state ≤ operator state + initial-error) (operator state ≤ initial state + initial-error))
  (steps : ℕ) (state : S)
  → proposition/conjunction (iterate₁ ≤ iterate + radius) (iterate ≤ iterate₁ + radius)
  where iterate := value/signed-operator-iterate S (value/nnrat-transition-signed-optimality-operator S A states actions transition reward discount fallback) (data/succ steps) initial state
  where iterate₁ := value/signed-operator-iterate S (value/nnrat-transition-signed-optimality-operator S A states actions transition reward discount fallback) steps initial state
  where operator := value/nnrat-transition-signed-optimality-operator S A states actions transition reward discount fallback initial
  where radius := value/signed-vi-error-radius (signed/from-nnrat discount) initial-error steps

value/nnrat-transition-signed-optimality-approximate-fixed-point-general-rate.{u, v} :
  (ap gp : ℕ) (S : Type u) (A : Type v) (states : Finset S) (actions : Finset A)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ) (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)
  (initial : S → ℚ) (initial-error : ℚ)
  (initial-close : ∀ (state : S), proposition/conjunction (initial state ≤ operator₁ state + initial-error) (operator₁ state ≤ initial state + initial-error))
  (initial-error-nonnegative : 0 ≤ initial-error)
  (initial-bound : initial-error ≤ signed/from-nnrat (nnrat/general-harmonic ap gp 0))
  (index : ℕ) (state : S)
  → proposition/conjunction ((fun steps => value/signed-operator-iterate S (value/nnrat-transition-signed-optimality-operator S A states actions transition reward (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))) fallback) steps initial) ((fun index₁ => nat/multiply (data/succ ap) index₁) index) state ≤ operator + signed/from-nnrat (nnrat/harmonic index)) (operator ≤ (fun steps => value/signed-operator-iterate S (value/nnrat-transition-signed-optimality-operator S A states actions transition reward (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))) fallback) steps initial) ((fun index₁ => nat/multiply (data/succ ap) index₁) index) state + signed/from-nnrat (nnrat/harmonic index))
  where operator := value/nnrat-transition-signed-optimality-operator S A states actions transition reward (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))) fallback ((fun steps => value/signed-operator-iterate S (value/nnrat-transition-signed-optimality-operator S A states actions transition reward (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))) fallback) steps initial) ((fun index₁ => nat/multiply (data/succ ap) index₁) index)) state
  where operator₁ := value/nnrat-transition-signed-optimality-operator S A states actions transition reward (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))) fallback initial

value/nnrat-transition-signed-optimality-approximate-fixed-point-exists-general-rate.{u, v} :
  (ap gp : ℕ) (S : Type u) (A : Type v) (states : Finset S) (actions : Finset A)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ) (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)
  (initial : S → ℚ) (initial-error : ℚ)
  (initial-close : ∀ (state : S), proposition/conjunction (initial state ≤ operator state + initial-error) (operator state ≤ initial state + initial-error))
  (initial-error-nonnegative : 0 ≤ initial-error)
  (initial-bound : initial-error ≤ signed/from-nnrat (nnrat/general-harmonic ap gp 0))
  (index : ℕ)
  → proposition/existence (S → ℚ) (fun candidate => ∀ (state : S), proposition/conjunction (candidate state ≤ value/nnrat-transition-signed-optimality-operator S A states actions transition reward (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))) fallback candidate state + signed/from-nnrat (nnrat/harmonic index)) (value/nnrat-transition-signed-optimality-operator S A states actions transition reward (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))) fallback candidate state ≤ candidate state + signed/from-nnrat (nnrat/harmonic index)))
  where operator := value/nnrat-transition-signed-optimality-operator S A states actions transition reward (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))) fallback initial

value/nnrat-transition-signed-optimality-approximate-fixed-point-sup-general-rate.{u, v} :
  (ap gp : ℕ) (S : Type u) (A : Type v) (states : Finset S) (actions : Finset A)
  (transition : S → A → S → ℚ≥0) (reward : S → A → ℚ) (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)
  (initial : S → ℚ) (initial-error : ℚ)
  (initial-close : ∀ (state : S), proposition/conjunction (initial state ≤ operator₁ state + initial-error) (operator₁ state ≤ initial state + initial-error))
  (initial-error-nonnegative : 0 ≤ initial-error)
  (initial-bound : initial-error ≤ signed/from-nnrat (nnrat/general-harmonic ap gp 0))
  (index : ℕ)
  → metric/finite-signed-sup-distance S states ((fun steps => value/signed-operator-iterate S (value/nnrat-transition-signed-optimality-operator S A states actions transition reward (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))) fallback) steps initial) ((fun index₁ => nat/multiply (data/succ ap) index₁) index)) (operator) ≤ signed/from-nnrat (nnrat/harmonic index)
  where operator := value/nnrat-transition-signed-optimality-operator S A states actions transition reward (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))) fallback ((fun steps => value/signed-operator-iterate S (value/nnrat-transition-signed-optimality-operator S A states actions transition reward (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))) fallback) steps initial) ((fun index₁ => nat/multiply (data/succ ap) index₁) index))
  where operator₁ := value/nnrat-transition-signed-optimality-operator S A states actions transition reward (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))) fallback initial