Reference · Algorithm guarantees

rainbow.algorithms.proofs.bellman-scaled-fixed-point-uniqueness

Algorithm guaranteessrc/rainbow/algorithms/proofs/bellman_scaled_fixed_point_uniqueness.clj0 definitions, 10 theorems

Constructive uniqueness of scaled fixed points for finite Bellman numerators.

nat/at-most-antisymmetric :
  (left right : ℕ)
  (left-right : left ≤ right)
  (right-left : right ≤ left)
  → left = right

nat/at-most-strict-below-transitive :
  (left middle right : ℕ)
  (first : left ≤ middle)
  (second : nat/strict-below middle right)
  → nat/strict-below left right

nat/positive-right-of-strict-below :
  (left right : ℕ) (ordered : nat/strict-below left right)
  → nat/strict-below 0 right

nat/multiply-right-strict-monotone-positive :
  (factor left right : ℕ) (ordered : nat/strict-below left right)
  (factor-positive : nat/strict-below 0 factor)
  → nat/strict-below (nat/multiply left factor) (nat/multiply right factor)

nat/recursive-max-multiply-left :
  (factor left right : ℕ)
  → nat/recursive-max (nat/multiply factor left) (nat/multiply factor right) = nat/multiply factor (nat/recursive-max left right)

list/nat-map-max-multiply-left.{u} :
  (A : Type u) (factor : ℕ) (mapping : A → ℕ) (source : List A)
  → list/nat-map-max A (fun value => nat/multiply factor (mapping value)) source = nat/multiply factor (list/nat-map-max A mapping source)

metric/finite-sup-distance-multiply-left.{u} :
  (A : Type u) (source : Finset A) (factor : ℕ) (left right : A → ℕ)
  → metric/finite-sup-distance A source (fun state => nat/multiply factor (left state)) (fun state => nat/multiply factor (right state)) = nat/multiply factor (distance)
  where distance := metric/finite-sup-distance A source left right

metric/scaled-contraction-scaled-fixed-points-have-zero-sup-distance.{u} :
  (A : Type u) (source : Finset A) (scale discount : ℕ) (transform : (A → ℕ) → A → ℕ)
  (left right : A → ℕ) (discount-below-scale : nat/strict-below discount scale)
  (contractive-bound : ∀ (candidate-left : A → ℕ), ∀ (candidate-right : A → ℕ), metric/finite-sup-distance A source (transform candidate-left) (transform candidate-right) ≤ nat/multiply discount (nat/multiply scale (metric/finite-sup-distance A source candidate-left candidate-right)))
  (left-scaled-fixed : ∀ (state : A), ∀ (member : state ∈ source), transform left state = (fun state₁ => nat/multiply (nat/multiply scale scale) (left state₁)) state)
  (right-scaled-fixed : ∀ (state : A), ∀ (member : state ∈ source), transform right state = (fun state₁ => nat/multiply (nat/multiply scale scale) (right state₁)) state)
  → metric/finite-sup-distance A source left right = 0

bellman/fixed-policy-scaled-fixed-points-have-zero-sup-distance.{u} :
  (A : Type u) (scale : ℕ) (source : Finset A) (transition : A → A → ℕ) (reward : A → ℕ)
  (discount : ℕ) (normalized : markov/rows-normalized-at A scale source transition)
  (discount-below-scale : nat/strict-below discount scale) (left right : A → ℕ)
  (left-scaled-fixed : ∀ (state : A), ∀ (member : state ∈ source), (fun state₁ => numerator left state₁) state = (fun state₁ => nat/multiply (nat/multiply scale scale) (left state₁)) state)
  (right-scaled-fixed : ∀ (state : A), ∀ (member : state ∈ source), (fun state₁ => numerator right state₁) state = (fun state₁ => nat/multiply (nat/multiply scale scale) (right state₁)) state)
  → metric/finite-sup-distance A source left right = 0
  where numerator := bellman/fixed-policy-numerator A scale source transition reward discount

bellman/fixed-policy-scaled-fixed-points-unique-on-support.{u} :
  (A : Type u) (scale : ℕ) (source : Finset A) (transition : A → A → ℕ) (reward : A → ℕ)
  (discount : ℕ) (normalized : markov/rows-normalized-at A scale source transition)
  (discount-below-scale : nat/strict-below discount scale) (left right : A → ℕ)
  (left-scaled-fixed : ∀ (state : A), ∀ (member : state ∈ source), (fun state₁ => numerator left state₁) state = (fun state₁ => nat/multiply (nat/multiply scale scale) (left state₁)) state)
  (right-scaled-fixed : ∀ (state : A), ∀ (member : state ∈ source), (fun state₁ => numerator right state₁) state = (fun state₁ => nat/multiply (nat/multiply scale scale) (right state₁)) state)
  (state : A)
  (member : state ∈ source)
  → left state = right state
  where numerator := bellman/fixed-policy-numerator A scale source transition reward discount