Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman-signed-value-iteration-general-converges

Finite types, distributions and Markov chainssrc/rainbow/math/finite/bellman_signed_value_iteration_general_converges.clj0 definitions, 6 theorems

General strict-rate convergence for signed Bellman value iteration. Any nnrat rate-null sequence remains rate-null after the Grothendieck embedding. For the canonical strict rational rate gamma = (ap+1)/(ap+gp+2), the exact signed power recurrence is dominated by the embedded general harmonic sequence. It therefore inherits the established modulus `(ap+1)*k`. Transporting that certificate to the signed Bellman error-radius removes the earlier discount-at-most-one-half restriction. The Bellman capstone still assumes a normalized nnrat transition kernel and existence of a signed fixed point. Native, kernel-checked, and axiom-free on D63.

Depends onmath.finite.bellman-signed-value-iteration-converges

analysis/signed-rate-null-from-nnrat :
  (sequence : ℕ → ℚ≥0) (modulus : ℕ → ℕ) (null : analysis/rate-null sequence modulus)
  → analysis/signed-rate-null (fun steps => signed/from-nnrat (sequence steps)) modulus

analysis/signed-general-harmonic-rate-null :
  (ap gp : ℕ)
  → analysis/signed-rate-null (fun steps => signed/from-nnrat (nnrat/general-harmonic ap gp steps)) (fun index => nat/multiply (data/succ ap) index)

signed/nnrat-power-scale-general-harmonic-bound :
  (ap gp : ℕ) (initial-error : ℚ)
  (initial-bound : initial-error ≤ signed/from-nnrat (nnrat/general-harmonic ap gp 0))
  (steps : ℕ)
  → signed/nnrat-power-scale (make) steps initial-error ≤ signed/from-nnrat (nnrat/general-harmonic ap gp steps)
  where make := nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))

analysis/signed-nnrat-power-rate-null-general :
  (ap gp : ℕ) (initial-error : ℚ)
  (initial-error-nonnegative : 0 ≤ initial-error)
  (initial-bound : initial-error ≤ signed/from-nnrat (nnrat/general-harmonic ap gp 0))
  → analysis/signed-rate-null (fun steps => signed/nnrat-power-scale (make) steps initial-error) (fun index => nat/multiply (data/succ ap) index)
  where make := nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))

analysis/signed-vi-error-radius-rate-null-general :
  (ap gp : ℕ) (initial-error : ℚ)
  (initial-error-nonnegative : 0 ≤ initial-error)
  (initial-bound : initial-error ≤ signed/from-nnrat (nnrat/general-harmonic ap gp 0))
  → analysis/signed-rate-null (fun steps => radius steps) (fun index => nat/multiply (data/succ ap) index)
  where radius := value/signed-vi-error-radius (signed/from-nnrat (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp)))) initial-error

value/nnrat-transition-signed-iterate-fixed-point-converges-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)
  (fixed-value : S → ℚ)
  (fixed-point : ∀ (state : S), value/signed-optimality-step S A actions fallback (fun value => fun state₁ => fun action => backup value state₁ action) fixed-value state = fixed-value state)
  (initial : S → ℚ) (initial-error : ℚ)
  (initial-error-nonnegative : 0 ≤ initial-error)
  (initial-bound : initial-error ≤ signed/from-nnrat (nnrat/general-harmonic ap gp 0))
  (initial-close : ∀ (state : S), proposition/conjunction (initial state ≤ fixed-value state + initial-error) (fixed-value state ≤ initial state + initial-error))
  → proposition/conjunction (null) (∀ (steps : ℕ), ∀ (state : S), proposition/conjunction (iterate steps initial state ≤ fixed-value state + (fun steps₁ => value/signed-vi-error-radius (signed/from-nnrat (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp)))) initial-error steps₁) steps) (fixed-value state ≤ iterate₁ steps initial state + (fun steps₁ => value/signed-vi-error-radius (signed/from-nnrat (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp)))) initial-error steps₁) steps))
  where backup := 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 (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp))))
  where iterate := value/signed-iterate 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 (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp)))) value state₁ action)
  where iterate₁ := value/signed-iterate S A actions fallback (fun value => fun state₁ => fun action => bellman/signed-action-backup S A states (fun state₂ => fun action₁ => fun next-state => …⟨1⟩ …⟨7⟩) reward (signed/from-nnrat (nnrat/make (data/succ ap) (algebra/nat-add ap (…⟨1⟩ …⟨1⟩)))) value state₁ action)
  where null := analysis/signed-rate-null (fun steps => value/signed-vi-error-radius (signed/from-nnrat (nnrat/make (data/succ ap) (algebra/nat-add ap (data/succ gp)))) initial-error steps) (fun index => nat/multiply (data/succ ap) index)