Reference · Finite types, distributions and Markov chains

rainbow.math.finite.bellman

Finite types, distributions and Markov chainssrc/rainbow/math/finite/bellman.clj8 definitions, 7 theorems

Exact scaled finite transition rows and fixed-policy Bellman numerators.

markov/row-total.{u} :
  (A : Type u) (source : Finset A) (transition : A → A → ℕ) (state : A)
  → ℕ

markov/rows-normalized-at.{u} :
  (A : Type u) (scale : ℕ) (source : Finset A) (transition : A → A → ℕ)
  → Prop

bellman/output-scale :
  (x₁ : ℕ)
  → ℕ

bellman/fixed-policy-numerator.{u} :
  (A : Type u) (scale : ℕ) (source : Finset A) (transition : A → A → ℕ) (reward : A → ℕ)
  (discount : ℕ) (value : A → ℕ) (x₁ : A)
  → ℕ

or-example/two-state-space :
  → Finset ℕ

or-example/uniform-mass :
  (x₁ : ℕ)
  → ℕ

or-example/uniform-transition :
  (x₁ x₂ : ℕ)
  → ℕ

or-example/identity-value :
  (x₁ : ℕ)
  → ℕ

probability/two-state-uniform-normalized :
  → probability/normalized-at ℕ 2 ahof-d2/grid or-example/uniform-mass

probability/two-state-identity-expectation :
  → probability/expectation-numerator ℕ ahof-d2/grid or-example/uniform-mass audit-ex/outcomes = 1

markov/two-state-rows-normalized :
  → markov/rows-normalized-at ℕ 2 ahof-d2/grid or-example/uniform-transition

bellman/two-state-state-one-result :
  → bellman/fixed-policy-numerator ℕ 2 ahof-d2/grid or-example/uniform-transition audit-ex/outcomes 1 audit-ex/outcomes 1 = 5

bellman/zero-data.{u} :
  (A : Type u) (scale : ℕ) (source : Finset A) (transition : A → A → ℕ) (discount : ℕ)
  (state : A)
  → bellman/fixed-policy-numerator A scale source transition (fun x₇ => 0) discount (fun x₈ => 0) state = 0

bellman/zero-discount.{u} :
  (A : Type u) (scale : ℕ) (source : Finset A) (transition : A → A → ℕ)
  (reward value : A → ℕ) (state : A)
  → bellman/fixed-policy-numerator A scale source transition reward 0 value state = nat/multiply (reward state) (nat/multiply scale scale)

bellman/fixed-policy-monotone.{u} :
  (A : Type u) (scale : ℕ) (source : Finset A) (transition : A → A → ℕ) (reward : A → ℕ)
  (discount : ℕ) (left right : A → ℕ)
  (ordered : ∀ (state : A), left state ≤ right state)
  (state : A)
  → numerator left state ≤ numerator right state
  where numerator := bellman/fixed-policy-numerator A scale source transition reward discount