Reference · Algorithm guarantees

rainbow.algorithms.proofs.bellman-contraction

Algorithm guaranteessrc/rainbow/algorithms/proofs/bellman_contraction.clj0 definitions, 5 theorems

Finite fixed-policy Bellman contraction over exact natural numerators.

list/nat-map-sum-distance-bound-by-on.{u} :
  (A : Type u) (left right bound : A → ℕ) (source : List A)
  (pointwise : ∀ (value : A), ∀ (member : list/membership A source value), nat/distance (left value) (right value) ≤ bound value)
  → nat/distance (list/nat-map-sum A left source) (list/nat-map-sum A right source) ≤ list/nat-map-sum A bound source

probability/expectation-distance-bound-on.{u} :
  (A : Type u) (source : Finset A) (mass left right : A → ℕ) (epsilon : ℕ)
  (pointwise : ∀ (state : A), ∀ (member : state ∈ source), nat/distance (left state) (right state) ≤ epsilon)
  → nat/distance (numerator₁) (numerator) ≤ nat/multiply (probability/weight-total A source mass) epsilon
  where numerator := probability/expectation-numerator A source mass right
  where numerator₁ := probability/expectation-numerator A source mass left

bellman/fixed-policy-pointwise-contraction.{u} :
  (A : Type u) (scale : ℕ) (source : Finset A) (transition : A → A → ℕ) (reward : A → ℕ)
  (discount : ℕ) (left right : A → ℕ) (epsilon : ℕ)
  (normalized : markov/rows-normalized-at A scale source transition)
  (pointwise : ∀ (next : A), ∀ (member : next ∈ source), nat/distance (left next) (right next) ≤ epsilon)
  (state : A)
  → nat/distance (numerator₁) (numerator) ≤ nat/multiply discount (nat/multiply scale epsilon)
  where numerator := bellman/fixed-policy-numerator A scale source transition reward discount right state
  where numerator₁ := bellman/fixed-policy-numerator A scale source transition reward discount left state

bellman/fixed-policy-sup-contraction.{u} :
  (A : Type u) (scale : ℕ) (source : Finset A) (transition : A → A → ℕ) (reward : A → ℕ)
  (discount : ℕ) (left right : A → ℕ)
  (normalized : markov/rows-normalized-at A scale source transition)
  → metric/finite-sup-distance A source (fun state => numerator₁ state) (fun state => numerator state) ≤ nat/multiply discount (multiply)
  where multiply := nat/multiply scale (metric/finite-sup-distance A source left right)
  where numerator := bellman/fixed-policy-numerator A scale source transition reward discount right
  where numerator₁ := bellman/fixed-policy-numerator A scale source transition reward discount left

bellman/two-state-contraction-example :
  → metric/finite-sup-distance ℕ ahof-d2/grid (fun state => numerator state) (fun state => bellman/fixed-policy-numerator ℕ 2 ahof-d2/grid or-example/uniform-transition audit-ex/outcomes 1 (fun x₄ => 0) state) ≤ 2
  where numerator := bellman/fixed-policy-numerator ℕ 2 ahof-d2/grid or-example/uniform-transition audit-ex/outcomes 1 audit-ex/outcomes