Reference · Rationals

rainbow.math.rational.bellman

Rationalssrc/rainbow/math/rational/bellman.clj7 definitions, 14 theorems

Finite fixed-policy Bellman evaluation over nonnegative rational proof data.

bellman/nnrat-fixed-policy.{u} :
  (A : Type u) (source : Finset A) (transition : A → A → ℚ≥0) (reward : A → ℚ≥0)
  (discount : ℚ≥0) (value : A → ℚ≥0) (x₁ : A)
  → ℚ≥0

bellman/nnrat-value-iterate.{u} :
  (A : Type u) (source : Finset A) (transition : A → A → ℚ≥0) (reward : A → ℚ≥0)
  (discount : ℚ≥0) (x₁ : ℕ) (x₂ : A → ℚ≥0) (x₃ : A)
  → ℚ≥0

or-example/nnrat-deterministic-transition :
  (x₁ x₂ : ℕ)
  → ℚ≥0

or-example/nnrat-identity-reward :
  (x₁ : ℕ)
  → ℚ≥0

or-example/nnrat-zero-value :
  (x₁ : ℕ)
  → ℚ≥0

or-example/nnrat-step-one-value :
  (x₁ : ℕ)
  → ℚ≥0

or-example/nnrat-two-step-value :
  (x₁ : ℕ)
  → ℚ≥0

bellman/two-state-first-step-zero :
  → or-example/nnrat-step-one-value 0 = 0

bellman/two-state-first-step-one :
  → or-example/nnrat-step-one-value 1 = 1

bellman/two-state-compact-second-step-zero :
  → or-example/nnrat-identity-reward 0 + nnrat/half · probability/nnrat-expectation ℕ ahof-d2/grid (or-example/nnrat-deterministic-transition 0) or-example/nnrat-identity-reward = 0

bellman/two-state-compact-second-step-one :
  → or-example/nnrat-identity-reward 1 + nnrat/half · probability/nnrat-expectation ℕ ahof-d2/grid (or-example/nnrat-deterministic-transition 1) or-example/nnrat-identity-reward = 3/2

probability/two-state-step-one-expectation-zero :
  → expectation or-example/nnrat-step-one-value = expectation or-example/nnrat-identity-reward
  where expectation := probability/nnrat-expectation ℕ ahof-d2/grid (or-example/nnrat-deterministic-transition 0)

probability/two-state-step-one-expectation-one :
  → expectation or-example/nnrat-step-one-value = expectation or-example/nnrat-identity-reward
  where expectation := probability/nnrat-expectation ℕ ahof-d2/grid (or-example/nnrat-deterministic-transition 1)

bellman/two-state-second-continuation-zero-congruent :
  → nnrat/half · expectation or-example/nnrat-step-one-value = nnrat/half · expectation or-example/nnrat-identity-reward
  where expectation := probability/nnrat-expectation ℕ ahof-d2/grid (or-example/nnrat-deterministic-transition 0)

bellman/two-state-second-continuation-one-congruent :
  → nnrat/half · expectation or-example/nnrat-step-one-value = nnrat/half · expectation or-example/nnrat-identity-reward
  where expectation := probability/nnrat-expectation ℕ ahof-d2/grid (or-example/nnrat-deterministic-transition 1)

bellman/two-state-second-step-zero-congruent :
  → or-example/nnrat-identity-reward 0 + nnrat/half · expectation or-example/nnrat-step-one-value = or-example/nnrat-identity-reward 0 + nnrat/half · expectation or-example/nnrat-identity-reward
  where expectation := probability/nnrat-expectation ℕ ahof-d2/grid (or-example/nnrat-deterministic-transition 0)

bellman/two-state-second-step-one-congruent :
  → or-example/nnrat-identity-reward 1 + nnrat/half · expectation or-example/nnrat-step-one-value = or-example/nnrat-identity-reward 1 + nnrat/half · expectation or-example/nnrat-identity-reward
  where expectation := probability/nnrat-expectation ℕ ahof-d2/grid (or-example/nnrat-deterministic-transition 1)

bellman/nnrat-fixed-policy-unfold.{u} :
  (A : Type u) (source : Finset A) (transition : A → A → ℚ≥0) (reward : A → ℚ≥0)
  (discount : ℚ≥0) (value : A → ℚ≥0) (state : A)
  → bellman/nnrat-fixed-policy A source transition reward discount value state = reward state + discount · probability/nnrat-expectation A source (transition state) value

bellman/nnrat-value-iterate-zero.{u} :
  (A : Type u) (source : Finset A) (transition : A → A → ℚ≥0) (reward : A → ℚ≥0)
  (discount : ℚ≥0) (initial : A → ℚ≥0) (state : A)
  → bellman/nnrat-value-iterate A source transition reward discount 0 initial state = initial state

bellman/nnrat-fixed-policy-congruent.{u} :
  (A : Type u) (source : Finset A) (transition equivalent-transition : A → A → ℚ≥0)
  (reward equivalent-reward : A → ℚ≥0) (discount equivalent-discount : ℚ≥0)
  (value equivalent-value : A → ℚ≥0)
  (same-transition : ∀ (state : A), ∀ (next : A), transition state next = equivalent-transition state next)
  (same-reward : ∀ (state : A), reward state = equivalent-reward state)
  (same-discount : discount = equivalent-discount)
  (same-value : ∀ (state : A), value state = equivalent-value state)
  (state : A)
  → bellman/nnrat-fixed-policy A source transition reward discount value state = bellman/nnrat-fixed-policy A source equivalent-transition equivalent-reward equivalent-discount equivalent-value state

bellman/two-state-two-step-value-iteration :
  → proposition/conjunction (or-example/nnrat-identity-reward 0 + nnrat/half · expectation = 0) (or-example/nnrat-identity-reward 1 + nnrat/half · expectation₁ = 3/2)
  where expectation := probability/nnrat-expectation ℕ ahof-d2/grid (or-example/nnrat-deterministic-transition 0) or-example/nnrat-step-one-value
  where expectation₁ := probability/nnrat-expectation ℕ ahof-d2/grid (or-example/nnrat-deterministic-transition 1) or-example/nnrat-step-one-value