Dynamic Programming

Motivation

Single-leg capacity allocation under customer choice is the basic dynamic problem of revenue management: a firm holds a fixed stock of a perishable resource (seats on a flight leg, rooms on a night), and in every period of a finite selling horizon it decides which products (fare classes) to offer to the arriving customer. Talluri and van Ryzin (Management Science, 2004) showed that under a multinomial logit (MNL) choice model with known parameters, the optimal assortment in every period is revenue-ordered and shrinks as capacity becomes scarcer ("nesting by fare order"), which is what justifies the protection levels and bid prices used in practice.

The MNL parameters are estimated from data and are never known exactly. Rusmevichientong and Topaloglu (Operations Research, 2012) study the robust version, in which an adversary picks the parameters of each period from an uncertainty set after seeing the offered assortment, following the robust Markov decision process framework of Iyengar (Mathematics of Operations Research, 2005). Their Section 4 shows that the structure of the known-parameter problem survives: the value function is concave in capacity, the optimal assortment is a revenue threshold set, and it grows with remaining capacity and, when uncertainty does not shrink, over time. This mission formalizes those results.

Setting

There are $n$ products $\mathcal A = \{1,\dots,n\}$ with revenues $r_1,\dots,r_n$. An MNL parameter vector is $v = (v_0, v_1, \dots, v_n) \in \mathbb R^{n+1}_{++}$; offered the assortment $S \subseteq \mathcal A$, a customer buys product $i \in S$ with probability

$$\phi_i(S,v) = \frac{v_i}{v_0 + \sum_{\ell\in S} v_\ell},$$

and nothing with probability $1 - \sum_{i\in S}\phi_i(S,v)$. The expected revenue is $f(S,v) = \sum_{i\in S} r_i \phi_i(S,v)$.

Static problem (Section 3). For a compact nonempty uncertainty set $\mathcal V \subseteq \mathbb R^{n+1}_{++}$,

$$Z^*(\mathcal V) = \max_{S\subseteq\mathcal A}\ \min_{v\in\mathcal V} f(S,v),$$

and $S^*(\mathcal V)$ is an optimal assortment of smallest cardinality.

Dynamic problem (Section 4). Periods $t = 1,\dots,T$ each bring one customer, whose parameter vector lies in a compact nonempty $\mathcal V_t \subseteq \mathbb R^{n+1}_{++}$. A purchase consumes one unit of capacity. The value function $J_t(x)$, the maximum worst-case revenue from period $t$ on with $x$ units of capacity, satisfies

$$J_t(x) = \max_{S_t\subseteq\mathcal A}\ \min_{v_t\in\mathcal V_t}\Big\{\sum_{i\in S_t}\phi_i(S_t,v_t)\big(r_i + J_{t+1}(x-1)\big) + \Big(1-\sum_{i\in S_t}\phi_i(S_t,v_t)\Big)J_{t+1}(x)\Big\}$$

for $x \ge 1$, with $J_t(0) = 0$ and $J_{T+1} \equiv 0$. The marginal value of capacity is $\Delta J_t(x) = J_t(x) - J_t(x-1)$, and $S^*_t(x)$ is a maximizer of the right-hand side of smallest cardinality.

Formalization targets

Goal: Theorem 4.3 (p. 17)

For every $1 \le t \le T$ and $x \ge 1$, and, in the second part, every $1 \le t \le T-1$ with $\mathcal V_t \subseteq \mathcal V_{t+1}$:

$$S^*_t(x) \subseteq S^*_t(x+1), \qquad \mathcal V_t \subseteq \mathcal V_{t+1} \implies S^*_t(x) \subseteq S^*_{t+1}(x).$$

Milestones

1. (Dynamic Robust), second line (p. 16): $J_t(x) = \max_{S}\min_{v\in\mathcal V_t}\sum_{i\in S}\phi_i(S,v)\,(r_i - \Delta J_{t+1}(x)) + J_{t+1}(x)$.
2. Proof of Theorem 4.2 (pp. 16–17): $S^*_t(x)$ is the static $S^*(\mathcal V_t)$ for revenues $r_i - \Delta J_{t+1}(x)$, and $J_t(x) - J_{t+1}(x)$ is the corresponding $Z^*(\mathcal V_t)$.
3. Theorem 3.2 (p. 7): $S^*(\mathcal V) = \{i : r_i > Z^*(\mathcal V)\}$.
4. Theorem 3.7 (p. 10): for $\delta \ge 0$, $S^*(\mathcal V)$ is contained in the robust assortment for revenues $r + \delta$.
5. Corollary 3.5 (p. 9): $\mathcal V \subseteq \mathcal V' \implies Z^*(\mathcal V') \le Z^*(\mathcal V)$ and $S^*(\mathcal V) \subseteq S^*(\mathcal V')$.
6. Theorem 4.1, first inequality (p. 16): $\Delta J_t(x+1) \le \Delta J_t(x)$.
7. Theorem 4.1, second inequality (p. 16): $\Delta J_{t+1}(x) \le \Delta J_t(x)$.
8. Theorem 4.2 (p. 16): $S^*_t(x) = \{i : r_i > J_t(x) - J_{t+1}(x-1)\}$.

Significance

The result. Theorems 4.1–4.3 say that robustness costs nothing structurally: the robust policy is still a nested threshold policy, so it can be implemented with the protection levels or bid-price controls already in use, and it can be computed by examining at most $n$ revenue-ordered assortments per state instead of $2^n$. Theorem 4.3 gives the operational content: with less inventory, offer fewer, higher-revenue products; nearer the end of the season (when the uncertainty sets are nested), offer more.

Formalizing it. The results are proved in the paper; none of them has a machine-checked proof. A formalization produces a checked robust finite-horizon dynamic program over finite action sets with compact adversary sets, the reduction of each Bellman step to a static max–min problem with shifted revenues, and checked concavity and time-monotonicity arguments that are reusable for other single-resource problems. The known-parameter analogues for general regular choice models and for the Markov chain choice model are separate drafts on the platform (RevenueOrdered.Nesting.*, MarkovChainChoice.SingleResource.*); they have no uncertainty set and are not used here.

Difficulty

The obvious route to concavity, an induction on $t$ in which $J_t$ is a maximum of concave functions, fails: a maximum of concave functions is not concave, and here each candidate assortment is evaluated by a minimum over $\mathcal V_t$, and the worst-case parameter vector changes with the capacity level, so the known-parameter argument cannot be reused term by term. Any induction on $t$ also has to handle the boundary $x = 0$, where the Bellman equation does not apply and only $J_t(0) = 0$ is given. Every step involving a minimum must use that the minimum over a compact set is attained, and translating a minimum by a constant must be justified rather than assumed.

Formalization scope

• Representation. Products are Fin n (Lean index $i$ is product $i+1$). A parameter vector is p : ℝ × (Fin n → ℝ) with p.1 $= v_0$. $f(S,v)$ is the published ChoiceCDLP.MNL.mnlObjective. Minima over uncertainty sets are real infima (sInf), equal to the attained minima under the standing hypotheses; maxima are Finset.sup' over all $2^n$ assortments.
• Standing assumptions. Every V t, $1 \le t \le T$, is compact, nonempty and contained in $\mathbb R^{n+1}_{++}$ (IsUncertaintySeq); the static results assume the same of V. The paper writes "$\mathcal V \subset \mathbb R^n_{++}$" in Theorem 3.2 and Corollary 3.5; this is read as $\mathbb R^{n+1}_{++}$, compact.
• Revenues are arbitrary reals. The paper orders $r_1 \ge \dots \ge r_n > 0$ "without loss of generality"; no proof uses it, and the dynamic reduction applies Theorem 3.2 to $r_i - \Delta J_{t+1}(x)$, which may be negative. Dropping it strengthens every statement.
• The value function is defined by the recursion. The max–min policy formulation (p. 15) and Iyengar's theorem that it satisfies the Bellman equation are not formalized. $J_t(x)$ is defined for every $x \in \mathbb N$; the initial capacity $C$ never enters the recursion, so the paper's $J_t$ on $\{0,\dots,C\}$ is the restriction.
• Capacity $x \ge 1$. Theorem 4.1 is printed "for any $x \in \{0,1,\dots,C\}$", which includes the undefined $\Delta J_t(0)$; Theorems 4.2 and 4.3 say "for any $x$", but $S^*_t(0)$ is not defined by the Bellman equation. All statements assume $x \ge 1$.
• Tie-break. $S^*(\mathcal V)$ and $S^*_t(x)$ are predicates ("$S$ is an optimal assortment of smallest cardinality"), not choice functions; Theorems 3.2 and 4.2 are stated as "↔ $S$ is the threshold set", which also asserts the threshold set is optimal. Without the tie-break Theorems 4.2 and 4.3 are false, since a product with revenue exactly at the threshold can be added.
• Ruled out. Defining $J$ as a maximum over revenue-ordered assortments, or through the threshold formula, would make Theorem 4.2 definitional; $J$ is defined with the minimum inside a maximum over all subsets.
• Restatements. Theorems 3.2, 3.7 and Corollary 3.5 restate, in RobustMNL.Dynamic, the companion mission on Section 3 of the same paper, identically up to namespace.
• Source. The source is the authors' manuscript of 20 September 2011 of the Operations Research 2012 article; its printed page numbers equal the PDF's.
• Welcome contributions. Lemmas on attained minima of continuous functions on compact sets of positive parameter vectors, the translation of a max–min by a constant, and the bound $\sum_{i\in S}\phi_i(S,v) \le 1$ are reusable across all three missions of this paper.

Selected references

• P. Rusmevichientong, H. Topaloglu, Robust Assortment Optimization in Revenue Management Under the Multinomial Logit Choice Model, Operations Research 60(4), 2012. https://doi.org/10.1287/opre.1120.1063
• K. Talluri, G. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 2004. https://doi.org/10.1287/mnsc.1030.0147
• G. N. Iyengar, Robust Dynamic Programming, Mathematics of Operations Research 30(2), 2005. https://doi.org/10.1287/moor.1040.0129

Motivation

Markov decision processes model sequential decisions under uncertainty, and their optimal policies are computed from transition probabilities that in practice are estimated from data. Optimal policies can be sensitive to estimation error in those probabilities. Robust dynamic programming replaces each transition law by a set of plausible laws and evaluates a policy by its worst-case expected reward over that set. Garud Iyengar's Robust dynamic programming (CORC Tech Report TR-2002-07, 2002, rev. 2004; Mathematics of Operations Research 30(2), 2005) set up this theory for countable state spaces and history-dependent policies. It isolated the Rectangularity assumption under which the robust problem keeps a Bellman equation. In the same period, Nilim and El Ghaoui studied robust control of Markov decision processes with finite state spaces.

Timeline:

• 1968, 1973. Satia (PhD thesis) and Satia and Lave (Operations Research 21) treat finite-state, finite-action Markov decision processes with uncertain transition probabilities. They state the max–min optimality equation and the optimality of stationary policies, assuming convex uncertainty sets, and do not prove that the solution of the equation is the robust value function.
• 2001. Bagnell, Ng and Schneider analyse robust policies when the decision maker is restricted to stationary policies.
• 2002–2005. Iyengar (this paper) and Nilim and El Ghaoui (Operations Research 53, 2005) give the rectangular theory. Iyengar proves the discounted robust Bellman equation for countable state spaces, against history-dependent randomized policies and an adversary that may change the law at every visit.

Setting

A discounted ambiguous Markov decision process has a countable state set $\mathcal S$, for each state $s$ a nonempty set $\mathcal A(s)$ of admissible actions, for each admissible pair $(s,a)$ a nonempty set $\mathcal P(s,a)$ of probability measures on $\mathcal S$ (the ambiguity set), a bounded reward $r(s,a,s')$ and a discount factor $\lambda\in(0,1)$. Decisions are made at epochs $t=0,1,2,\dots$.

A policy $\pi=(d_0,d_1,\dots)$ maps each history $h_t=(s_0,a_0,\dots,s_t)$ to a probability measure on $\mathcal A(s_t)$. $\Pi$ is the set of all such policies. A deterministic Markov policy plays $d_t(s_t)$ for maps $d_t:\mathcal S\to\mathcal A$ with $d_t(s)\in\mathcal A(s)$. A stationary policy uses one such rule $d$ at every epoch.

Under Rectangularity, the adversary picks a law $p\in\mathcal P(s_t,a_t)$ separately at every epoch and history, and may pick a different law each time a state–action pair recurs. This is the dynamic model, and the set of path measures it generates is $\mathcal T^\pi$. In the static model the adversary fixes one $\bar p_{sa}\in\mathcal P(s,a)$ per pair. The robust value of a policy and the robust value function are

$$V^\pi_\lambda(s)=\inf_{\mathbf P\in\mathcal T^\pi}\mathbf E^{\mathbf P}\Big[\sum_{t=0}^\infty\lambda^t r(s_t,d_t(h_t),s_{t+1})\Big],\qquad V^*_\lambda(s)=\sup_{\pi\in\Pi}V^\pi_\lambda(s).$$

Let $\mathbf V$ be the bounded functions on $\mathcal S$ with $\|V\|=\sup_s|V(s)|$. For a set $\mathcal D$ of deterministic Markov rules, the robust Bellman operator is

$$\mathcal L_{\mathcal D}V(s)=\sup_{d\in\mathcal D}\ \inf_{p\in\mathcal P(s,d(s))}\mathbf E^p\big[r(s,d(s),s')+\lambda V(s')\big].$$

Formalization targets

Goal: Corollary 2(b)

$$V^*_\lambda(s)=\sup_{a\in\mathcal A(s)}\ \inf_{p\in\mathcal P(s,a)}\mathbf E^p\big[r(s,a,s')+\lambda V^*_\lambda(s')\big],\qquad s\in\mathcal S,$$

$V^*_\lambda$ is the only bounded solution of this equation, and for every $\epsilon>0$ some stationary deterministic policy $\pi^\epsilon$ has $V^{\pi^\epsilon}_\lambda\ge V^*_\lambda-\epsilon$.

Milestones

1. Theorem 5(a). $\mathcal L_{\mathcal D}$ maps $\mathbf V$ to $\mathbf V$ and $\|\mathcal L_{\mathcal D}U-\mathcal L_{\mathcal D}V\|\le\lambda\|U-V\|$.
2. Theorem 5(b). For $\mathcal D=\prod_s\mathcal D(s)$, the equation $\mathcal L_{\mathcal D}V=V$ has a unique bounded solution, equal to the robust value over deterministic Markov policies with rules in $\mathcal D$.
3. Corollary 2(a). The robust value of a stationary policy $(d,d,\dots)$ is the unique bounded solution of $V(s)=\inf_{p\in\mathcal P(s,d(s))}\mathbf E^p[r(s,d(s),s')+\lambda V(s')]$.
4. Theorem 4. $V^*_\lambda(s)=\sup_{\pi\in\Pi_{MD}}V^\pi_\lambda(s)$.
5. Lemma 3. For a stationary policy, the dynamic and static models give the same value.
6. Lemma 2. The value of a stationary policy is the optimal solution of the robust program (31).
7. Lemma 1, first claim. The output of robust value iteration is within $\epsilon/4$ of $V^*_\lambda$.

Significance

Corollary 2(b) justifies computing the robust value function by solving a state-wise max–min equation. Value iteration, policy iteration and their approximations all rely on that equation. It also shows that a decision maker facing a history-dependent adversary loses at most $\epsilon$ by committing to a stationary deterministic rule. Corollary 2(a) and Lemma 2 make robust policy evaluation a fixed point problem and a robust optimization problem. Lemma 3 shows that, for stationary policies, the dynamic model costs nothing relative to the static model, in which the true transition law is fixed but unknown.

The results are proved on paper. The page proves Theorem 4 only by citation to Puterman's non-robust arguments. No machine-checked proof of any of them is known. The platform has finite-state analogues posed by the Nilim–El Ghaoui and Satia–Lave missions, which compare only stationary or Markov controllers. This mission poses the countable, history-dependent version, and proving it would establish them in this generality.

Difficulty

The contraction property is a state-by-state $\epsilon$-argument. The hard step is to identify the fixed point with the value of the game against all history-dependent randomized policies. The adversary's choices at different epochs interact only through Rectangularity, so splitting the infimum over path measures into a first-step infimum and a continuation infimum must be justified for an infinite horizon, uncountably many adversary strategies and no attainment of the infima. The ambiguity sets need not be convex or closed. The naive route, "take the minimizing law at each state", is unavailable, and every bound must be carried with an $\epsilon$ slack. Truncating the infinite sum needs the uniform reward bound. Theorem 4 needs a separate argument that randomization and history dependence do not help the decision maker against the dynamic adversary.

Formalization scope

States and actions are countable Lean types; $\mathcal A(s)$ and $\mathcal P(s,a)$ are sets, assumed nonempty, with no convexity or closedness. Laws are PMFs and $\mathbf E^p[f]=\sum_x p(x)f(x)$ as a tsum. The rewards satisfy $|r(s,a,s')|\le R$ on admissible actions. This is the reading of the page's "$\sup r=R<\infty$", which its bounds $\pm R/(1-\lambda)$ require. The discount factor satisfies $0<\lambda<1$. Epochs start at $0$, so the first reward is undiscounted.

A policy maps $(n, h_n)$ to a PMF supported on $\mathcal A(s_n)$. The dynamic adversary maps $(n,h_n,a)$ to a law in $\mathcal P(s_n,a)$. The path law is built by PMF.bind, and the discounted reward is $\sum_t\lambda^t\mathbf E[r(s_t,a_t,s_{t+1})]$, which converges absolutely. Values are real infima and suprema over nonempty families bounded by $R/(1-\lambda)$, so no junk value arises. $\mathbf V$ is the predicate "bounded", and $\|\cdot\|$ is a supremum (the page writes max). All uniqueness claims are uniqueness among bounded functions.

$V^*_\lambda$ is a supremum over all history-dependent randomized policies. Defining it over deterministic Markov or stationary policies would make Theorem 4 trivial and weaken the goal, so it is ruled out. The adversary in $V^\pi_\lambda$ is the dynamic one; the static adversary appears only in Lemma 3.

The mission deviates from the page in three places:

• Theorem 5(b) is stated for product sets $\mathcal D=\prod_s\mathcal D(s)$. For an arbitrary $\mathcal D$ the printed statement fails, because its proof pastes $\epsilon$-greedy actions state by state. Both uses in Corollary 2 are products.
• Lemma 3 is stated for randomized Markov rules, which is the page's "any decision rule". The page proves it for deterministic rules.
• Lemma 2 adds $\sum_s\alpha(s)<\infty$ and restricts the program to bounded $V$.

Only the first claim of Lemma 1 is posed. Its second claim, that an $\epsilon/2$-greedy rule is $\epsilon$-optimal, is false as printed.

A complete development needs a general toolkit that is reusable beyond this mission: path laws of countable controlled processes with history-dependent policies, a uniform $\epsilon$-optimal selection argument for real infima over arbitrary sets, and the Banach fixed point theorem on bounded functions (Mathlib's ContractingWith). Proofs of individual milestones are welcome in any order. Theorem 5(a) is the natural entry point.

Selected references

• G. Iyengar, Robust dynamic programming, CORC Tech Report TR-2002-07, Columbia University, 2002 (rev. May 4, 2004); published in Mathematics of Operations Research 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
• A. Nilim and L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Operations Research 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
• J. K. Satia and R. E. Lave, Markovian decision processes with uncertain transition probabilities, Operations Research 21(3):728–740, 1973. https://doi.org/10.1287/opre.21.3.728
• J. A. Bagnell, A. Y. Ng and J. Schneider, Solving uncertain Markov decision problems, Tech. Report CMU-RI-TR-01-25, Carnegie Mellon University, 2001. https://www.ri.cmu.edu/publications/solving-uncertain-markov-decision-problems/
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

Markov decision processes assume that the transition law is known exactly. In practice it is estimated from data, and the optimal policy computed for the point estimate can perform badly when the true law differs. Robust dynamic programming replaces each transition law by a set of plausible laws and evaluates a policy by its worst-case expected reward over that set. The worst case is taken against an adversary (nature) who may choose a law from the set at every step.

For this worst case to be computable by backward induction, the set of path measures of a policy has to decompose epoch by epoch. Garud Iyengar named this property Rectangularity and proved that under it the classical finite horizon theory carries over: a robust Bellman equation holds, and deterministic Markov policies are optimal among all history dependent randomized policies, with state and action sets that may be countably infinite and ambiguity sets that need not be convex (Iyengar, CORC Tech Report TR-2002-07, rev. 2004; published in Math. Oper. Res. 30(2), 2005).

Timeline:

• 1973: Satia and Lave study Markov decision processes with uncertain transition probabilities, finite states and actions (Oper. Res. 21(3)).
• 2001: Epstein and Schneider axiomatize recursive multiple priors, the decision-theoretic origin of rectangular ambiguity (J. Econ. Theory 113, working paper 2001).
• 2002–2005: Nilim and El Ghaoui give a robust counterpart of the Bellman recursion for finite state and action spaces and convex ambiguity sets, against Markov controllers (Oper. Res. 53(5)).
• 2002–2005: Iyengar proves the robust Bellman equation and Markov optimality for countable spaces, arbitrary ambiguity sets and all history dependent randomized policies, under Rectangularity.

Setting

A finite horizon ambiguous Markov decision process (AMDP) has decision epochs $t \in T = \{0,\dots,N-1\}$, $N\ge 1$, and a terminal epoch $N$. States lie in a countable set $\mathcal S$ and actions in a countable set $\mathcal A$. In state $s$ at epoch $t$ the admissible actions form a nonempty set $\mathcal A_t(s)$. For each admissible action $a$, the next state is drawn from some probability measure $p \in \mathcal P_t(s,a)$, where $\mathcal P_t(s,a)$ is a nonempty set of probability measures on $\mathcal S$, the ambiguity set. The decision maker receives $r_t(s,a,s')$ when $a$ is taken in $s$ and the next state is $s'$, and $r_N(s)$ at the terminal epoch.

A history at epoch $n$ is $h_n=(s_0,a_0,\dots,s_{n-1},a_{n-1},s_n)$. A policy $\pi=(d_t)$ assigns to each history $h_t$ a probability measure $d_t(h_t)$ on $\mathcal A_t(s_t)$. It is deterministic ($\Pi_D$) if every $d_t(h_t)$ is a point mass, and deterministic Markov ($\Pi_{MD}$) if moreover the chosen action depends on the current state $s_t$ alone. $\Pi$ denotes all history dependent randomized policies.

Under Rectangularity (Assumption 1), the set $\mathcal T^\pi$ of path measures consistent with $\pi$ is a product of one-epoch sets: nature chooses, for every epoch $t$, every history $h_t$ and every admissible action $a$, a measure $p_{h_t,a}\in\mathcal P_t(s_t,a)$, and the path measure is $\mathbf P(h_N)=\prod_t d_t(h_t)(a_t)\,p_{h_t,a_t}(s_{t+1})$. The robust value of $\pi$ from $h_n$ and the robust value function are

$$V^\pi_n(h_n)=\inf_{\mathbf P\in\mathcal T^\pi_n}E^{\mathbf P}\Big[\sum_{t=n}^{N-1}r_t(s_t,a_t,s_{t+1})+r_N(s_N)\Big],\qquad V^*_n(h_n)=\sup_{\pi\in\Pi}V^\pi_n(h_n).$$

The optimistic values $\bar V^\pi_n$, $\bar V^*_n$ replace the infimum over $\mathcal T^\pi_n$ by a supremum.

Formalization targets

Goal: Theorem 2 (Markov optimality)

For $n=0,\dots,N$, $V^*_n(h_n)$ depends on $h_n$ only through $s_n$; for $n\in T$, $V^*_n(s_n)=\sup_{\pi\in\Pi_{MD}}V^\pi_n(s_n)$; and

$$V^*_n(s)=\sup_{a\in\mathcal A_n(s)}\ \inf_{p\in\mathcal P_n(s,a)}E^p\big[r_n(s,a,s')+V^*_{n+1}(s')\big],\qquad n\in T. \tag{16}$$

Milestones

1. Proof of Theorem 1, eq. (15): at one epoch, randomizing over actions does not raise the worst-case value, and the adversary may choose its measure separately per action.
2. Theorem 1 (Bellman equation): $V^*_N(h_N)=r_N(s_N)$ and $V^*_n(h_n)=\sup_{a}\inf_{p\in\mathcal P_n(s_n,a)}E^p[r_n(s_n,a,s)+V^*_{n+1}(h_n,a,s)]$ (11).
3. Corollary 1: $V^*_n(h_n)=\sup_{\pi\in\Pi_D}V^\pi_n(h_n)$ for $n\in T$.
4. Theorem 3: the optimistic analogue of Theorem 2, with recursion (18) in which both the outer and the inner optimizations are suprema.

The mission also contains, as a draft theorem that is not a milestone, the per-policy identity of the proof of Theorem 1, eq. (12): for each policy, $V^\pi_n(h_n)=\inf_{p\in\mathcal T^{d_n}}E^p[r_n+V^\pi_{n+1}(h_n,a_n,s_{n+1})]$.

Significance

Theorem 2 is the basis of robust dynamic programming in finite horizon: computing an optimal robust policy reduces to $N$ backward passes, each a family of one-stage problems $\inf_{p\in\mathcal P_n(s,a)}E^p[v]$. It also justifies restricting attention to deterministic Markov policies, which is what every algorithm in the robust MDP literature computes. Theorem 1 isolates the role of Rectangularity: without it the worst case over path measures does not decompose and the recursion characterizes nothing.

The results are proved on paper; no machine-checked proof is known. The platform holds the finite-state, Markov-controller special case (the Nilim–El Ghaoui RobustMDP series, posed, not proved), whose comparison class is too small to express the claim $\Pi_{MD}$ suffices against $\Pi$. A formal proof here supplies the history dependent policy and adversary machinery on countable spaces that the discounted robust theory and the robust MDP literature reuse.

Difficulty

The obvious argument writes the robust value as an inf–sup over path measures and pushes the infimum inside the expectation epoch by epoch. That step is the content of (12): the infimum of an expectation equals the expectation of an infimum only because nature's continuation choice may depend on the realized action and next state, so near-worst continuations for different branches can be glued into one admissible adversary. Infima need not be attained (the ambiguity sets are arbitrary, the state set countable), so the gluing is an $\epsilon$-argument over countably many branches. The supremum over policies needs a matching splicing of $\epsilon$-optimal continuation policies (13)–(14). Finally, randomized decision rules must be eliminated (15), which uses Rectangularity again, now per action. Restricting either the policies or the adversary to Markov ones from the start is not allowed: it changes the comparison class and makes the goal circular.

Formalization scope

• One countable state type S and one countable action type A serve all epochs; the page's epoch-dependent sets $\mathcal S_t$ embed into their disjoint union. Epochs are 0-based natural numbers, with terminal epoch M.N and 1 ≤ N.
• A history at epoch $n$ is (Fin n → S × A) × S. Probability measures are PMF; $E^p[f]=\sum_s p(s)f(s)$ as a tsum. The expected reward under a policy and an adversary is computed by backward iterated sums, which is the expectation under the product path measure (3).
• A policy is a decision rule for every epoch, admissible for t < N; the supremum over $\Pi$ equals that over the page's $\Pi_n$ because $V^\pi_n$ uses only $d_n,\dots,d_{N-1}$. An adversary chooses $p_{h_t,a}\in\mathcal P_t(s_t,a)$ for every epoch, history and admissible action.
• Added and implicit hypotheses: $\mathcal A_t(s)\neq\emptyset$ and $\mathcal P_t(s,a)\neq\emptyset$ (implicit on the page), and a uniform bound $|r_t|\le R$, $|r_N|\le R$ (added: Section 2 states none, but with countable states the expectations and the real suprema and infima need it). All values then lie in a bounded interval, so no supremum or infimum is a junk value.
• Ambiguity sets are arbitrary nonempty sets of measures: no convexity, closedness or attainment is assumed anywhere.
• "$V^*_n$ is a function of the current state alone" is stated as the existence of $W(n,s)$ with $V^*_n(h_n)=W(n,s_n)$; the value is not defined on states, which would hide the claim. The notation $V^\pi_n(s_n)$ for Markov policies is made explicit as a clause.
• Ruled out: restricting $\Pi$ or the adversary to Markov or stationary objects, a static adversary that fixes one $p$ per $(s,a)$ for the whole horizon, and suprema over unbounded or empty families; each makes some target false or trivial.

Definitions: AMDP, History, History.extend, IsPolicy, Policy, IsDeterministic, IsDetMarkov, Adversary, Selection, expect, expTail, expectedReward, V, Vstar, Vbar, VbarStar, all in RobustDP.FiniteHorizon. Lemmas about gluing adversaries along history prefixes and about suprema of bounded families indexed by subtypes are reusable. Contributions to any milestone are welcome, in any order; (15) is a one-epoch statement independent of the rest.

Selected references

• G. Iyengar, Robust dynamic programming, CORC Tech Report TR-2002-07, Columbia University, revised May 4, 2004; Math. Oper. Res. 30(2):257–280, 2005. https://doi.org/10.1287/moor.1040.0129
• A. Nilim and L. El Ghaoui, Robust control of Markov decision processes with uncertain transition matrices, Oper. Res. 53(5):780–798, 2005. https://doi.org/10.1287/opre.1050.0216
• J. K. Satia and R. E. Lave, Markovian decision processes with uncertain transition probabilities, Oper. Res. 21(3):728–740, 1973. https://doi.org/10.1287/opre.21.3.728
• L. G. Epstein and M. Schneider, Recursive multiple-priors, J. Econ. Theory 113(1):1–31, 2003. https://doi.org/10.1016/S0022-0531(03)00097-8
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994. https://doi.org/10.1002/9780470316887

Motivation

A reinforcement-learning agent that does not know its environment has to act and learn at once. Each step spent gathering information about unfamiliar states is a step not spent collecting reward, and an agent that only exploits what it already knows may never find better behaviour. Chapter 8 of Kakade's thesis (Kakade 2003) turns this trade-off into a counting question. Run an algorithm for an arbitrarily long time on one unbroken path of experience, with no resets. At how many timesteps does it fail to act optimally with respect to a fixed planning horizon $T$? Kakade calls this number the sample complexity of exploration.

The question builds on two algorithms. $E^3$ (Kearns and Singh 2002) gave the first polynomial-time guarantee for near-optimal behaviour in an unknown MDP. $R_{max}$ (Brafman and Tennenholtz 2002) replaced $E^3$'s explicit explore-or-exploit switch by optimism: unknown states are treated as maximally rewarding. Kakade's chapter sharpens the analysis of $R_{max}$. For deterministic MDPs it shows that the number of non-optimal steps is at most $NAT$, which matches its own lower bound. The thesis notes that its deterministic results are similar to those of Koenig and Simmons (1993), with the dependence on $N$, $A$ and $T$ made explicit (pp. 99, 104). The later PAC-MDP literature (for example Strehl, Li and Littman 2009) took this counting notion as its standard measure of exploration efficiency.

Setting

An MDP $M$ has a finite set $S$ of $N$ states, a finite nonempty set of $A$ actions, a transition model $P(s'\mid s,a)$ and a deterministic reward $r(s,a)\in[0,1]$. A deterministic MDP has a next-state map $f$, with $P(s'\mid s,a)=1$ exactly when $s'=f(s,a)$.

Online model. An algorithm $\mathcal A$ is a deterministic function that maps the path observed so far, $(s_0,a_0,r_0,\dots,s_t)$, to the next action $a_t$. Started at $s_0$, it produces one path $c=(s_0,a_0,s_1,a_1,\dots)$; $c_t$ is the subpath up to $s_t$. The $T$-step end time $t'$ of $t$ is the smallest multiple of $T$ larger than $t$. The $T$-step value of the algorithm on $c_t$ is the normalized reward it collects until $t'$,

$$U_{\mathcal A}(c_t)=\frac1T\,\mathbb E\Big[\sum_{\tau=t}^{t'-1}r(s_\tau,a_\tau)\Big],$$

and $U^*(c_t)$ is the supremum of this quantity over all algorithms continuing from $c_t$.

$T$-step policies. A $T$-step policy $\pi$ is a sequence of deterministic decision rules $\pi(\cdot,0),\dots,\pi(\cdot,T-1)$. Its $t$-value is $U_{\pi,t,M}(s)=\frac1T\mathbb E[\sum_{\tau=t}^{T-1}r(s_\tau,a_\tau)\mid s_t=s]$, and $U^*_{t,M}(s)$ is the supremum over $T$-step policies. For a set of states $K$, the induced MDP $M_K$ agrees with $M$ on $K$ and makes every state outside $K$ absorbing with reward $1$. The escape probability $\Pr(\text{escape from }K\mid\pi,M,s_t=s)$ is the probability that the path $(s_t,\dots,s_{T-1})$ of $\pi$ in $M$ leaves $K$. A transition model $\hat P$ is an $\varepsilon$-approximation to $P$ if $\sum_{s'}|\hat P(s'\mid s,a)-P(s'\mid s,a)|<\varepsilon$ for every $(s,a)$.

Formalization targets

Goal: Theorem 8.3.5 (deterministic sample complexity)

For every $N$, $A$ and $T\ge1$ there is one algorithm $\mathcal A$ such that, for every deterministic MDP with rewards in $[0,1]$, every start state and every $L$,

$$\#\{\,t<L:\ U_{\mathcal A}(c_t)\neq U^*(c_t)\,\}\ \le\ NAT .$$

Milestones

• Lemma 8.4.4 (induced inequalities). For every $T$-step policy, every $t<T$ and every state $s$,

$$U_{\pi,t,M_K}(s)\ge U_{\pi,t,M}(s)\ge U_{\pi,t,M_K}(s)-\Pr(\text{escape from }K\mid\pi,M,s_t=s).$$

• Corollary 8.4.5 (implicit explore or exploit). If $\pi$ is $T$-step optimal in $M_K$, then for every $t<T$ and every state $s$,

$$U_{\pi,t,M}(s)\ge U^*_{t,M}(s)-\Pr(\text{escape from }K\mid\pi,M,s_t=s).$$

• Deterministic escapes (p. 114). In a deterministic MDP every escape probability is $0$ or $1$.
• Non-escaping steps are optimal (p. 114). In a deterministic MDP, an optimal policy of $M_K$ that does not escape from $(s,t)$ satisfies $U_{\pi,t,M}(s)=U^*_{t,M}(s)$.
• Lemma 8.5.4 ($\varepsilon$-approximation condition). If $\hat P$ is an $\varepsilon$-approximation to $P$ and the rewards agree, then $|U_{\pi,t,\hat M}(s)-U_{\pi,t,M}(s)|<\varepsilon T$ for all $\pi$, $s$ and $t<T$.
• Lemma 8.5.5, pinned. If $m\ge\frac{8N}{\varepsilon^2}\log\frac{2N}\delta$ with $\varepsilon>0$, $0<\delta<1$, then the empirical distribution of $m$ independent samples from a distribution $p$ on $N$ points satisfies $\sum_i|\hat p(i)-p(i)|\le\varepsilon$ with probability greater than $1-\delta$.

Significance

The result. The bound $NAT$ does not depend on $L$. However long the agent runs, only a fixed number of its steps fail to be $T$-step optimal. The thesis's Theorem 8.3.6 shows that every algorithm has $\Omega(NAT)$ such steps on some deterministic MDP, so for deterministic MDPs the upper and lower bounds coincide. The induced-MDP lemmas carry over unchanged to stochastic MDPs. Together with Lemmas 8.5.4 and 8.5.5, they give the chapter's general bound (Theorem 8.3.1). They are the template for later optimism-based analyses, which compare an optimistic model with the true one and charge the difference to the probability of leaving the known region.

Formalizing it. The results are proved in the thesis; neither Mathlib nor the Prove2Me catalog contains a machine-checked version of any of them. A complete development would contain:

• a verified finite-horizon dynamic-programming layer (backward recursions, optimal $T$-step values as suprema);
• a simulation lemma in $\ell_1$;
• a concentration bound for empirical distributions whose sample size is linear in $N$;
• an explicit construction of an online exploration algorithm, with a counting argument about its run.

The proof of Lemma 8.5.5 in the thesis uses a Chernoff bound of the form $P(|\hat p_i-p_i|>\alpha p_i)\le2e^{-\alpha^2p_im/2}$. This form fails for the upper tail when $\alpha>1$, so the pinned statement needs a different argument.

Difficulty

The algorithm must be fixed before the MDP. It knows nothing about $f$ or $r$ beyond what its own path reveals, yet the count has to hold for every MDP, every start state and every run length at once. A direct approach could explore each state-action pair once and then plan. That does not bound the count. Exploration is interleaved with exploitation, the agent can only reach unknown pairs through known states, and every step on the way is judged against the full $T$-step optimum of the current cycle. The work lies in charging each non-optimal step to a distinct newly tried state-action pair, with at most $T$ steps charged per pair, while the planning policy is recomputed every time the set of known states grows. In the stochastic lemmas, the main issue is that $U^*_{t,M}$ is a supremum over all $T$-step policies, so the comparison has to go through $M_K$ for every competing policy, not only the planner's.

Formalization scope

• Model. $S$ and $A$ are finite types, $A$ nonempty; $N=|S|$ and $A=|A|$. Rewards are deterministic, with $0\le r\le1$ a hypothesis of every statement. Transition models are IsTransitionKernel functions $P(s'\mid s,a)$.
• Normalization and time. Values carry the factor $1/T$, so they lie in $[0,1]$; epochs are 0-based. $T$-step policies are functions $\mathbb N\to S\to A$, entered into the canonical stochastic $T$-epoch layer as indicator policies. $U^*_{t,M}$ is the supremum over these policies, which is bounded under the hypotheses.
• Online model. In the online model the algorithm has type List (S × A × ℝ) → S → A. The run is defined by recursion and is infinite. $U_{\mathcal A}(c_t)$ is the realised normalized sum up to the end time, and $U^*(c_t)$ is the backward recursion $W_{t'-t}(s_t)$, which is the supremum over algorithms by the Markov property. The count runs over $t<L$ for every $L$.
• Corrections to the printed text. Corollary 8.4.5 is stated for $t<T$, where its quantities are defined; the printed range is $t\le T$. Lemma 8.5.5 carries an explicit sample size in place of $O(\cdot)$.

Four formalizations would make the goal trivial or false, and each is excluded:

• quantifying the algorithm after the MDP, which lets it read $f$ and $r$;
• giving the algorithm a type that takes $f$ or $r$ as an argument;
• defining $U^*$ as a junk real supremum;
• hiding rewards from the observed path, which makes the statement false.

Reusable beyond this mission are the finite-horizon value layer, the induced-MDP and escape-probability lemmas, and the $\ell_1$ concentration bound. Contributions to any of these are useful independently of the goal.

Selected references

• S. M. Kakade, On the Sample Complexity of Reinforcement Learning, PhD thesis, Gatsby Computational Neuroscience Unit, University College London, 2003. https://discovery.ucl.ac.uk/id/eprint/10100726/
• R. I. Brafman and M. Tennenholtz, R-max — a general polynomial time algorithm for near-optimal reinforcement learning, Journal of Machine Learning Research 3, 2002. https://www.jmlr.org/papers/v3/brafman02a.html
• M. Kearns and S. Singh, Near-optimal reinforcement learning in polynomial time, Machine Learning 49, 2002. https://doi.org/10.1023/A:1017984413808
• A. L. Strehl, L. Li and M. L. Littman, Reinforcement learning in finite MDPs: PAC analysis, Journal of Machine Learning Research 10, 2009. https://jmlr.org/papers/v10/strehl09a.html

Why the gradient of the value matters

Policy gradient methods search a parameterized family of stochastic policies $\pi(a\mid s,\theta)$, $\theta\in\mathbb R^k$, by following the gradient of the policy's performance. They are the standard tool when the state space is too large for tabular dynamic programming and when a compact policy class (a neural network, a linear softmax) is easier to represent than a value function. Every such method rests on one identity: a formula for the gradient of the value with respect to $\theta$ that involves only quantities of the current policy, so that it can be estimated from the policy's own trajectories.

Chapter 4 of S. M. Kakade's PhD thesis, On the Sample Complexity of Reinforcement Learning (University College London, 2003), states this identity in two settings, the $T$-epoch undiscounted setting and the $\gamma$-discounted setting, both in the thesis's normalized convention, in which values lie in $[0,1]$. The thesis then uses the formula to analyse how many samples a gradient estimate needs (§4.2.3), and in §5.4.2 rewrites it in terms of advantages to explain why gradient methods can stall far from optimal: the gradient weights advantages by the current policy's state distribution, not by the distribution of an optimal policy.

Timeline:

• 1992: R. J. Williams introduces the likelihood-ratio (REINFORCE) estimator for episodic tasks.
• 2000: Sutton, McAllester, Singh and Mansour state the policy gradient theorem with function approximation, for discounted and average-reward criteria (NeurIPS 1999 proceedings, 2000); Konda and Tsitsiklis give actor-critic counterparts.
• 2001: Baxter and Bartlett analyse biased gradient estimation in the infinite-horizon setting.
• 2003: Kakade's thesis restates both theorems for normalized values, introduces the future state-time distribution $d_{\pi,s_0}$ for non-stationary $T$-epoch policies, and draws the "mismeasure" consequence.

Setting

A finite MDP has a finite state set $S$, a finite nonempty action set $A$, a transition kernel $P(s'\mid s,a)$ and a deterministic reward $r(s,a)\in[0,1]$.

$T$-epoch case. Epochs are $t\in\{0,\dots,T-1\}$, $T\ge1$. A non-stationary policy chooses $a$ at epoch $t$ in state $s$ with probability $\pi(a\mid s,t)$. Starting from $s_0$, $\Pr(s_t=s\mid\pi,s_0)$ is the probability of being in $s$ at epoch $t$. The normalized $t$-value is

$$V_{\pi,t}(s)=\frac1T\,\mathbb E\Big[\sum_{\tau=t}^{T-1}r(s_\tau,a_\tau)\,\Big|\,\pi,s_t=s\Big],\qquad V_\pi=V_{\pi,0},$$

the $t$ state-action value is $Q_{\pi,t}(s,a)=\frac1T r(s,a)+\mathbb E_{s'\sim P(\cdot\mid s,a)}[V_{\pi,t+1}(s')]$ with $V_{\pi,T}=0$, and the future state-time distribution on $S\times\{0,\dots,T-1\}$ is $d_{\pi,s_0}(s,t)=\frac1T\Pr(s_t=s\mid\pi,s_0)$.

Discounted case. For a stationary policy $\pi(a\mid s)$ and $0\le\gamma<1$, the normalized value, state-action value, advantage and discounted future state distribution are

$$V_{\pi,\gamma}(s)=(1-\gamma)\,\mathbb E\Big[\sum_{\tau\ge0}\gamma^\tau r(s_\tau,a_\tau)\,\Big|\,\pi,s_0=s\Big],\qquad Q_{\pi,\gamma}(s,a)=(1-\gamma)r(s,a)+\gamma\,\mathbb E_{s'}[V_{\pi,\gamma}(s')],$$ $$A_\pi(s,a)=Q_{\pi,\gamma}(s,a)-V_{\pi,\gamma}(s),\qquad d_{\pi,s_0,\gamma}(s)=(1-\gamma)\sum_{t\ge0}\gamma^t\Pr(s_t=s\mid\pi,s_0).$$

A parameterized policy is a family $\pi(a\mid s,\theta)$ (resp. $\pi(a\mid s,t,\theta)$) of policies indexed by $\theta\in\mathbb R^k$, each entry differentiable in $\theta$; $\nabla$ is the gradient in $\theta$.

Formalization targets

Goal: Theorem 4.2.4 (p. 48)

$$\nabla V_{\pi,\gamma}(s_0)=\frac1{1-\gamma}\,\mathbb E_{s\sim d_{\pi,s_0,\gamma}}\Big[\sum_a\nabla\pi(a\mid s,\theta)\,Q_{\pi,\gamma}(s,a)\Big].$$

The statement asserts that $\theta\mapsto V_{\pi_\theta,\gamma}(s_0)$ is differentiable at the given parameter and that its derivative is the right-hand side. It is the thesis's version of the Sutton–McAllester–Singh–Mansour theorem, and the result the rest of the thesis's discussion of gradient methods builds on.

Milestones

• Value representations (p. 47): $V_\pi(s_0)=\mathbb E_{(s,t)\sim d_{\pi,s_0}}\mathbb E_{a\sim\pi(\cdot\mid s,t)}[r(s,a)]$ and $V_{\pi,\gamma}(s_0)=\mathbb E_{s\sim d_{\pi,s_0,\gamma}}\mathbb E_{a\sim\pi(\cdot\mid s)}[r(s,a)]$.
• Theorem 4.2.3 (p. 48), the $T$-epoch gradient:

$$\nabla V_\pi(s_0)=T\,\mathbb E_{(s,t)\sim d_{\pi,s_0}}\Big[\sum_a\nabla\pi(a\mid s,t,\theta)\,Q_{\pi,t}(s,a)\Big].$$

• The advantage form (§5.4.2, p. 66), with $A=|A|$ the number of actions:

$$\nabla V_\pi(s_0)=\frac{A}{1-\gamma}\,\mathbb E_{s\sim d_{\pi,s_0}}\,\mathbb E_{a\sim\mathrm{Uniform}}\big[A_\pi(s,a)\,\nabla\pi(a\mid s,\theta)\big].$$

Significance

The result. The gradient formula contains no derivative of the state distribution: the effect of $\theta$ on which states are visited cancels, and the gradient is an expectation over states drawn from the current policy, weighted by a sum over actions. This is what makes Monte Carlo and actor-critic estimators possible, and it is the reason the thesis's sample-size analysis of §4.2.3 has no dependence on the size of the state space. The advantage form makes the limitation equally explicit: a small gradient certifies small advantages only under $d_{\pi,s_0}$, while the performance difference lemma (Lemma 5.2.1) shows that closeness to optimal is governed by advantages under $d_{\pi^*,s_0}$. That gap motivates the conservative policy iteration of Chapter 7.

Formalizing it. The theorems are proved in the thesis and in the cited literature; none of them is machine-checked in this normalized convention. The platform has a proved finite-horizon policy gradient theorem for a scalar parameter, a stationary policy and unnormalized values (policy_gradient_discounted_finite, policy_gradient_finite_horizon), and a posed direct-parameterization gradient for Agarwal et al.'s unnormalized discounted value (PolicyGradTheory.ProjGA.direct_gradient). This mission adds the multi-parameter statements, the non-stationary $T$-epoch version with its state-time distribution, and the infinite-horizon discounted version, where differentiability of an infinite series must be established rather than computed from a finite recursion.

Difficulty

In the $T$-epoch case the value is a finite polynomial in the policy entries, and the work is bookkeeping: unrolling the backward recursion for $V_{\pi,t}$ against the forward recursion for $\Pr(s_t=\cdot)$ so that the terms involving $\nabla V_{\pi,t+1}$ telescope. In the discounted case the obvious route, differentiating the recursion $V=(1-\gamma)r_\pi+\gamma P_\pi V$ term by term and recursing forever, presupposes that $\theta\mapsto V_{\pi_\theta,\gamma}(s)$ is differentiable, which the thesis's proof takes for granted. The value is an infinite series in $t$, so that differentiability is a genuine part of the claim, and the resulting formula must be matched with $d_{\pi,s_0,\gamma}$ and $Q_{\pi,\gamma}$, which are themselves defined as infinite series.

Formalization scope

• Finite $S$ and $A$ (Fintype), $A$ nonempty; transition kernel IsTransitionKernel P; rewards in $[0,1]$ as a standing hypothesis of every statement; $0\le\gamma<1$; $T\ge1$. The thesis's later chapters allow infinite state spaces; this mission is finite.
• Normalization exactly as in the thesis: $T$-epoch values and $d_{\pi,s_0}$ carry $1/T$, discounted values and $d_{\pi,s_0,\gamma}$ carry $1-\gamma$. Hence the factors $T$ and $1/(1-\gamma)$ in the gradient formulas.
• The discounted layer is the published normalized model ApproxOptRL.Shared.Model (value, qValue, advantage, futureStateDist; $d_{\pi,s_0,\gamma}$ is futureStateDist at the point mass on $s_0$). The $T$-epoch layer is defined in this mission (TEpoch): 0-based epochs, tValue by backward recursion, tQValue, stateDist, stateTimeDist.
• Parameters live in EuclideanSpace ℝ (Fin k). Every statement assumes that $\pi(\cdot\mid s,\theta)$ (resp. $\pi(\cdot\mid s,t,\theta)$ for $t<T$) is a probability distribution for every $\theta$, and that each entry is differentiable at the parameter $\theta_0$ ("the derivatives $\nabla\pi$ exist", p. 48). Differentiability of the value is not assumed.
• Gradients are stated with HasFDerivAt: the value map has the right-hand side as its Fréchet derivative at $\theta_0$. A statement with fderiv of the value alone, or with a policy that does not depend on $\theta$, would reduce to $0=0$ and is ruled out.
• Expectations over finite sets are finite sums; the uniform expectation over actions is $\frac1{|A|}\sum_a$.
• Contributions welcome: the forward/backward recursion identity for $T$-epoch values, summability and differentiability of the discounted series, and the closed form of $V_{\pi,\gamma}$ via $(I-\gamma P_\pi)^{-1}$; all are reusable by the other missions of this series.

Selected references

• S. M. Kakade, On the Sample Complexity of Reinforcement Learning, PhD thesis, Gatsby Computational Neuroscience Unit, University College London, 2003. https://discovery.ucl.ac.uk/id/eprint/10100726/
• R. S. Sutton, D. McAllester, S. Singh, Y. Mansour, Policy Gradient Methods for Reinforcement Learning with Function Approximation, Advances in Neural Information Processing Systems 12, 2000. https://proceedings.neurips.cc/paper/1999/hash/464d828b85b0bed98e80ade0a5c43b0f-Abstract.html
• R. J. Williams, Simple statistical gradient-following algorithms for connectionist reinforcement learning, Machine Learning 8, 229–256, 1992. https://doi.org/10.1007/BF00992696
• J. Baxter, P. L. Bartlett, Infinite-Horizon Policy-Gradient Estimation, Journal of Artificial Intelligence Research 15, 319–350, 2001. https://doi.org/10.1613/jair.806
• V. R. Konda, J. N. Tsitsiklis, Actor-Critic Algorithms, Advances in Neural Information Processing Systems 12, 2000. https://proceedings.neurips.cc/paper/1999/hash/6449f44a102fde848669bdd9eb6b76fa-Abstract.html

Motivation

Most practical reinforcement-learning methods do not compute value functions exactly. They alternate between estimating a value function from data, usually with a parametric approximator, and acting greedily with respect to that estimate. Approximate value iteration and approximate policy iteration are the two classical schemes of this kind, and their error analysis decides how accuracy in the estimation step translates into quality of the policies produced. Chapter 3 of S. M. Kakade's thesis On the Sample Complexity of Reinforcement Learning (University College London, 2003) collects the basic guarantees, developed from Bertsekas (Dynamic Programming: Deterministic and Stochastic Models, 1987) for greedy policies, Singh and Yee (1994), and Bertsekas and Tsitsiklis, Neuro-Dynamic Programming (Athena Scientific, 1996). The bounds are stated in terms of the worst-case (max-norm) error of the evaluation step, and the thesis uses them to argue that max-norm error is the obstacle to state-space-independent sample complexity results for these methods, which motivates the later chapters of the thesis.

Setting

A finite discounted Markov decision process consists of a finite set of states $S$, a finite nonempty set of actions $A$, a transition kernel $P(s'\mid s,a)$ (for every $(s,a)$ a probability distribution over $S$), a deterministic reward $r(s,a)\in[0,1]$, and a discount factor $0\le\gamma<1$. A policy $\pi(a\mid s)$ is a probability distribution over actions for every state; a deterministic policy is a map $f:S\to A$, identified with the policy that plays $f(s)$ with probability one.

Values are normalized: the value of $\pi$ at $s$ is

$$V_\pi(s)=(1-\gamma)\,\mathbb E\Big[\sum_{t\ge0}\gamma^t r(s_t,a_t)\,\Big|\,\pi,\ s_0=s\Big],$$

and the state-action value is $Q_\pi(s,a)=(1-\gamma)r(s,a)+\gamma\,\mathbb E_{s'\sim P(\cdot\mid s,a)}[V_\pi(s')]$. With rewards in $[0,1]$, every value lies in $[0,1]$. An optimal policy $\pi^*$ has $V_{\pi^*}(s)\ge V_\pi(s)$ for every policy $\pi$ and state $s$; write $V^*=V_{\pi^*}$ and $Q^*=Q_{\pi^*}$. The max norm is $\|x\|_\infty=\max_s|x(s)|$ on state vectors and $\max_{s,a}|x(s,a)|$ on state-action arrays.

The backup operator is $[BJ](s)=\max_a\big((1-\gamma)r(s,a)+\gamma\,\mathbb E_{s'\sim P(\cdot\mid s,a)}[J(s')]\big)$. A deterministic policy $f$ is greedy with respect to $Q$ if $f(s)\in\arg\max_a Q(s,a)$ for every $s$.

• $\gamma$-approximate value iteration produces vectors $J_0=0,J_1,J_2,\dots$ with $\|J_t-BJ_{t-1}\|_\infty\le\varepsilon$, and greedy policies $\pi_t$ for the lookahead $(1-\gamma)r(s,a)+\gamma\,\mathbb E_{s'}[J_t(s')]$.
• $\gamma$-approximate policy iteration starts from any deterministic $\pi_0$, forms an estimate $\tilde Q_t$ of $Q_{\pi_t}$ with $\|\tilde Q_t-Q_{\pi_t}\|_\infty\le\varepsilon$, and takes $\pi_{t+1}$ greedy with respect to $\tilde Q_t$.

Formalization targets

Goal: Theorem 3.2.2 (approximate policy iteration)

$$\limsup_{t\to\infty}\|V^*-V_{\pi_t}\|_\infty\le\frac{2\varepsilon}{(1-\gamma)^2}.$$

The policies need not converge; the statement bounds where they end up.

Milestones

• Theorem 3.1.1: if $\|\tilde Q-Q^*\|_\infty\le\varepsilon$ and $\pi$ is greedy for $\tilde Q$, then $V_\pi(s)\ge V^*(s)-\frac{2\varepsilon}{1-\gamma}$ for all $s$.
• Lemma 3.2.3: $\|V^*-V_{\pi_{t+1}}\|_\infty\le\gamma\|V^*-V_{\pi_t}\|_\infty+\frac{2\varepsilon}{1-\gamma}$.
• Rate of approximate policy iteration (p. 41): $\|V^*-V_{\pi_t}\|_\infty\le\gamma^t+\frac{2\varepsilon}{(1-\gamma)^2}$.
• Contraction of the backup (p. 26): $\|BJ-BJ'\|_\infty\le\gamma\|J-J'\|_\infty$.
• Approximate value iteration (p. 40): $\|V^*-J_t\|_\infty\le\gamma^t+\frac{\varepsilon}{1-\gamma}$.
• Rate of approximate value iteration (p. 41): $\|V^*-V_{\pi_t}\|_\infty\le\frac{2\gamma^t}{1-\gamma}+\frac{2\varepsilon}{(1-\gamma)^2}$.
• Theorem 3.2.1: the same lim sup bound $\frac{2\varepsilon}{(1-\gamma)^2}$ for approximate value iteration.

Significance

The results give the standard performance guarantee for greedy approximate dynamic programming: an evaluation error of $\varepsilon$ in max norm costs at most $2\varepsilon/(1-\gamma)^2$ in max-norm suboptimality, uniformly over the asymptotic set of policies, with a geometric rate of approach. Example 3.1.2 of the thesis shows that the factor $2\varepsilon/(1-\gamma)$ of Theorem 3.1.1 is attained, so the greedy step itself cannot be improved; the two factors of the horizon $1/(1-\gamma)$ in the limit bound are the reason the thesis turns to other error measures in later chapters.

All the statements are classical and proved in the literature (Bertsekas–Tsitsiklis 1996, Chapter 6, in the unnormalized model and with a factor $\gamma$ to spare in the limit bounds); Lemma 3.2.3 and Theorem 3.2.2 are stated in the thesis without proof. To our knowledge none has a machine-checked proof. The mission produces formal proofs in the normalized model shared with the formalization of Kakade–Langford (2002) on this platform, so later chapters of the series (conservative policy iteration, policy search) can compare against them.

Difficulty

Approximate policy iteration is not monotone: with evaluation errors, $V_{\pi_{t+1}}$ can be worse than $V_{\pi_t}$ at some states, so the argument of exact policy iteration, which uses $V_{\pi_{t+1}}\ge V_{\pi_t}$ everywhere, does not apply. The difficulty of Lemma 3.2.3 is to control the distance to optimality without improvement at each step, combining the greedy step with the lack of monotonicity of the new policy's value; the thesis calls the proof of Theorem 3.2.2 "somewhat technical" and omits it. A second, mechanical difficulty is that the normalized value $V_\pi$ is defined as an infinite series, so its Bellman equation $V_\pi(s)=Q_\pi(s,\pi(s))$, the optimality equation $V^*=BV^*$ and the bound $0\le V_\pi\le1$ have to be derived from that definition before any of the recursions can be run.

Formalization scope

• The model is the published normalized model ApproxOptRL.Shared.Model: value P r γ π is $V_\pi$ (defined as $(1-\gamma)$ times a tsum), qValue is $Q_\pi$. $S$ and $A$ are finite types, $A$ nonempty; $P$ satisfies IsTransitionKernel; every statement assumes $0\le r\le1$ and $0\le\gamma<1$.
• The optimal policy is a binder $\pi^*$ with IsOptimalPolicy P r γ πstar (a stationary stochastic policy dominating every stationary stochastic policy at every state). Such a policy exists for every finite MDP (p. 26 of the thesis), and for finite MDPs it is optimal among all policies.
• Policies of the runs are deterministic, S → A, and are evaluated through the indicator policy detPolicy. "Greedy" is the relation ∀ s a, Q s a ≤ Q s (f s): every tie-breaking rule is covered.
• The runs are sequences indexed by ℕ, with the greedy and accuracy conditions as hypotheses at every index; the value-iteration condition is written for indices $t+1$ and $t$.
• $\|\cdot\|_\infty$ is Mathlib's sup norm on S → ℝ and S → A → ℝ.
• The lim sup statements are in $\varepsilon$–$N$ form: for every $\delta>0$ the bound plus $\delta$ holds eventually.
• Ruled out: the accuracy hypothesis is stated against $Q_{\pi_t}$, the value of the current policy, not against $Q^*$, and the greedy relation genuinely constrains $\pi_{t+1}$; with either changed, the hypotheses would be unsatisfiable or the policies unconstrained and the theorem empty.
• Infrastructure needed and reusable beyond this mission: the Bellman equation of the normalized value for indicator policies, $V^*=BV^*$, monotonicity and contraction of policy-evaluation and backup operators in the normalized model, and the bound $0\le V_\pi\le1$. Contributions of these lemmas are welcome.

Selected references

• S. M. Kakade, On the Sample Complexity of Reinforcement Learning, PhD thesis, Gatsby Computational Neuroscience Unit, University College London, 2003. https://discovery.ucl.ac.uk/id/eprint/10100726/
• D. P. Bertsekas and J. N. Tsitsiklis, Neuro-Dynamic Programming, Athena Scientific, 1996. ISBN 1-886529-10-8.
• S. P. Singh and R. C. Yee, An upper bound on the loss from approximate optimal-value functions, Machine Learning 16 (1994), 227–233. https://doi.org/10.1007/BF00993104
• S. M. Kakade and J. Langford, Approximately optimal approximate reinforcement learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005