Skip to content

Value iteration

StructureMarkov decision process#✓fully proved

A Markov decision process with states in \(S\), actions in \(A\) and values in \(K\) consists of a reward \(r(s, a) \in K\) for taking action \(a\) in state \(s\) and, for all states \(s, s'\) and actions \(a\), a value \(p(s, a, s') \in K\), the probability of moving from \(s\) to \(s'\) under action \(a\).

No condition is imposed here: finiteness of the states and actions, an order on \(K\) and the stochasticity of \(p\) are hypotheses of the results that use them.

structure MDP (S A K : Type*) where
  /-- The reward for taking action `a` in state `s`. -/
  reward : S → A → K
  /-- The probability of moving from `s` to `s'` under action `a`. -/
  prob : S → A → S → K
Used by 32
Used byPolicy improvement step · Values below their Bellman image lie below the policy value · Policy iteration · Improvement stalls exactly at optimal policies · Away from optimality, improvement changes the value · Policy improvement theorem · Policy iteration terminates · Policy iteration never decreases the value · Once optimal, policy iteration stays optimal · The Bellman operator contracts by \(\gamma\) · Bellman optimality operator · Bellman's operator is a contraction · The optimal value solves the Bellman optimality equation · Stopping test · A priori error bound for value iteration · Uniqueness of the solution of the Bellman optimality equation · Uniqueness of the solution of a policy's Bellman equation · Greedy policy · Optimal value of a discounted Markov decision process · Bellman operator of a policy · A policy's Bellman update is at most the optimal one · A policy's value satisfies its Bellman equation · Value of a policy · A greedy policy for the optimal value is optimal · No policy beats the optimal value · Q-value of an action · The greedy action attains the Bellman maximum · Stochastic Markov decision process · Value iteration converges · Value iteration · Tabulated value iteration · Tabulated value iteration is correct

DefinitionStochastic Markov decision process#✓fully proved

A Markov decision process with finitely many states and transition probabilities \(P(s,a,s')\) in a field \(K\) with a linear order is stochastic when \(0 \le P(s,a,s')\) for all states \(s, s'\) and actions \(a\), and \(\sum_{s'} P(s,a,s') = 1\) for every state \(s\) and action \(a\).

def MDP.Stochastic (M : MDP S A K) : Prop :=
  (∀ s a s', 0 ≤ M.prob s a s') ∧ ∀ s a, ∑ s', M.prob s a s' = 1
Uses 1 · Used by 22
Statement usesMarkov decision process
Used byPolicy improvement step · Values below their Bellman image lie below the policy value · Policy iteration · Improvement stalls exactly at optimal policies · Away from optimality, improvement changes the value · Policy improvement theorem · Policy iteration terminates · Policy iteration never decreases the value · Once optimal, policy iteration stays optimal · The Bellman operator contracts by \(\gamma\) · Bellman's operator is a contraction · The optimal value solves the Bellman optimality equation · Stopping test · A priori error bound for value iteration · Uniqueness of the solution of the Bellman optimality equation · Uniqueness of the solution of a policy's Bellman equation · Optimal value of a discounted Markov decision process · A policy's value satisfies its Bellman equation · Value of a policy · A greedy policy for the optimal value is optimal · No policy beats the optimal value · Value iteration converges

DefinitionQ-value of an action#✓fully proved

Let \(M\) be a Markov decision process with a finite set of states \(S\) and with rewards \(r(s,a)\) and transition probabilities \(P(s,a,s')\) in a field \(K\), and let \(\gamma \in K\). The Q-value of action \(a\) in state \(s\) against a value estimate \(V : S \to K\) is \(r(s,a) + \gamma \sum_{s'} P(s,a,s') \, V(s')\).

def qValue (M : MDP S A K) (γ : K) (V : S → K) (s : S) (a : A) : K :=
  M.reward s a + γ * ∑ s', M.prob s a s' * V s'
Uses 1 · Used by 11
Statement usesMarkov decision process
Used byValues below their Bellman image lie below the policy value · The Bellman operator contracts by \(\gamma\) · Bellman optimality operator · Uniqueness of the solution of a policy's Bellman equation · Greedy policy · Bellman operator of a policy · A policy's Bellman update is at most the optimal one · A policy's value satisfies its Bellman equation · Value of a policy · No policy beats the optimal value · The greedy action attains the Bellman maximum

DefinitionBellman optimality operator#✓fully proved

Let \(M\) be a Markov decision process with finitely many states \(s\), a nonempty finite set of actions \(a\), rewards \(r(s, a)\) and transition probabilities \(p(s, a, s')\) in a field \(K\) carrying a linear order, and let \(\gamma \in K\) be a discount factor. The Bellman optimality operator \(T\) sends a function \(V\) from states to \(K\) to the function

\[(TV)(s) = \max_a \Big( r(s, a) + \gamma \sum_{s'} p(s, a, s') V(s') \Big),\]

the largest action value in state \(s\).

def bellman (M : MDP S A K) (γ : K) (V : S → K) : S → K :=
  fun s => Finset.univ.sup' Finset.univ_nonempty (qValue M γ V s)
Uses 2 · Used by 17
Statement usesMarkov decision process · Q-value of an action
Used byImprovement stalls exactly at optimal policies · Policy improvement theorem · The Bellman operator contracts by \(\gamma\) · Bellman's operator is a contraction · The optimal value solves the Bellman optimality equation · Stopping test · A priori error bound for value iteration · Uniqueness of the solution of the Bellman optimality equation · Optimal value of a discounted Markov decision process · A policy's Bellman update is at most the optimal one · A greedy policy for the optimal value is optimal · No policy beats the optimal value · The greedy action attains the Bellman maximum · Value iteration converges · Value iteration · Tabulated value iteration · Tabulated value iteration is correct

DefinitionBellman operator of a policy#✓fully proved

Let \(M\) be a Markov decision process with a finite set of states \(S\), a set of actions \(A\), and rewards \(r(s,a)\) and transition probabilities \(P(s,a,s')\) in a field \(K\), let \(\gamma \in K\) be a discount factor, and let \(\pi : S \to A\) be a deterministic stationary policy. The Bellman operator of \(\pi\) sends a value estimate \(V : S \to K\) to the function \(s \mapsto r(s,\pi(s)) + \gamma \sum_{s'} P(s,\pi(s),s') \, V(s')\).

def policyBellman (M : MDP S A K) (γ : K) (π : S → A) (V : S → K) : S → K :=
  fun s => qValue M γ V s (π s)
Uses 2 · Used by 9
Statement usesMarkov decision process · Q-value of an action
Used byValues below their Bellman image lie below the policy value · Improvement stalls exactly at optimal policies · Policy improvement theorem · Uniqueness of the solution of a policy's Bellman equation · A policy's Bellman update is at most the optimal one · A policy's value satisfies its Bellman equation · Value of a policy · A greedy policy for the optimal value is optimal · No policy beats the optimal value

DefinitionValue iteration#✓fully proved

Let \(M\) be a Markov decision process with finitely many states, a nonempty finite set of actions, and rewards and transition probabilities in a field \(K\) carrying a linear order, let \(\gamma \in K\), and let \(T\) be the Bellman optimality operator of \(M\) with discount \(\gamma\). For \(n \in \mathbb{N}\) and a function \(V\) from states to \(K\), \(n\) steps of value iteration from \(V\) give the \(n\)-fold iterate \(T^n V\), where \(T^0 V = V\).

Evaluated directly, this definition recomputes earlier iterates; tabulated value iteration stores each update instead.

def valueIteration (M : MDP S A K) (γ : K) (n : ℕ) (V : S → K) : S → K :=
  (bellman M γ)^[n] V
Uses 2 · Used by 3
Statement usesMarkov decision process · Bellman optimality operator
Used byA priori error bound for value iteration · Value iteration converges · Tabulated value iteration is correct

DefinitionTabulated value iteration#✓fully proved

Let \(M\) be a Markov decision process with states \(\{0, \dots, m-1\}\), a nonempty finite set of actions, and rewards and transition probabilities in a field \(K\) carrying a linear order, let \(\gamma \in K\), and let \(T\) be the Bellman optimality operator of \(M\) with discount \(\gamma\). Tabulated value iteration takes a number of steps \(n \in \mathbb{N}\) and a vector \(v \in K^m\), read as a function on states: with \(0\) steps it returns \(v\), and with \(k + 1\) steps it computes the vector \(\bigl((Tv)(0), \dots, (Tv)(m-1)\bigr)\) and then runs \(k\) steps from that vector.

Each update is stored as a vector, so update \(k + 1\) reads the stored values of update \(k\).

def valueIterationVec {m : ℕ} (M : MDP (Fin m) A K) (γ : K) : ℕ → Vector K m → Vector K m
  | 0, v => v
  | k + 1, v => valueIterationVec M γ k (Vector.ofFn (bellman M γ fun s => v.get s))
Uses 2 · Used by 1
Statement usesMarkov decision process · Bellman optimality operator
Used byTabulated value iteration is correct

DefinitionGreedy policy#✓fully proved

Let \(M\) be a Markov decision process with finitely many states, a nonempty finite set of actions, and rewards \(r(s, a)\) and transition probabilities \(p(s, a, s')\) in a field \(K\) carrying a linear order, let \(\gamma \in K\), and let \(V\) be a function from states to \(K\). The greedy policy for \(V\) chooses in each state \(s\) an action \(a\) maximizing the action value \(r(s, a) + \gamma \sum_{s'} p(s, a, s') V(s')\); when several actions attain the maximum, one of them is fixed by choice.

noncomputable def greedy (M : MDP S A K) (γ : K) (V : S → K) (s : S) : A :=
  (Finset.univ.exists_max_image (qValue M γ V s) Finset.univ_nonempty).choose
Uses 2 · Used by 5
Statement usesMarkov decision process · Q-value of an action
Used byPolicy improvement step · Improvement stalls exactly at optimal policies · Policy improvement theorem · A greedy policy for the optimal value is optimal · The greedy action attains the Bellman maximum

TheoremTabulated value iteration is correct#✓fully proved

Let \(M\) be a Markov decision process with states \(\{0, \dots, m-1\}\), a nonempty finite set of actions and values in a field \(K\) with a linear order, let \(\gamma \in K\), and let \(T\) be the Bellman optimality operator of \(M\) with discount \(\gamma\). For every \(n \in \mathbb{N}\), every vector \(v \in K^m\) and every state \(s\), entry \(s\) of the vector computed by \(n\) steps of tabulated value iteration from \(v\) equals \((T^n v)(s)\), where \(v\) is read as a function on states.

theorem valueIterationVec_get {m : ℕ} (M : MDP (Fin m) A K) (γ : K) :
    ∀ (n : ℕ) (v : Vector K m) (s : Fin m),
      (valueIterationVec M γ n v).get s = valueIteration M γ n (fun s => v.get s) s
Uses 4
Statement usesMarkov decision process · Value iteration · Tabulated value iteration
Proof usesBellman optimality operator
24 fully proved

Order and contraction facts, in any ordered field

TheoremA policy's Bellman update is at most the optimal one#✓fully proved

Let \(M\) be a Markov decision process with a finite set of states \(S\), a finite nonempty set of actions \(A\), and rewards \(r(s,a)\) and transition probabilities \(P(s,a,s')\) in a field \(K\) with a linear order, let \(\gamma \in K\), and let \(\pi : S \to A\) be a deterministic stationary policy. For every \(V : S \to K\) and every state \(s\), the Bellman operator of \(\pi\) applied to \(V\) is at most the Bellman optimality operator applied to \(V\) at \(s\): \(r(s,\pi(s)) + \gamma \sum_{s'} P(s,\pi(s),s') \, V(s') \le \max_a \bigl(r(s,a) + \gamma \sum_{s'} P(s,a,s') \, V(s')\bigr)\).

theorem policyBellman_le_bellman (π : S → A) (V : S → K) :
    policyBellman M γ π V ≤ bellman M γ V
Uses 4 · Used by 2
Statement usesMarkov decision process · Bellman optimality operator · Bellman operator of a policy
Proof usesQ-value of an action
Used byPolicy improvement theorem · No policy beats the optimal value

TheoremThe greedy action attains the Bellman maximum#✓fully proved

Let \(M\) be a Markov decision process with a finite set of states \(S\), a finite nonempty set of actions, and rewards \(r(s,a)\) and transition probabilities \(P(s,a,s')\) in a field \(K\) with a linear order, and let \(\gamma \in K\). For every \(V : S \to K\) and every state \(s\), the action \(g\) that the greedy policy for \(V\) chooses in \(s\) satisfies \(r(s,g) + \gamma \sum_{s'} P(s,g,s') \, V(s') = \max_a \bigl(r(s,a) + \gamma \sum_{s'} P(s,a,s') \, V(s')\bigr)\), so its action value equals the value of the Bellman optimality operator applied to \(V\) at \(s\).

theorem qValue_greedy (V : S → K) (s : S) :
    qValue M γ V s (greedy M γ V s) = bellman M γ V s
Uses 4 · Used by 3
Statement usesMarkov decision process · Bellman optimality operator · Greedy policy · Q-value of an action
Used byImprovement stalls exactly at optimal policies · Policy improvement theorem · A greedy policy for the optimal value is optimal

TheoremThe Bellman operator contracts by \(\gamma\)#✓fully proved

Let \(M\) be a Markov decision process with finitely many states, a nonempty finite set of actions, and rewards and stochastic transition probabilities in a linearly ordered field \(K\), let \(\gamma \ge 0\) in \(K\), and let \(T\) be the Bellman optimality operator of \(M\) with discount \(\gamma\). If two functions \(V, W\) from states to \(K\) satisfy \(|V(s) - W(s)| \le d\) for every state \(s\), where \(d \in K\), then \(|(TV)(s) - (TW)(s)| \le \gamma d\) for every state \(s\).

theorem abs_bellman_sub_le (hM : M.Stochastic) (hγ : 0 ≤ γ) {V W : S → K} {d : K}
    (h : ∀ s, |V s - W s| ≤ d) (s : S) : |bellman M γ V s - bellman M γ W s| ≤ γ * d
Uses 4 · Used by 1
Statement usesMarkov decision process · Stochastic Markov decision process · Bellman optimality operator
Proof usesQ-value of an action
Used byBellman's operator is a contraction

Real values: contraction, value iteration, optimality

TheoremBellman's operator is a contraction#✓fully proved

Let \(M\) be a Markov decision process with finitely many states, a nonempty finite set of actions, real rewards and stochastic transition probabilities, and let \(0 \le \gamma < 1\). Then the Bellman optimality operator \(T\) of \(M\) with discount \(\gamma\), acting on real-valued functions on the states with the sup metric, is a contraction with constant \(\gamma\): for all such functions \(V\) and \(W\), \(\|TV - TW\|_\infty \le \gamma \|V - W\|_\infty\).

theorem bellman_contracting (hM : M.Stochastic) (hγ0 : 0 ≤ γ) (hγ1 : γ < 1) :
    ContractingWith γ.toNNReal (bellman M γ)
Sources
  • Puterman, Theorem 6.2.3.
Uses 4 · Used by 6
Statement usesMarkov decision process · Stochastic Markov decision process · Bellman optimality operator
Proof usesThe Bellman operator contracts by \(\gamma\)
Used byThe optimal value solves the Bellman optimality equation · Stopping test · A priori error bound for value iteration · Uniqueness of the solution of the Bellman optimality equation · Optimal value of a discounted Markov decision process · Value iteration converges

DefinitionOptimal value of a discounted Markov decision process#✓fully proved

Let \(M\) be a Markov decision process with finitely many states \(S\), finitely many actions (at least one), real rewards \(r(s,a)\), and transition probabilities \(P(s,a,s')\) that are nonnegative and sum to \(1\) over \(s'\), and let \(0 \le \gamma < 1\). The optimal value of \(M\) with discount \(\gamma\) is the unique function \(V^* : S \to \mathbb{R}\) that is a fixed point of the Bellman optimality operator, that is, \(V^*(s) = \max_a \bigl(r(s,a) + \gamma \sum_{s'} P(s,a,s') \, V^*(s')\bigr)\) for every state \(s\). It exists and is unique because this operator is a \(\gamma\)-contraction in the sup metric.

noncomputable def optimalValue (M : MDP S A ℝ) (γ : ℝ) (hM : M.Stochastic) (hγ0 : 0 ≤ γ)
    (hγ1 : γ < 1) : S → ℝ :=
  ContractingWith.fixedPoint _ (bellman_contracting hM hγ0 hγ1)
Uses 4 · Used by 11
Statement usesMarkov decision process · Stochastic Markov decision process · Bellman optimality operator · Bellman's operator is a contraction
Used byImprovement stalls exactly at optimal policies · Away from optimality, improvement changes the value · Policy iteration terminates · Once optimal, policy iteration stays optimal · The optimal value solves the Bellman optimality equation · Stopping test · A priori error bound for value iteration · Uniqueness of the solution of the Bellman optimality equation · A greedy policy for the optimal value is optimal · No policy beats the optimal value · Value iteration converges

DefinitionValue of a policy#✓fully proved

Let \(M\) be a Markov decision process with a finite set of states \(S\), a set of actions \(A\), real rewards \(r(s,a)\), and transition probabilities \(P(s,a,s')\) that are nonnegative and sum to \(1\) over \(s'\), let \(0 \le \gamma < 1\), and let \(\pi : S \to A\) be a deterministic stationary policy. The value of \(\pi\) is the unique function \(V^\pi : S \to \mathbb{R}\) that is a fixed point of the Bellman operator of \(\pi\), that is, \(V^\pi(s) = r(s,\pi(s)) + \gamma \sum_{s'} P(s,\pi(s),s') \, V^\pi(s')\) for every state \(s\). It exists and is unique because this operator is a \(\gamma\)-contraction in the sup metric.

noncomputable def policyValue (M : MDP S A ℝ) (γ : ℝ) (hM : M.Stochastic) (hγ0 : 0 ≤ γ)
    (hγ1 : γ < 1) (π : S → A) : S → ℝ :=
  ContractingWith.fixedPoint _ (policyBellman_contracting hM hγ0 hγ1 π)
Uses 4 · Used by 12
Statement usesMarkov decision process · Stochastic Markov decision process · Bellman operator of a policy · Q-value of an action
Used byPolicy improvement step · Values below their Bellman image lie below the policy value · Improvement stalls exactly at optimal policies · Away from optimality, improvement changes the value · Policy improvement theorem · Policy iteration terminates · Policy iteration never decreases the value · Once optimal, policy iteration stays optimal · Uniqueness of the solution of a policy's Bellman equation · A policy's value satisfies its Bellman equation · A greedy policy for the optimal value is optimal · No policy beats the optimal value

TheoremThe optimal value solves the Bellman optimality equation#✓fully proved

Let \(M\) be a Markov decision process with finitely many states, a nonempty finite set of actions, real rewards and stochastic transition probabilities, and let \(0 \le \gamma < 1\). Then the optimal value \(V^*\) of \(M\) with discount \(\gamma\) is a fixed point of the Bellman optimality operator \(T\) of \(M\) with discount \(\gamma\): \(T V^* = V^*\).

theorem bellman_optimalValue : bellman M γ (optimalValue M γ hM hγ0 hγ1) =
    optimalValue M γ hM hγ0 hγ1
Uses 5 · Used by 2
Statement usesMarkov decision process · Stochastic Markov decision process · Bellman optimality operator · Optimal value of a discounted Markov decision process
Proof usesBellman's operator is a contraction
Used byA greedy policy for the optimal value is optimal · No policy beats the optimal value

TheoremUniqueness of the solution of the Bellman optimality equation#✓fully proved

Let \(M\) be a Markov decision process with finitely many states, a nonempty finite set of actions, real rewards and stochastic transition probabilities, and let \(0 \le \gamma < 1\). If a real-valued function \(V\) on the states satisfies \(TV = V\), where \(T\) is the Bellman optimality operator of \(M\) with discount \(\gamma\), then \(V\) is the optimal value of \(M\) with discount \(\gamma\).

theorem eq_optimalValue_of_bellman_eq {V : S → ℝ} (h : bellman M γ V = V) :
    V = optimalValue M γ hM hγ0 hγ1
Uses 5 · Used by 1
Statement usesMarkov decision process · Stochastic Markov decision process · Bellman optimality operator · Optimal value of a discounted Markov decision process
Proof usesBellman's operator is a contraction
Used byImprovement stalls exactly at optimal policies

TheoremA policy's value satisfies its Bellman equation#✓fully proved

Let \(M\) be a Markov decision process with finitely many states, real rewards \(r(s,a)\), and transition probabilities \(P(s,a,s')\) that are nonnegative and sum to \(1\) over \(s'\), let \(0 \le \gamma < 1\), and let \(\pi\) be a deterministic stationary policy with value \(V^\pi\). Then \(V^\pi\) is a fixed point of the Bellman operator of \(\pi\): for every state \(s\), \(V^\pi(s) = r(s,\pi(s)) + \gamma \sum_{s'} P(s,\pi(s),s') \, V^\pi(s')\).

theorem policyBellman_policyValue (π : S → A) :
    policyBellman M γ π (policyValue M γ hM hγ0 hγ1 π) = policyValue M γ hM hγ0 hγ1 π
Uses 5 · Used by 2
Statement usesMarkov decision process · Stochastic Markov decision process · Bellman operator of a policy · Value of a policy
Proof usesQ-value of an action
Used byImprovement stalls exactly at optimal policies · Policy improvement theorem

TheoremUniqueness of the solution of a policy's Bellman equation#✓fully proved

Let \(M\) be a Markov decision process with finitely many states, real rewards and stochastic transition probabilities, let \(0 \le \gamma < 1\), and let \(\pi\) be a deterministic stationary policy, a map from states to actions. If a real-valued function \(V\) on the states satisfies \(T_\pi V = V\), where \(T_\pi\) is the Bellman operator of \(\pi\) in \(M\) with discount \(\gamma\), then \(V\) is the value of \(\pi\).

theorem eq_policyValue_of_policyBellman_eq (π : S → A) {V : S → ℝ}
    (h : policyBellman M γ π V = V) : V = policyValue M γ hM hγ0 hγ1 π
Uses 5 · Used by 1
Statement usesMarkov decision process · Stochastic Markov decision process · Bellman operator of a policy · Value of a policy
Proof usesQ-value of an action
Used byA greedy policy for the optimal value is optimal

TheoremValue iteration converges#✓fully proved

Let \(M\) be a Markov decision process with finitely many states \(S\), a nonempty finite set of actions, real rewards and stochastic transition probabilities (nonnegative, each row summing to \(1\)), and let \(0 \le \gamma < 1\) be a discount factor. Let \(T\) be the Bellman optimality operator of \(M\) with discount \(\gamma\). Then for every initial value function \(V : S \to \mathbb{R}\), the value iterates \(T^n V\) converge to the optimal value of \(M\) with discount \(\gamma\) as \(n \to \infty\).

theorem tendsto_valueIteration (V : S → ℝ) :
    Tendsto (fun n => valueIteration M γ n V) atTop (𝓝 (optimalValue M γ hM hγ0 hγ1))
Uses 6
Statement usesMarkov decision process · Stochastic Markov decision process · Optimal value of a discounted Markov decision process · Value iteration
Proof usesBellman optimality operator · Bellman's operator is a contraction

TheoremA priori error bound for value iteration#✓fully proved

Let \(M\) be a Markov decision process with finitely many states, a nonempty finite set of actions, real rewards and stochastic transition probabilities, let \(0 \le \gamma < 1\), and let \(T\) be the Bellman optimality operator and \(V^*\) the optimal value of \(M\) with discount \(\gamma\). For every real-valued function \(V\) on the states and every \(n \in \mathbb{N}\), the result \(T^n V\) of \(n\) steps of value iteration from \(V\) satisfies \(\|T^n V - V^*\|_\infty \le \|V - TV\|_\infty \, \gamma^n / (1 - \gamma)\), where \(\|\cdot\|_\infty\) is the sup norm.

theorem dist_valueIteration_le (V : S → ℝ) (n : ℕ) :
    dist (valueIteration M γ n V) (optimalValue M γ hM hγ0 hγ1) ≤
      dist V (bellman M γ V) * γ ^ n / (1 - γ)
Uses 6
Statement usesMarkov decision process · Stochastic Markov decision process · Bellman optimality operator · Optimal value of a discounted Markov decision process · Value iteration
Proof usesBellman's operator is a contraction

TheoremStopping test#✓fully proved

Let \(M\) be a Markov decision process with finitely many states, a nonempty finite set of actions, real rewards and stochastic transition probabilities, let \(0 \le \gamma < 1\), and let \(T\) be the Bellman optimality operator and \(V^*\) the optimal value of \(M\) with discount \(\gamma\). For every real-valued function \(V\) on the states, \(\|V - V^*\|_\infty \le \|V - TV\|_\infty / (1 - \gamma)\), where \(\|\cdot\|_\infty\) is the sup norm. So if one Bellman update moves \(V\) by at most \(\varepsilon\), then \(V\) is within \(\varepsilon / (1 - \gamma)\) of the optimal value.

theorem dist_optimalValue_le (V : S → ℝ) :
    dist V (optimalValue M γ hM hγ0 hγ1) ≤ dist V (bellman M γ V) / (1 - γ)
Uses 5
Statement usesMarkov decision process · Stochastic Markov decision process · Bellman optimality operator · Optimal value of a discounted Markov decision process
Proof usesBellman's operator is a contraction

TheoremNo policy beats the optimal value#✓fully proved

Let \(M\) be a Markov decision process with finitely many states, finitely many actions (at least one), real rewards \(r(s,a)\), and transition probabilities \(P(s,a,s')\) that are nonnegative and sum to \(1\) over \(s'\), and let \(0 \le \gamma < 1\). For every deterministic stationary policy \(\pi\), the value \(V^\pi\) of \(\pi\) is at most the optimal value \(V^*\) in every state: \(V^\pi(s) \le V^*(s)\) for all states \(s\).

theorem policyValue_le_optimalValue (π : S → A) :
    policyValue M γ hM hγ0 hγ1 π ≤ optimalValue M γ hM hγ0 hγ1
Uses 9 · Used by 2
Statement usesMarkov decision process · Stochastic Markov decision process · Optimal value of a discounted Markov decision process · Value of a policy
Proof usesBellman optimality operator · The optimal value solves the Bellman optimality equation · Bellman operator of a policy · A policy's Bellman update is at most the optimal one · Q-value of an action
Used byImprovement stalls exactly at optimal policies · Once optimal, policy iteration stays optimal

TheoremA greedy policy for the optimal value is optimal#✓fully proved

Let \(M\) be a Markov decision process with finitely many states, finitely many actions (at least one), real rewards \(r(s,a)\), and transition probabilities \(P(s,a,s')\) that are nonnegative and sum to \(1\) over \(s'\), let \(0 \le \gamma < 1\), and let \(V^*\) be the optimal value. Let \(\pi\) be the greedy policy for \(V^*\), which in each state \(s\) chooses an action \(a\) maximizing \(r(s,a) + \gamma \sum_{s'} P(s,a,s') \, V^*(s')\). Then the value of \(\pi\) equals \(V^*\).

theorem policyValue_greedy :
    policyValue M γ hM hγ0 hγ1 (greedy M γ (optimalValue M γ hM hγ0 hγ1)) =
      optimalValue M γ hM hγ0 hγ1
Uses 10
Statement usesMarkov decision process · Stochastic Markov decision process · Greedy policy · Optimal value of a discounted Markov decision process · Value of a policy
Proof usesBellman optimality operator · The optimal value solves the Bellman optimality equation · Uniqueness of the solution of a policy's Bellman equation · Bellman operator of a policy · The greedy action attains the Bellman maximum

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.