Operations Research

Motivation

Assortment optimization asks which set of products a firm should offer when customers choose among the offered products according to a discrete choice model; it underlies shelf-space planning in retail and fare-class control in airline revenue management (Talluri and van Ryzin, 2004). Under the nested logit model products are grouped into nests, and a customer first picks a nest and then a product inside it. Davis, Gallego and Topaloglu (Operations Research, 2014; DOI 10.1287/opre.2014.1256) map out how hard this problem is across variants of the model.

When every nest dissimilarity parameter is at most one and a customer who chose a nest always buys there, offering the top-revenue products of each nest is optimal (Theorem 4 of the paper, the subject of an earlier mission of this series). Once a customer may leave a nest without buying — a partially-captured nest — that structure breaks and the problem becomes NP-hard (Theorem 8). This mission targets the paper's response: a small, explicitly constructed family of candidate assortments per nest from which a linear program recovers a solution within a factor of two of optimal.

Setting

There are $m$ nests $M$ and, in each nest, $n$ products $N = \{1, \dots, n\}$. Product $j$ of nest $i$ has a revenue $r_{ij} \ge 0$ and a preference weight $v_{ij} > 0$, with $r_{i1} \ge \dots \ge r_{in}$. Nest $i$ has a dissimilarity parameter $\gamma_i > 0$ and a within-nest no-purchase weight $v_{i0} \ge 0$; $v_0 \ge 0$ is the weight of choosing no nest. For an assortment $S_i \subseteq N$,

$$V_i(S_i) = v_{i0} + \sum_{j \in S_i} v_{ij}, \qquad R_i(S_i) = \frac{\sum_{j \in S_i} r_{ij} v_{ij}}{V_i(S_i)},\quad R_i(\emptyset)=0,$$

and the expected revenue of $(S_1, \dots, S_m)$ is $\Pi = \sum_i V_i(S_i)^{\gamma_i} R_i(S_i) / (v_0 + \sum_i V_i(S_i)^{\gamma_i})$. The optimal expected revenue $Z^*$ is the optimal value of the linear program

$$\text{(3)}\quad \min\ x \quad\text{s.t.}\quad v_0 x \ge \sum_{i \in M} y_i,\qquad y_i \ge V_i(S_i)^{\gamma_i}\big(R_i(S_i) - x\big)\ \ \forall S_i \subseteq N,\ i \in M,$$

and problem (4) is the same program with the second family of constraints imposed only for a chosen collection of candidate assortments in each nest.

Throughout, $\gamma_i \le 1$ for every nest and the $v_{i0}$ are arbitrary. For a capacity $\epsilon_i \ge 0$, the knapsack value $K_i(\epsilon_i)$ is the largest $\sum_{j \in S} r_{ij} v_{ij}$ over assortments $S$ with $\sum_{j \in S} v_{ij} \le \epsilon_i$ (display (9)). Its continuous relaxation (11) allows fractional $z_{ij} \in [0, \mathbf 1(v_{ij} \le \epsilon_i)]$ under the same capacity. The greedy solution $\hat z_i(\epsilon_i)$ of (11) fills the capacity with the products of weight at most $\epsilon_i$ in revenue order, each fully while it fits and the next one fractionally, and

$$\hat S_i(\epsilon_i) = \{ j \in N : \hat z_{ij}(\epsilon_i) = 1 \}.$$

Problem (10) replaces the per-assortment constraints of (3) by $y_i \ge \max_{\epsilon_i \ge 0} (v_{i0}+\epsilon_i)^{\gamma_i}[K_i(\epsilon_i)/(v_{i0}+\epsilon_i) - x]$.

Formalization targets

Goal: Theorem 10 (p. 24)

Let $(\hat x, \hat y)$ be an optimal solution of (4) with candidate collections $\{\hat S_i(\epsilon_i) : \epsilon_i \in [0,\infty]\} \cup \{\{j\} : j \in N\}$. Then

$$(2\hat x,\ 2\hat y) \ \text{ is feasible for (3).}$$

Milestones

1. Per-nest identity (proof of Lemma 9, p. 23). For $x \ge 0$, $\max_{S_i} V_i(S_i)^{\gamma_i}(R_i(S_i) - x) = \max_{\epsilon_i \ge 0}(v_{i0}+\epsilon_i)^{\gamma_i}[K_i(\epsilon_i)/(v_{i0}+\epsilon_i) - x]$.
2. Lemma 9 (p. 23). Problems (3) and (10) have the same optimal solutions.
3. Relaxation (p. 23). Every feasible point of (9) is feasible for (11), so $\hat K_i(\epsilon_i) \ge K_i(\epsilon_i)$.
4. Greedy solution (pp. 23–24). $\hat z_i(\epsilon_i)$ is optimal for (11) and has at most one fractional component.
5. Sign (A.3, p. 45). $\hat x \ge 0$.
6. Inequalities (28) and (29) (A.3, pp. 45–46). In both cases — $\hat z_i(\epsilon)$ with and without a fractional component — $2\hat y_i \ge (v_{i0}+\epsilon)^{\gamma_i}[K_i(\epsilon)/(v_{i0}+\epsilon) - 2\hat x]$.

Two further statements accompany the goal: the factor-two revenue guarantee obtained from Theorem 10 and Theorem 1 of the paper, and the fact that every $\hat S_i(\epsilon_i)$ is one of the at most $1 + n^2$ assortments $N^k_{ij}$, the first $j$ products by revenue among the $k$ lightest.

Significance

Theorem 10 turns an NP-hard assortment problem into a linear program with $1 + m$ variables and $1 + m(1 + n + n^2)$ constraints whose solution is within a factor of two of optimal. The construction is explicit: the candidates are defined by a greedy rule, not by an optimization oracle. The same template, a restricted linear program whose doubled optimum is feasible for the full one, is reused in §6 of the paper for the most general instances, and Lemma 9's knapsack reformulation is the link to the classical approximation theory of knapsack problems (Williamson and Shmoys, 2011).

The theorem is proved in the paper. No machine-checked proof of it, of Lemma 9, or of greedy optimality for the continuous knapsack with an eligibility bound exists on the platform. Formalizing it yields a checked factor-two guarantee and a reusable fractional-knapsack development.

Difficulty

The obvious argument would compare the restricted program (4) with (3) constraint by constraint. That fails: (3) has one constraint per subset of products, and most subsets are not candidates. The comparison has to pass through the knapsack reformulation (10), which requires showing that a maximum over all subsets equals a maximum over a one-dimensional capacity parameter, using $\gamma_i \le 1$ and $x \ge 0$ in an essential way. The second obstacle is that the greedy assortment $\hat S_i(\epsilon_i)$ keeps only the fully taken products, so its value can fall short of the continuous knapsack value, and no single candidate assortment need attain the knapsack bound. With dissimilarity parameters above one the monotonicity behind the reformulation is lost, and §6 of the paper needs a different factor.

Formalization scope

Products are Fin n (indices $0, \dots, n-1$), nests a finite type, and every quantity is real. Powers are Real.rpow; $x/0 = 0$, which gives $R_i(\emptyset) = 0$. An optimal solution of a linear program is a feasible pair whose $x$ is minimal among feasible pairs. The constraint "$y_i \ge \max_{\epsilon_i \ge 0}(\dots)$" of (10) is stated in constraint form, for every $\epsilon_i \ge 0$, so no real supremum is taken. $K_i(\epsilon)$ is defined for $\epsilon \ge 0$ only; its placeholder value for $\epsilon < 0$ is never used. Ties in revenue (and, for $N^k_{ij}$, in weight) are broken by index. The candidate collection is taken over real $\epsilon_i \ge 0$; $\epsilon_i = \infty$ adds nothing, since every capacity of at least $\sum_j v_{ij}$ already gives $\hat S_i = N$.

Standing assumptions and added hypotheses: $\gamma_i \le 1$ for every nest (the section's assumption) on the goal and on every model milestone; the pins $v_{ij} > 0$, $r_{ij} \ge 0$, $\gamma_i > 0$ and the revenue ordering, shared by the series; $n \ge 1$ on Lemma 9, on $\hat x \ge 0$ and on (28)/(29), the paper's nonempty $N$; and $v_0 > 0$ on the factor-two revenue guarantee, where Theorem 1 of the paper fails without it.

The greedy assortments $\hat S_i(\epsilon_i)$ are defined explicitly. Quantifying over arbitrary optimal solutions of (11) instead would change the candidate collection and is not the paper's theorem. The goal states feasibility for the full program (3) and does not mention knapsack values, the greedy solution or the case split. A formalization that weakens the conclusion to feasibility for (10), or that drops the singletons from the candidate collection, is not a solution.

Needed infrastructure: fractional knapsack optimality of the greedy rule with an eligibility bound, monotonicity of $t \mapsto t^{\gamma}$ and $t \mapsto t^{\gamma - 1}$ for $\gamma \le 1$, and finite maximization over subsets. The fractional-knapsack lemmas are reusable beyond this mission. Proofs of any milestone, and alternative decompositions of the goal, are welcome.

Selected references

• J. M. Davis, G. Gallego, H. Topaloglu, Assortment Optimization under Variants of the Nested Logit Model, Operations Research 62(2), 2014 (revised manuscript of June 18, 2013, cited here). DOI 10.1287/opre.2014.1256
• K. T. Talluri, G. J. van Ryzin, Revenue Management Under a General Discrete Choice Model of Consumer Behavior, Management Science 50(1), 15–33, 2004. DOI 10.1287/mnsc.1030.0147
• D. P. Williamson, D. B. Shmoys, The Design of Approximation Algorithms, Cambridge University Press, 2011. DOI 10.1017/CBO9780511921735

Motivation

A retailer that sells products in several categories, channels or stores has to decide which products to offer in each. Customers substitute: a product left out of the assortment sends some of its demand to other products, and some of it away. The nested logit model (McFadden 1974, 1981) is the standard choice model for this situation. It groups products into nests, so that substitution within a nest differs from substitution across nests. Assortment optimization under this model asks which products to offer in each nest so as to maximize expected revenue.

Davis, Gallego and Topaloglu (Oper. Res. 62(2), 2014) split the problem into four cases: dissimilarity parameters at most one or unrestricted, and nests that are fully or only partially captured. The problem is polynomially solvable in the first case and NP-hard in the other three. Every approximation guarantee in the paper for the hard cases (Theorems 7, 10, 11, 12) comes from one general framework, set up in §2: a linear program equivalent to the assortment problem, and Theorem 1, which turns a feasibility certificate for that linear program into a performance guarantee. This mission formalizes that framework.

Setting

There are $m$ nests $M$ and $n$ products $N = \{1, \dots, n\}$ in each nest. Product $j$ of nest $i$ has revenue $r_{ij} \ge 0$ and preference weight $v_{ij} > 0$, and the products in each nest are ordered so that $r_{i1} \ge \dots \ge r_{in}$. Nest $i$ has a no-purchase weight $v_{i0} \ge 0$ and a dissimilarity parameter $\gamma_i > 0$. The weight of choosing no nest at all is $v_0 \ge 0$. If the assortment $S_i \subseteq N$ is offered in nest $i$, write

$$V_i(S_i) = v_{i0} + \sum_{j \in S_i} v_{ij}, \qquad R_i(S_i) = \frac{\sum_{j\in S_i} r_{ij} v_{ij}}{V_i(S_i)}, \quad R_i(\emptyset) = 0 .$$

A customer picks nest $i$ with probability $Q_i = V_i(S_i)^{\gamma_i} / (v_0 + \sum_{l\in M} V_l(S_l)^{\gamma_l})$, and then a product of that nest by the multinomial logit model. The expected revenue is

$$\Pi(S_1, \dots, S_m) = \sum_{i \in M} Q_i(S_1, \dots, S_m)\, R_i(S_i),$$

and problem (2) is $Z^* = \max_{S_i \subseteq N} \Pi(S_1, \dots, S_m)$.

The linear program (3) in the variables $(x, y_1, \dots, y_m)$ minimizes $x$ subject to

$$v_0 x \ge \sum_{i\in M} y_i, \qquad y_i \ge V_i(S_i)^{\gamma_i}\big(R_i(S_i) - x\big) \quad \forall S_i \subseteq N,\ i \in M.$$

Given candidate collections $\{A_{it} : t \in \mathcal T_i\}$ of assortments for each nest, the linear program (4) is (3) with the second family of constraints imposed only for $S_i$ in the collection of nest $i$.

Formalization targets

Goal: Theorem 1 (p. 13)

Let $(\hat x, \hat y)$ be an optimal solution of (4), and let $\hat S_i$ solve $\max_{S_i \in \{A_{it}\}} V_i(S_i)^{\gamma_i}(R_i(S_i) - \hat x)$, problem (5), in every nest. If $(\alpha \hat x, \beta \hat y)$ is feasible for (3) for some $\alpha, \beta$, then, with $\hat Z = \Pi(\hat S_1, \dots, \hat S_m)$,

$$\alpha \hat Z \ \ge\ Z^* \ \ge\ \hat Z .$$

The theorem fixes no candidate collection and no value of $\alpha$. Each later section of the paper instantiates it with its own collection and its own factor, so a formal proof applies to all of them.

Milestones (§2, pp. 11–12)

1. Problem (2) is equivalent to (3): $Z^*$ is the least $x$ for which some $y$ makes $(x, y)$ feasible for (3).
2. At an optimal solution of (4), the first constraint binds at the maximizers $\hat S_i$ of (5), and $\hat x = \Pi(\hat S_1, \dots, \hat S_m)$.
3. Problem (4) relaxes (3), so $\hat x \le Z^*$.

Companions (§7, pp. 29–30)

• The tighter program (16), which lets each nest's assortment be a fractional vector $z_i \in [0,1]^n$, has every feasible $x$ above $Z^*$.
• Proposition 13: $\hat F_i(x) = \max_{z_i \in [0,1]^n} F_i(z_i \mid x)$ is convex, with subgradient $-(v_{i0} + \sum_j v_{ij}\hat z_{ij}(x))^{\gamma_i}$ at $x$.

Significance

Theorem 1 is the common step behind the paper's four approximation guarantees: the factor $\rho$ or $2\kappa$ of Theorem 7, the factor 2 of Theorem 10, the factor of Theorem 11, and the $\delta^{2\bar\gamma+1}$ of Theorem 12. Each of these reduces to checking that a scaled optimum of a small linear program is feasible for (3). With Theorem 1 formalized, those guarantees reduce to inequalities about candidate collections, which are the subject of the sister missions of this series. The upper bound (16) and Proposition 13 give the instance-specific bound that the paper uses to assess its assortments numerically.

The results are proved in the paper. To our knowledge none of them has a machine-checked proof. The formal work adds two things: the statements below are made exact at the degenerate inputs the prose passes over (an empty assortment, $v_0 = 0$), and a formal proof certifies the framework once for every later instantiation.

Difficulty

The equivalence of (2) and (3) rests on decomposing a maximum over joint assortments into a sum of per-nest maxima, and on reading the fractional objective $\Pi \le x$ as a linear constraint. Both steps need care where a denominator $v_0 + \sum_i V_i(S_i)^{\gamma_i}$ can vanish. The binding argument for (4) is a perturbation argument: lowering $\hat x$ must keep every constraint satisfiable, which needs a continuity and monotonicity property of the right-hand side in $x$. The obvious one-line reading of Theorem 1, "$\hat x = \hat Z$ and $\alpha\hat x \ge Z^*$", is correct only once both of these facts are established with their hypotheses. In particular, it is false when $v_0 = 0$ (see below). Proposition 13 requires that the supremum over the box be finite, which comes from the boundedness of $F_i$ on $[0,1]^n$.

Formalization scope

Nests are a finite type ι and products are Fin n, indexed $0, \dots, n-1$. An assortment is a finite set of products per nest, and a candidate collection is a set of such finite sets. Powers are real powers, and Lean's $x / 0 = 0$ gives $R_i(\emptyset) = 0$. $Z^*$ is $\Pi(S^*)$ for an arbitrary optimal assortment $S^*$; no supremum over assortments is taken. "Optimal solution of (4)" means feasible with minimal $x$, and "$\hat S_i$ solves (5)" means $\hat S_i$ belongs to the collection of nest $i$ and maximizes the objective of (5) over it at $\hat x$.

Standing assumptions and pins. These are $v_0, v_{i0} \ge 0$ and ordered revenues, together with $v_{ij} > 0$, $r_{ij} \ge 0$ and $\gamma_i > 0$. The paper allows zero-weight padding products and $\gamma_i = 0$, but its own conventions fail there. Theorem 1 and the binding milestone add $v_0 > 0$. The page allows $v_0 = 0$, but then Theorem 1 is false: take one nest with $v_{10} = 0$, $\gamma_1 = 1$, $r_{11} = v_{11} = 1$ and candidates $\{\emptyset, \{1\}\}$. Then $\hat x = 1$ and $\hat S_1 = \emptyset$ meet every hypothesis with $\alpha = \beta = 1$, yet $\hat Z = 0 < Z^* = 1$. The equivalence of (2) and (3) and the bound from (16) keep $v_0 \ge 0$, as the page does, and assume at least one nest and one product: with neither and $v_0 = 0$, every $x$ is feasible for (3).

A formalization that assumes the binding equality, the identity $\hat x = \hat Z$, or the inequality $\hat x \le Z^*$ in the goal would trivialize it. Those facts appear only as milestones. Likewise, reading "optimal solution of (4)" as mere feasibility would make the goal false rather than easier.

The development needs only finite sums, real powers and elementary order reasoning. Proposition 13 also needs the boundedness of a continuous function on a box and the convexity of a pointwise supremum of affine functions. Welcome contributions include proofs of the milestones, the goal from them, and reusable lemmas on the per-nest decomposition of maxima, which the sister missions of this series use as well.

Selected references

• J. M. Davis, G. Gallego, H. Topaloglu, Assortment optimization under variants of the nested logit model, Operations Research 62(2), 2014 (revised manuscript of June 18, 2013, cited here). https://doi.org/10.1287/opre.2014.1256
• D. McFadden, Econometric models of probabilistic choice, in C. Manski, D. McFadden (eds.), Structural Analysis of Discrete Data with Econometric Applications, MIT Press, 1981. https://eml.berkeley.edu/~mcfadden/discrete.html
• P. Rusmevichientong, D. Shmoys, H. Topaloglu, Assortment optimization with mixtures of logits, Technical report, Cornell University, 2010. https://people.orie.cornell.edu/huseyin/publications/publications.html
• M. S. Bazaraa, H. D. Sherali, C. M. Shetty, Nonlinear Programming: Theory and Algorithms, 2nd ed., Wiley, 1993. https://doi.org/10.1002/0471787779

Motivation

In most control problems the controller does not see the state of the system. It sees noisy observations, remembers its past controls, and must act on that record. Inventory systems with delayed or inaccurate counts, maintenance of machines whose wear is only inspected, target tracking, and medical treatment planned from test results all have this form. The standard device for such problems is to replace the hidden state by a summary of the record, most often the conditional distribution of the state given the observations, and to solve a dynamic program whose state is that summary.

For finite or countable spaces this reduction goes back to Åström (1965) and Striebel (1965), who introduced the conditional distribution of the state as a "sufficient statistic" for control. Chapter 10 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (Academic Press 1978; Athena Scientific 1996) carries it out for Borel state, control and observation spaces, with universally measurable policies and costs that are only lower semianalytic. In that generality the measurability of the reduced model is the whole difficulty, and the chapter isolates exactly what a summary must satisfy for the reduction to be exact.

Setting

The imperfect state information model (ISI) of Definition 10.3 has a nonempty Borel state space $S$, control space $C$ and observation space $Z$; a discount factor $\alpha>0$; a lower semianalytic cost $g:SC\to R^*=[-\infty,\infty]$; a Borel state transition kernel $t(dx'\mid x,u)$; Borel observation kernels $s_0(dz\mid x)$ and $s(dz\mid u,x)$; and a horizon $N$. The initial state $x_0$ has distribution $p\in P(S)$, $z_0\sim s_0(\cdot\mid x_0)$, and then $x_{k+1}\sim t(\cdot\mid x_k,u_k)$, $z_{k+1}\sim s(\cdot\mid u_k,x_{k+1})$. The controller knows the information vector $i_k=(z_0,u_0,\dots,u_{k-1},z_k)\in I_k$ and must choose $u_k\in U_k(i_k)$, where the constraint set $\Gamma_k=\{(i_k,u)\mid u\in U_k(i_k)\}$ is analytic.

A policy $\pi=(\mu_0,\dots,\mu_{N-1})$ consists of universally measurable stochastic kernels $\mu_k(du_k\mid p;i_k)$ that respect the constraints (Definition 10.4). Together with $p$ it determines probability measures $P_k(\pi,p)$ on the histories $(x_0,z_0,u_0,\dots,x_k,z_k,u_k)$, the cost

$$J_{N,\pi}(p)=\int\Big[\sum_{k=0}^{N-1}\alpha^k g(x_k,u_k)\Big]dP_{N-1}(\pi,p),$$

and the optimal cost $J^*_N(p)=\inf_\pi J_{N,\pi}(p)$ (Definition 10.5). Assumption $(F^+)$ asks that the expected discounted negative part of the cost be finite for every policy and initial distribution; $(F^-)$ asks the same of the positive part.

A statistic is a sequence of Borel maps $\eta_k:P(S)I_k\to Y_k$ into nonempty Borel spaces. It is sufficient for control (Definition 10.6) if (a) the constraints can be read off from it, $\Gamma_k=\{(i_k,u)\mid(\eta_k(p;i_k),u)\in\hat\Gamma_k\}$ with $\hat\Gamma_k$ analytic; (b) the conditional law of $\eta_{k+1}$ given $(\eta_k,u_k)$ is a Borel kernel $\hat t_k(dy_{k+1}\mid y_k,u_k)$, for every $p$ and every policy; and (c) the conditional expectation of $g(x_k,u_k)$ given $(\eta_k,u_k)$ is a lower semianalytic function $\hat g_k(y_k,u_k)$. The perfect state information model (PSI) of Definition 10.7 has states $y_k\in Y_k$, constraints $\hat U_k(y_k)=(\hat\Gamma_k)_{y_k}$, costs $\hat g_k$ and transitions $\hat t_k$; its cost and optimal cost at $y\in Y_0$ are $\hat J_{N,\hat\pi}(y)$ and $\hat J^*_N(y)$. The initial distribution of $y_0$ is

$$\varphi(p)(\underline Y_0)=\int_S s_0(\{z_0\mid\eta_0(p;z_0)\in\underline Y_0\}\mid x_0)\,p(dx_0).$$

A Markov (PSI) policy $\hat\mu_k(du\mid y_k)$ acts in (ISI) through $\mu_k(du\mid p;i_k)=\hat\mu_k(du\mid\eta_k(p;i_k))$.

Formalization targets

Goal: Proposition 10.3

Under $(F^+,\hat F^+)$ or $(F^-,\hat F^-)$,

$$J^*_N(p)=\int_{Y_0}\hat J^*_N(y_0)\,\varphi(p)(dy_0)\qquad\forall p\in P(S),$$

and a Markov (PSI) policy that is optimal, $\varphi(p)$-optimal or weakly $\varphi(p)$-$\varepsilon$-optimal for (PSI) is respectively optimal, optimal at $p$, or $\varepsilon$-optimal at $p$ for (ISI); under $(F^+,\hat F^+)$ an $\varepsilon$-optimal (PSI) policy is $\varepsilon$-optimal for (ISI). Here $\hat\pi$ is weakly $q$-$\varepsilon$-optimal if $\int\hat J_{N,\hat\pi}\,dq\le\int\hat J^*_N\,dq+\varepsilon$ when $\int\hat J^*_N\,dq>-\infty$ and $\int\hat J_{N,\hat\pi}\,dq\le-1/\varepsilon$ otherwise, and $q$-optimal if $q(\{y_0\mid\hat J_{N,\hat\pi}(y_0)=\hat J^*_N(y_0)\})=1$ (Definition 10.8).

Milestones

1. Lemma 10.1: the process $(\eta_0,u_0,\dots,\eta_k,u_k)$ generated in (ISI) by a Markov (PSI) policy has the law $\hat P_k[\hat\pi,\varphi(p)]$.
2. Proposition 10.2: $J_{N,\hat\pi}(p)=\int\hat J_{N,\hat\pi}\,d\varphi(p)$ for Markov $\hat\pi$.
3. Corollary 10.2.1: $J^*_N(p)\le\int\hat J^*_N\,d\varphi(p)$.
4. Lemma 10.2: every (ISI) policy is matched in cost by some Markov (PSI) policy.
5. Proposition 10.4: $\varepsilon$-optimal nonrandomized (ISI) policies that depend on $i_k$ only through $\eta_k(p;i_k)$.
6. Proposition 10.6: the identity maps on $P(S)I_k$ form a statistic sufficient for control.

Significance

Proposition 10.3 says that an imperfect-information problem loses nothing by being solved in the reduced model: the optimal cost is the $\varphi(p)$-average of the reduced optimal cost, and good reduced policies are good original policies. Combined with Proposition 10.6, every (ISI) model has such a reduction, so the finite-horizon dynamic programming theory of Chapter 8 (existence of $\varepsilon$-optimal policies, the dynamic programming algorithm) transfers to partially observed problems on Borel spaces. Proposition 10.4 turns this into a structural statement about the original problem: nearly optimal controllers need to retain only the statistic.

These results are proved in the book. None of them is formalized: the platform's related results (Bäuerle–Rieder's partially observable models with observation densities, and the linear-quadratic-Gaussian separation theorem) work in different models and do not cover universally measurable policies, analytic constraints, or lower semianalytic costs. A machine-checked version makes the conditional-expectation bookkeeping of the reduction explicit, and the definitions of this mission (universal measurability, lower semianalytic functions, the book's extended integral, history measures built from universally measurable kernels) are reusable by every other chapter of the book.

Difficulty

The obvious argument says: replace the state by the statistic, observe that costs and transitions depend only on the statistic, and conclude. In the Borel setting each step is a measurability claim that the naive argument does not supply. The conditions of Definition 10.6 are almost-everywhere statements about conditional distributions under every pair $(p,\pi)$, while the reduced model needs genuine kernels; the policies are only universally measurable, so integrals and compositions must be taken with respect to completions; the costs take the values $\pm\infty$, so interchanging sums and integrals requires the finiteness assumptions $(F^\pm)$ and $(\hat F^\pm)$; and the inequality $J^*_N\ge\int\hat J^*_N\,d\varphi(p)$ requires producing, from an arbitrary history-dependent (ISI) policy, a Markov (PSI) policy with the same cost, which the naive argument does not do.

Formalization scope

• Horizon. Only finite horizons $N\ge1$ are covered, hence only the cases $(F^+,\hat F^+)$ and $(F^-,\hat F^-)$ of the book's statements; the infinite-horizon cases $(P,\hat P)$, $(N,\hat N)$, $(D,\hat D)$ are out of scope.
• Extended reals. Costs live in EReal with the book's convention $\infty-\infty=+\infty$ written out explicitly (badd, bsum, extIntegral); Mathlib's EReal subtraction ($\top-\top=\bot$) is never used where both terms can be infinite.
• Spaces and measures. $S$, $C$, $Z$, $Y_k$ are Borel spaces in the sense of Definition 7.7 with their Borel $\sigma$-algebras; $P(S)$ carries the weak topology and the Giry $\sigma$-algebra. Policies are families of maps into ProbabilityMeasure C that are measurable for the completion of every probability measure. History measures are characterized by their values on rectangles. Families indexed by the stage are indexed by all of $\mathbb N$; only stages $k<N$ are constrained.
• Conditional statements. Conditions (22) and (23) are stated through the defining relations of conditional probability and expectation, for every $p$ and every policy, with (23) required when $g(x_k,u_k)$ is quasi-integrable.
• Policies in Proposition 10.3. The (PSI) policies in the optimality transfers are Markov, as in Proposition 10.2.
• No trivialization. Definition 10.6 is the full definition: analytic $\hat\Gamma_k$ with full projection, Borel kernels $\hat t_k$ satisfying (22) for every $p$ and policy, and lower semianalytic $\hat g_k$ satisfying (23); a weaker notion would make Proposition 10.6 empty.

Contributions are welcome on any milestone. Basic facts that a full development needs, such as composition of universally measurable maps (Proposition 7.44), measurability of integrals against universally measurable kernels (Proposition 7.46), and existence of the history measures (Proposition 7.45), can be posed and proved as supporting lemmas; they are reusable across the book.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific, 1996, Chapter 10. https://web.mit.edu/dimitrib/www/soc.html
• K. J. Åström, Optimal control of Markov processes with incomplete state information, Journal of Mathematical Analysis and Applications 10 (1965) 174–205. https://doi.org/10.1016/0022-247X(65)90154-X
• C. Striebel, Sufficient statistics in the optimum control of stochastic systems, Journal of Mathematical Analysis and Applications 12 (1965) 576–592. https://doi.org/10.1016/0022-247X(65)90027-2
• N. Bäuerle and U. Rieder, Markov Decision Processes with Applications to Finance, Springer, 2011, Chapter 5. https://doi.org/10.1007/978-3-642-18324-9

Motivation

A single-server queue in which customers arrive according to a renewal process and are served in exponentially distributed times is the system GI/M/1. Observed just before successive arrivals, its queue length is a Markov chain on $\{0, 1, 2, \dots\}$, the imbedded chain introduced by D. G. Kendall (Kendall 1953, Ann. Math. Statist. 24, pp. 338–354). Whether this chain settles into a statistical equilibrium, keeps returning to the empty state without one, or drifts off to infinity is the first question asked about the queue, and every later quantity (stationary queue lengths, waiting-time distributions) presupposes the answer.

F. G. Foster's 1953 paper (Foster 1953) answers it for GI/M/1 and for M/G/1 by a different route from Kendall's direct analysis: it first proves general criteria, stated in terms of solutions of linear equations and inequalities in the transition matrix, for a countable Markov chain to be ergodic, recurrent or transient, and then checks them on the two queueing matrices. The criteria are of independent use; one of them (Theorem 2 of the paper) is now known as Foster's criterion, the starting point of the drift (Lyapunov-function) method for stability of Markov chains and queueing networks.

Timeline. Kendall (1951, J. Roy. Statist. Soc. B 13) studied queue-length processes directly, including a recurrence argument for M/G/1 that Foster's §3 reproduces; Kendall (1953) introduced the imbedded-chain method and, for GI/M/1, proved by it that $\rho < 1$ is sufficient for ergodicity (Foster 1953, p. 359); Foster (1953) proved the full classification, ergodic iff $\rho < 1$ and recurrent iff $\rho \le 1$, by the general criteria. This mission treats the GI/M/1 half; a companion mission treats M/G/1.

Setting

A transition matrix on the states $\{0, 1, 2, \dots\}$ is an array $[p_{ij}]$ of nonnegative reals whose rows sum to $1$. For a state $j$, $f_{jj}$ is the probability that the chain started at $j$ returns to $j$ at some later step. The chain is recurrent if $f_{jj} = 1$ for every $j$, transient if $f_{jj} < 1$ for every $j$, and ergodic (recurrent-nonnull, positive recurrent) if moreover every mean recurrence time $\sum_n n f^{(n)}_{jj}$ is finite. Foster's general theorems concern an irreducible chain (every state reachable from every state), assumed aperiodic for simplicity.

The GI/M/1 chain is described by a sequence $a = (a_n)_{n \ge 0}$ of positive numbers with $\sum_n a_n = 1$: $a_n$ is the probability that exactly $n$ services are completed between two arrivals. With the tails $\alpha_i = \sum_{j \ge i+1} a_j$,

$$[p_{ij}] = \begin{bmatrix} \alpha_0 & a_0 & 0 & 0 & \cdots \\ \alpha_1 & a_1 & a_0 & 0 & \cdots \\ \alpha_2 & a_2 & a_1 & a_0 & \cdots \\ \vdots & \vdots & \vdots & \vdots & \end{bmatrix},$$

that is $p_{i0} = \alpha_i$, $p_{ij} = a_{i+1-j}$ for $1 \le j \le i+1$, and $p_{ij} = 0$ for $j > i+1$. In Lean this matrix is gim1Matrix a. The traffic parameter $\rho$ is defined through its inverse,

$$\rho^{-1} = \sum_{n=1}^{\infty} n\, a_n \in (0, \infty],$$

the mean number of service completions per interarrival interval (rhoInv a, and rho a $= \rho$).

Formalization targets

Goal: the classification of GI/M/1 (§4, p. 359)

$$\text{the chain is ergodic} \iff \rho < 1, \qquad \text{the chain is recurrent} \iff \rho \le 1 .$$

Together: ergodic for $\rho < 1$, recurrent-null for $\rho = 1$, transient for $\rho > 1$. The statement carries no constants and leaves the sequence $a$ free apart from positivity and normalization.

Milestones

1. Theorem 7 (p. 358): for a probability distribution $\{p_n\}$ with $p_0 > 0$, the equation $\sum_{n \ge 0} z^n p_n = z$ has a root in $(0, 1)$ iff $\sum_{n\ge1} n p_n > 1$.
2. Theorem 1, sufficiency (p. 355): a nonnull solution of $\sum_i x_i p_{ij} = x_j$ with $\sum_i |x_i| < \infty$ makes the system ergodic.
3. Theorem 1, necessity (p. 355): in an ergodic system every nonnegative solution of $\sum_i x_i p_{ij} \le x_j$ has $\sum_i x_i < \infty$.
4. Theorem 4 (pp. 356–357): the system is transient iff $\sum_j p_{ij} y_j = y_i$ ($i \ne 0$) has a bounded nonconstant solution.

Milestones 2–4 are stated for a general irreducible aperiodic chain.

Significance

The classification tells exactly when the GI/M/1 queue is stable: the stationary distribution of the imbedded chain, which is geometric, exists precisely in the ergodic case $\rho < 1$, and for $\rho > 1$ the queue grows without bound. Theorems 1 and 4 are general tools, reusable for any countable chain: Theorem 1 characterizes ergodicity by summable invariant vectors, Theorem 4 characterizes transience by bounded harmonic functions off one state. Theorem 7 is the extinction criterion of branching processes and recurs throughout applied probability.

All of these results are proved in the literature (Foster 1953; Feller's textbook for Theorem 7 and a version of Theorem 4). As far as a search of the platform shows, none of them has a machine-checked proof; the platform holds related special cases for the G/M/1 queue with a specific interarrival law (QueueingFundamentals.GM1.unique_root_unit_interval, open), but not the general lemma or the classification. A formalization would provide the general criteria as reusable library results and the first verified stability classification of a non-Markovian queue's imbedded chain.

Difficulty

The matrix is explicit, but none of the three properties is a finite computation: ergodicity and recurrence are statements about return times over all horizons, so each direction must go through an existence or nonexistence statement about infinite systems of equations. For the converse directions the obvious argument fails: exhibiting a candidate solution such as $x_i \equiv 1$ shows nothing until it is known that ergodicity forces every such solution to be summable, and showing that no bounded nonconstant solution of (7) exists when $\rho < 1$ requires control of all solutions, not of one. The general criteria themselves rest on limit theorems for $p_{ij}^{(n)}$ and on interchanging infinite sums, and the infinite-mean case $\sum n a_n = \infty$ has to be carried along everywhere.

Formalization scope

• The Markov-chain vocabulary is the published definition QueueingFundamentals_Foundations_MarkovChain: TransitionMatrix (entries p, nonnegativity, rows summing to $1$ via HasSum), returnProb, meanRecurrenceTime, Irreducible, Aperiodic, PositiveRecurrent. "Ergodic" is PositiveRecurrent. IsRecurrent and IsTransient are defined state by state from returnProb; their complementarity for irreducible chains is a theorem, not a definition.
• States are indexed from $0$, as in the paper. The goal quantifies over every TransitionMatrix whose entries equal gim1Matrix a; such a matrix exists for every admissible $a$ (rows sum to $1$), so the statement is not vacuous.
• $\rho^{-1}$ and $\rho$ live in $[0, \infty]$ (ℝ≥0∞), with $\infty^{-1} = 0$: an infinite mean gives $\rho = 0$, and that chain is ergodic.
• The goal does not assume irreducibility or aperiodicity: they follow from $a_n > 0$. Milestones 2–4 carry them, as the paper's standing assumptions (§1).
• Every infinite series appearing in a hypothesis is required to converge (HasSum or Summable), so that a divergent series cannot satisfy an equation or inequality vacuously. In Theorem 1's sufficiency half the $x_i$ may be of either sign. In Theorem 7 the distribution is renamed $q$ to avoid a clash with $p_{ij}$.
• Ruled out as trivializing: defining $\rho$ by a real inverse of a real series, defining "ergodic" as the existence of a summable invariant vector (which is Theorem 1's condition), or stating the goal over a matrix that need not exist.
• Not included: the paper's explicit description of the solutions of (7) for $\rho \ge 1$ via the generating function $(1 - z)\{A(z) - z\}^{-1}$, and the M/G/1 half (Theorems 2, 3, 5), which is the companion mission. Contributions welcome: proofs of the general criteria (reusable for any countable chain), of Theorem 7, and lemmas on the GI/M/1 matrix such as irreducibility and aperiodicity.

Selected references

• F. G. Foster, On the stochastic matrices associated with certain queuing processes, Ann. Math. Statist. 24 (1953), 355–360. https://doi.org/10.1214/aoms/1177728976
• D. G. Kendall, Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain, Ann. Math. Statist. 24 (1953), 338–354 (the paper immediately preceding Foster's in the same issue).
• D. G. Kendall, Some problems in the theory of queues, J. Roy. Statist. Soc. B 13 (1951), 151–185.
• W. Feller, An Introduction to Probability Theory and Its Applications, Vol. 1, Wiley, 1950.

Motivation

The conditional logit model is the workhorse of discrete choice analysis in transportation, marketing, labour and industrial organization. McFadden's 1974 chapter derived it from a theory of population choice behaviour and showed how to estimate it by maximum likelihood; this line of work was recognized by his 2000 Nobel Prize in Economic Sciences, awarded for theory and methods of discrete choice analysis. Every applied logit estimation rests on a basic question: does the maximum likelihood estimate exist for the sample at hand? In small samples it may not. When one alternative is always chosen whenever it is available, the likelihood keeps increasing as a parameter tends to infinity, and numerical optimizers report diverging coefficients. This failure is known in the binary case as complete or quasi-complete separation. McFadden's Lemma 3 gives the exact condition, for the multinomial conditional logit model with general alternative sets, under which a maximizer exists.

Timeline. Berkson (1951, 1955) popularized binomial logit; multinomial versions were developed by Gurland (1960), Bloch (1967), Rassam (1971), McFadden (1968) and Theil (1969, 1970). McFadden (1974) stated the existence criterion for the conditional logit likelihood (Lemma 3) together with a quadratic-programming test for it (Lemma 4). Albert and Anderson (1984) later classified separation patterns for binary and multinomial logistic regression, and Haberman (1974) treated existence for log-linear models.

Setting

A choice experiment has $N \ge 1$ trials. Trial $n$ offers an alternative set of $J_n$ alternatives, indexed $i = 1,\dots,J_n$, each described by an attribute vector $z_{in} \in \mathbb{R}^K$ (the values of $K$ specified functions of the individual's and the alternative's characteristics). Trial $n$ is repeated $R_n \ge 1$ times, and alternative $i$ is chosen $S_{in}$ times, so $R_n = \sum_{j} S_{jn}$.

For a parameter $\theta \in \mathbb{R}^K$, with $z_{in}\theta$ the inner product, the selection probabilities are

$$P_{in}(\theta) = \frac{e^{z_{in}\theta}}{\sum_{j=1}^{J_n} e^{z_{jn}\theta}} \qquad (16)$$

and the log-likelihood of the sample is

$$L(\theta) = C - \sum_{n=1}^N \sum_{i=1}^{J_n} S_{in} \log \sum_{j=1}^{J_n} e^{(z_{jn} - z_{in})\theta}, \qquad C = \sum_{n=1}^N \Big[\log R_n! - \sum_{j=1}^{J_n}\log S_{jn}!\Big]. \qquad (18)$$

Write $\bar z_n(\theta) = \sum_i z_{in}P_{in}(\theta)$ for the probability-weighted mean attribute vector of trial $n$.

Axiom 5 (Full Rank). The $\big(\sum_n J_n\big)\times K$ matrix with rows $z_{in} - \bar z_n$ has rank $K$.

Axiom 6. There is no nonzero $\gamma \in \mathbb{R}^K$ with $S_{in}(z_{jn} - z_{in})\gamma \le 0$ for all $i, j = 1,\dots,J_n$ and $n = 1,\dots,N$. Equivalently, no nonzero direction makes every observed choice weakly best in its alternative set.

Formalization targets

Goal: Lemma 3

Under Axiom 5,

$$\big(\exists\, \hat\theta \in \mathbb{R}^K,\ \forall \theta,\ L(\theta) \le L(\hat\theta)\big) \iff \text{Axiom 6}.$$

Milestones

1. Equation (19): the gradient $\partial L/\partial\theta = \sum_n \sum_j (S_{jn} - R_nP_{jn}) z_{jn}$.
2. Equation (20): the Hessian $\partial^2L/\partial\theta\,\partial\theta' = -\sum_n R_n \sum_j (z_{jn} - \bar z_n)'P_{jn}(z_{jn} - \bar z_n)$.
3. $L$ is concave, and every critical point is a global maximizer.
4. A Hessian that is nonsingular everywhere makes $L$ strictly concave with at most one maximizer.
5. Axiom 5 holds at $\theta$ if and only if the Hessian at $\theta$ is negative definite.
6. Necessity: under Axiom 5, a maximizer forces Axiom 6.
7. Equation (21): under Axiom 6, $b(\gamma) = \max_n \max_{i,j} S_{in}(z_{jn}-z_{in})\gamma$ has a positive lower bound $b^*$ on the unit sphere.
8. The bound $L(\theta) - C \le -b^*|\theta|$ for all $\theta$.
9. Sufficiency: Axiom 6 gives a maximizer.

Significance

Lemma 3 tells the practitioner when the conditional logit maximum likelihood estimate exists, before any numerical optimization is attempted. It is a linear-inequality condition on the data alone, so it can be checked by linear or quadratic programming (Lemma 4 of the same paper). The existence of the estimator is also the first step of McFadden's asymptotic theory: Lemma 5 shows that Axiom 6 holds with probability tending to one, and Lemma 6, consistency and asymptotic normality, concerns the estimator whose existence Lemma 3 characterizes. The concavity and Hessian formulas (19)–(20) are the basis of the Newton–Raphson computation of the estimator and of its asymptotic covariance matrix.

The result has been proved since 1974 and is classical. To our knowledge it has no machine-checked proof; Mathlib has no statement about the existence of logit or softmax-regression maximum likelihood estimates. Formalizing it produces a verified existence criterion for the multinomial logit likelihood, verified gradient and Hessian formulas for log-sum-exp likelihoods with repeated observations, and a verified link between full column rank and strict concavity.

Difficulty

The likelihood is concave, and concave functions on $\mathbb{R}^K$ need not attain their supremum. Concavity alone therefore gives nothing, and existence must come from a growth condition. The obvious approach, "the likelihood is bounded above by $C$, hence attains its maximum", fails: $L$ is bounded but can approach its supremum only at infinity, which is exactly the separation case. Sufficiency needs a quantitative rate at which $L$ decreases, uniform over all directions; a direction-by-direction argument does not suffice. Necessity requires strict concavity, which is where Axiom 5 and the requirement that every trial be observed enter. A trial with $R_n = 0$ can supply the rank of Axiom 5 while contributing nothing to $L$, so with such a trial necessity fails. The calculus part, (19)–(20), involves differentiating sums of log-sum-exp terms over dependent index types and identifying the result with a weighted covariance operator.

Formalization scope

• Representation. $\mathbb{R}^K$ is EuclideanSpace ℝ (Fin K), so $|\theta| = (\theta'\theta)^{1/2}$ is the Euclidean norm and $z\theta$ is the inner product ⟪z, θ⟫. Trials are Fin N, alternatives of trial $n$ are Fin (J n), and the counts $S_{in}$ are natural numbers.
• Data structure. The structure Data K bundles $N$, $J$, $z$, $S$ and the standing assumptions $N \ge 1$ and $R_n = \sum_i S_{in} \ge 1$ for every trial; these make the trial and alternative index sets nonempty.
• Axioms 1–4 are built in. The model is the logit form (16) with $v$ linear in $\theta$ (Axiom 4), so "Suppose Axioms 1–5 hold" becomes "Data plus Axiom 5".
• Axiom 5 is read at every $\theta$. The row space of the matrix does not depend on $\theta$.
• Hessian. The Hessian is the Fréchet derivative of the gradient vector field (19), as a continuous linear map.
• The maximizer is global over all of $\mathbb{R}^K$. Neither a local maximizer nor "$L(\hat\theta) \ge L(0)$" is acceptable as the goal; that would make it trivial.
• Infrastructure. Gradients and Hessians of log-sum-exp with dependent finite index types; positive definiteness from full column rank; attainment of the maximum of a coercive continuous function on a finite-dimensional space. The calculus lemmas are reusable for any multinomial logit or softmax likelihood. Missions 4 and 5 of this series reuse the same model. Contributions of general log-sum-exp lemmas, independent of this mission's definitions, are welcome.

Selected references

• D. McFadden, Conditional logit analysis of qualitative choice behavior, in P. Zarembka (ed.), Frontiers in Econometrics, Academic Press, New York, 1974, pp. 105–142. https://eml.berkeley.edu/reprints/mcfadden/zarembka.pdf
• A. Albert and J. A. Anderson, On the existence of maximum likelihood estimates in logistic regression models, Biometrika 71(1), 1984, pp. 1–10. https://doi.org/10.1093/biomet/71.1.1
• S. J. Haberman, The Analysis of Frequency Data, University of Chicago Press, 1974.
• J. Berkson, Maximum likelihood and minimum χ² estimates of the logistic function, Journal of the American Statistical Association 50, 1955, pp. 130–162. https://doi.org/10.1080/01621459.1955.10501255

Motivation

Infinite horizon dynamic programming asks for the least expected cost of controlling a stochastic system forever, and for a policy attaining it. On finite or countable state spaces the theory has been classical since Bellman, Blackwell (1965) and Strauch (1966). Many models in operations research, inventory control, queueing and economics have continuous states and controls, however, and there the Bellman equation raises a question the countable theory never meets: the optimal cost need not be Borel-measurable, so its expectation under the transition law, which the equation requires, may not be defined.

Bertsekas and Shreve (1978) settled this question by working with lower semianalytic cost functions and universally measurable policies. In that framework the optimal cost is always measurable enough to be integrated, and the optimality equation holds with no continuity or compactness assumption. Chapter 9 of their book treats the infinite horizon model under the three classical cost structures: nonnegative costs (P), nonpositive costs (N), and bounded discounted costs (D).

Timeline:

• 1965: Blackwell, discounted dynamic programming on Borel spaces with Borel-measurable data, case (D).
• 1966: Strauch, negative dynamic programming, case (N), with Borel-measurable data.
• 1978: Bertsekas and Shreve, Chapter 9: lower semianalytic costs and universally measurable policies, in all three cases (P), (N), (D).
• 1979: Shreve and Bertsekas, the journal account of universally measurable policies.

Setting

An infinite horizon stochastic optimal control model (SM) is an eight-tuple $(S, C, U, W, p, f, \alpha, g)$. The state space $S$, the control space $C$ and the disturbance space $W$ are nonempty Borel spaces, that is, spaces homeomorphic to Borel subsets of complete separable metric spaces. The control constraint $U$ assigns to each state $x$ a nonempty set $U(x) \subseteq C$, and the set $\Gamma = \{(x,u) \mid u \in U(x)\}$ is analytic. The disturbance kernel $p(dw \mid x, u)$ is a Borel stochastic kernel and the system function $f : SCW \to S$ is Borel. The discount factor is $\alpha > 0$, and the one-stage cost $g : \Gamma \to [-\infty, \infty]$ is lower semianalytic: each sublevel set $\{g < c\}$ is analytic. The state moves by $x_{k+1} = f(x_k, u_k, w_k)$, with transition kernel $t(B \mid x, u) = p(\{w \mid f(x,u,w) \in B\} \mid x, u)$.

A policy $\pi = (\mu_0, \mu_1, \dots)$ chooses $u_k$ at random from a universally measurable stochastic kernel $\mu_k(du_k \mid x_0, u_0, \dots, x_k)$ concentrated on $U(x_k)$; $\Pi'$ is the set of all policies. A policy is Markov if each $\mu_k$ depends only on $x_k$, and it is stationary if, moreover, $\mu_k = \mu$ for all $k$. Writing $q_k(\pi, p_x)$ for the law of $(x_k, u_k)$ started from $x_0 = x$, the cost of $\pi$ and the optimal cost are

$$J_\pi(x) = \sum_{k=0}^\infty \alpha^k \int g\, dq_k(\pi, p_x), \qquad J^*(x) = \inf_{\pi \in \Pi'} J_\pi(x).$$

For $J : S \to [-\infty, \infty]$, the dynamic programming operators are

$$T(J)(x) = \inf_{u \in U(x)} \Big\{ g(x,u) + \alpha \int_S J(x')\, t(dx' \mid x, u) \Big\}, \qquad T_\mu(J)(x) = \int_C \Big[ g(x,u) + \alpha \int_S J\, dt \Big] \mu(du \mid x).$$

The three cases are (P) $g \ge 0$ on $\Gamma$; (N) $g \le 0$ on $\Gamma$; (D) $\alpha < 1$ and $|g| \le b$ on $\Gamma$ for some real $b$.

Formalization targets

Goal: the optimality equation (Proposition 9.8, Eq. (22))

Under each of (P), (N) and (D),

$$J^* = T(J^*).$$

Milestones

• $J^*$ is lower semianalytic (Corollary 9.4.1).
• For a stationary policy, $J_\mu = T_\mu(J_\mu)$ (Proposition 9.9).
• Optimality tests for stationary policies: under (P) or (D), $(\mu, \mu, \dots)$ is optimal iff $J^* = T_\mu(J^*)$ (Proposition 9.12); under (N) or (D), iff $J_\mu = T(J_\mu)$ (Proposition 9.13).
• Under (N) or (D), value iteration from $0$ converges to $J^*$, and under (D) it converges uniformly from every bounded lower semianalytic start (Proposition 9.14).

Further statements of the mission

• Markov policies suffice: at each state some Markov policy matches any policy's cost (Proposition 9.1), so $J^* = \inf_{\pi \in \Pi} J_\pi$ (Corollary 9.1.1).
• Partial converses of the optimality equation: $J \ge T(J)$, $J \ge 0$ gives $J \ge J^*$ under (P); $J \le T(J)$, $J \le 0$ gives $J \le J^*$ under (N); a bounded solution of $J = T(J)$ equals $J^*$ under (D) (Proposition 9.10). The analogous statements for $T_\mu$ and $J_\mu$ (Proposition 9.11).

Significance

The optimality equation is the basic structural fact of infinite horizon control. Corollary 9.12.1 uses it to construct optimal stationary policies from minimizers in the equation. The existence results for $\varepsilon$-optimal policies (Propositions 9.19 and 9.20), the convergence analysis of value iteration in Section 9.5, and the reduction of imperfect state information problems in Chapter 10 all build on it. It holds for arbitrary Borel models, with no continuity or compactness assumption.

All results of the mission were proved in 1978. None of them has a machine-checked proof: Mathlib has stochastic kernels and the Ionescu-Tulcea construction for measurable kernels, but no theory of lower semianalytic functions, universally measurable kernels, or dynamic programming on Borel spaces. A formal development would fix the measurability bookkeeping on which the textbook proofs rest and supply a reusable substrate for the stochastic control papers that cite this book.

Difficulty

Under (D), $T$ is a contraction on bounded functions, and its fixed point is the limit of value iteration. That argument, however, gives a fixed point only within a fixed class of measurable functions. Showing that this fixed point equals $J^*$ requires knowing that $J^*$ belongs to the class and that history-dependent randomized policies do no better. Under (P), value iteration can converge to the wrong limit (Example 1 of the chapter: $\lim_k J_k(0) = 0$ while $J^*(0) = \infty$). Even when each $J_k$ is Borel, $J^*$ may fail to be (Example 2). So $J^* = T(J^*)$ cannot be obtained as a limit of the finite horizon equations, and the natural class of Borel functions is not closed under the partial minimization that defines $T$.

The book's route lifts (SM) to a deterministic model on the space of probability measures $P(S)$, where no measurability restriction is needed, and transfers the results back. Making this transfer rigorous requires that the cost of a randomized policy be a measurable functional of its law, and that the infimum over policies preserve lower semianalyticity.

Formalization scope

The draft fixes the following conventions.

• Spaces. Borel spaces are topological spaces homeomorphic to Borel subsets of complete separable metric spaces, carrying their Borel $\sigma$-algebras. Analytic sets are Mathlib's AnalyticSet. A set is universally measurable if it is null-measurable for every probability measure.
• Extended reals. Values lie in EReal. The book's convention $\infty - \infty = -\infty + \infty = \infty$ is implemented explicitly, because Mathlib's EReal sets $\bot + \top = \bot$. The integral of an extended-real function is $\int f^+ - \int f^-$ with the same convention.
• Policies. These are sequences of universally measurable stochastic kernels on the history spaces $S_0C_0 \cdots S_k$, charging $U(x_k)$ with mass one. The laws of $(x_0, u_0, \dots, x_k, u_k)$ are built recursively from the kernels.
• Costs. $J_\pi$ is the series $\sum_k \alpha^k \int g\, dq_k$, computed as the difference of the series of positive and negative parts. Under each of (P), (N), (D) it coincides with the integral of the total discounted cost. $J^*$ is the infimum over all policies.
• Case labels. Each statement carries the case labels the book attaches to it, as hypotheses on the model.
• Scope. Only the (SM) statements are formalized. The deterministic model (DM) on $P(S)$ is the book's proof device and enters no statement.

The goal admits a trivializing formalization that this draft rules out. $J^*$ is not defined as a fixed point of $T$, nor as the limit of $T^k(0)$; it is the infimum of the costs of all policies, which under (P) can differ from that limit.

A complete development needs universally measurable kernels and their compositions on product spaces, measurability of $x \mapsto \int f(x, y)\, q(dy \mid x)$ for universally measurable integrands, the measurable selection theorem of Jankov and von Neumann, and the closure of lower semianalytic functions under partial infimum. These are the subject of the series' mission on Chapter 7, and they are reusable for any stochastic control model on Borel spaces. Contributions are welcome at any level: these foundations, the Markov reduction (Proposition 9.1), or the case-by-case arguments.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press, 1978; Athena Scientific reprint, 1996. Chapter 9. https://web.mit.edu/dimitrib/www/soc.html
• D. Blackwell, Discounted dynamic programming, Annals of Mathematical Statistics 36 (1965), 226–235. https://doi.org/10.1214/aoms/1177700285
• R. E. Strauch, Negative dynamic programming, Annals of Mathematical Statistics 37 (1966), 871–890. https://doi.org/10.1214/aoms/1177699369
• S. E. Shreve and D. P. Bertsekas, Universally measurable policies in dynamic programming, Mathematics of Operations Research 4 (1979), 15–30. https://doi.org/10.1287/moor.4.1.15