Optimization

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 choosing which products to display, or an airline choosing which fare classes to open, solves an assortment optimization problem: pick the set of offered products that maximizes expected revenue when customers choose among what is offered according to a discrete choice model. Under the multinomial logit model the answer has a simple form: an optimal assortment consists of the few highest-revenue products (Talluri and van Ryzin, 2004). The multinomial logit model, however, forces every pair of products to compete in the same way. The nested logit model relaxes this by grouping products into nests (brands, store sections, departure times) and letting a customer first choose a nest and then a product inside it.

Davis, Gallego and Topaloglu (Operations Research, 2014; DOI 10.1287/opre.2014.1256) study how much of the multinomial logit structure survives under the nested logit model. Their first answer is the theorem this mission targets: when the nest dissimilarity parameters are at most one and no customer who chose a nest leaves it without buying, offering the top products of each nest is still optimal. The other missions of this series treat the cases where this fails: dissimilarity parameters above one (the problem becomes NP-hard) and nests with their own no-purchase option.

Setting

There are $m$ nests $M = \{1, \dots, 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$; products are ordered so that $r_{i1} \ge r_{i2} \ge \dots \ge r_{in}$. Nest $i$ carries a dissimilarity parameter $\gamma_i > 0$ and a within-nest no-purchase weight $v_{i0} \ge 0$, and $v_0 \ge 0$ is the weight of choosing no nest at all.

An assortment is a tuple $(S_1, \dots, S_m)$ of subsets $S_i \subseteq N$. 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, inside the nest, product $j$ with probability $v_{ij}/V_i(S_i)$. The expected revenue is

$$\Pi(S_1, \dots, S_m) = \sum_{i \in M} Q_i\, R_i(S_i) = \frac{\sum_{i \in M} V_i(S_i)^{\gamma_i} R_i(S_i)}{v_0 + \sum_{i \in M} V_i(S_i)^{\gamma_i}},$$

and problem (2) asks for $Z^* = \max \Pi(S_1, \dots, S_m)$ over all assortments. The nested-by-revenue assortment $N_{ij} = \{1, \dots, j\}$ collects the $j$ highest-revenue products of nest $i$, with $N_{i0} = \emptyset$ and $N_+ = \{0, 1, \dots, n\}$.

This mission works under the standing assumptions of §3 of the paper: competitive products, $\gamma_i \le 1$, and fully-captured nests, $v_{i0} = 0$, for every nest $i$.

Formalization targets

Goal: Theorem 4 (p. 15)

If $\gamma_i \le 1$ and $v_{i0} = 0$ for all $i \in M$, there exists an optimal solution $(S^*_1, \dots, S^*_m)$ of problem (2) such that

$$S^*_i = N_{ij} \ \text{ for some } j \in N_+, \qquad \text{for all } i \in M.$$

Milestones

1. The case $v_0 = 0$ (p. 14). Offering only the single product with the largest revenue $\max_{i} r_{i1}$ is optimal.
2. Proposition 2 (p. 14). If $S^*$ is optimal and $S^*_i \ne \emptyset$, then $R_i(S^*_i) \ge Z^*$.
3. Lemma 3 (p. 14). If $Z = \Pi(S)$, $R_i(S_i) \ge Z$ and some $j \in S_i$ has $r_{ij} < \gamma_i Z + (1-\gamma_i) R_i(S_i)$, removing $j$ strictly increases the expected revenue.
4. $g(\alpha) \le \gamma$ (p. 15). For $0 < \gamma \le 1$ and $0 < \alpha < 1$: $(1 - \alpha^{\gamma})/(\alpha^{\gamma-1} - \alpha^{\gamma}) \le \gamma$.
5. Revenue threshold (p. 15). Every $j \in S^*_i$ of an optimal $S^*$ has $r_{ij} \ge \gamma_i Z^* + (1-\gamma_i) R_i(S^*_i)$.
6. $h(\alpha) \ge \gamma$ (p. 16). For $0 < \gamma \le 1$ and $0 < \alpha < 1$: $(1 - \alpha^{\gamma})/(1 - \alpha) \ge \gamma$.
7. Exchange step (p. 15). If $S^*$ is optimal, $j \in S^*_i$, $k \notin S^*_i$ and $k < j$, then adding $k$ to $S^*_i$ keeps the assortment optimal.

A companion item (not a milestone) states the algorithmic consequence at the end of §3: solving the linear program (4) over the candidates $\{N_{ij} : j \in N_+\}$ and choosing in each nest a maximizer of problem (5) gives an optimal solution of (2).

Significance

Theorem 4 reduces problem (2), a search over $2^{mn}$ assortments, to $(n+1)^m$ nested-by-revenue combinations, and the paper then finds the best one with a linear program with $1 + m$ variables and $1 + m(1+n)$ constraints. It marks the exact boundary of the classical multinomial logit structure inside the nested logit model: the paper's §4 shows that a single nest with $\gamma_i > 1$ already breaks it, and that the general problem is NP-hard. The structural statement is also the base case for the approximation guarantees of §§5–6, which compare against nested-by-revenue assortments.

The theorem is proved in the paper; to our knowledge it has no machine-checked proof. A formal proof would supply a verified reduction from a combinatorial revenue maximization over the nested logit model to a polynomial-size search, with every boundary case (empty nests, $v_0 = 0$, ties in revenues) handled explicitly.

Difficulty

The obvious argument copies the multinomial logit proof: take an optimal assortment and swap a low-revenue product for a missing higher-revenue one. Under the nested logit model this exchange changes the nest's attraction $V_i(S_i)^{\gamma_i}$ non-linearly, so the revenue of the modified assortment is not an affine function of the change, and a simple swap can lower the expected revenue. The argument must instead control how adding or removing one product moves the nest weight relative to the nest revenue, and this is exactly where $\gamma_i \le 1$ enters, through two scalar inequalities in the ratio $\alpha$ of nest weights. With $\gamma_i > 1$ these inequalities fail and so does the theorem.

A second subtlety is ties: several optimal assortments may exist, and only some of them are nested by revenue. The statement asserts existence, not that every optimum has this form.

Formalization scope

All statements live in the namespace NestedLogitVariants.Competitive and share one definition file. Nests form a finite type ι with decidable equality; products are Fin n, indexed $0, \dots, n-1$, so $N_{ij}$ is nbr n j $= \{k : k < j\}$ with $j \le n$, and $j = 0$ gives $\emptyset$. Powers are Real.rpow, and $x / 0 = 0$, which gives $R_i(\emptyset) = 0$. Optimality of an assortment means its revenue is at least that of every assortment.

Standing assumptions carried as hypotheses: $v_0 \ge 0$, $v_{i0} \ge 0$, revenues ordered within each nest, and §3's $\gamma_i \le 1$ and $v_{i0} = 0$. Three pins are disclosed: $v_{ij} > 0$ (the paper allows zero-weight padding products, under which Proposition 2 fails), $r_{ij} \ge 0$, and $\gamma_i > 0$ (the paper's $\gamma_i \ge 0$; its convention $V_i(\emptyset)^{\gamma_i} = 0$ fails at $\gamma_i = 0$). The section's "without loss of generality $v_0 > 0$" is a hypothesis of Proposition 2, Lemma 3, the threshold, the exchange step and the LP item; the goal itself only assumes $v_0 \ge 0$, and the case $v_0 = 0$ is milestone 1. The two scalar inequalities are stated as inequalities, not as monotonicity claims.

The goal is not trivialized by any hypothesis: it assumes none of the milestones, and stating "some nested-by-revenue assortment exists" (always true) or "every optimal assortment is nested by revenue" (false under ties) would be a different theorem.

Needed infrastructure is light: finite sums, real powers, and concavity of $x \mapsto x^{\gamma}$ for $\gamma \le 1$. The scalar lemmas are reusable for other nested logit results. Proofs of any milestone are welcome independently.

Selected references

• J. M. Davis, G. Gallego, H. Topaloglu, Assortment optimization under variants of the nested logit model, Operations Research 62(2), 250–273, 2014. https://doi.org/10.1287/opre.2014.1256 (cited from the authors' revised manuscript of June 18, 2013)
• K. Talluri, G. van Ryzin, Revenue management under a general discrete choice model of consumer behavior, Management Science 50(1), 15–33, 2004. https://doi.org/10.1287/mnsc.1030.0147
• D. McFadden, Modelling the choice of residential location, in A. Karlqvist et al. (eds.), Spatial Interaction Theory and Planning Models, North-Holland, 75–96, 1978.

Motivation

Chapter 4 of F. P. Kelly's Reversibility and Stochastic Networks (Wiley, 1979) applies the product-form theory of Chapter 3 to concrete systems. Two of its results have numbered statements, and they answer two practical questions.

The first comes from the design of store-and-forward communication networks (telegraph and packet-switched data networks). Messages queue at channels; the designer chooses each channel's capacity subject to a budget, and wants to minimize the delay messages suffer. Because the equilibrium law at every channel is geometric under several different modelling assumptions (§4.1, pp. 95–96), the mean delay has a closed form, and the budget allocation problem becomes a small convex program with an explicit solution. This square-root capacity assignment goes back to L. Kleinrock's work on communication nets (Communication Nets, McGraw-Hill, 1964) and remains the textbook example of optimal design for a network of queues.

The second comes from compartmental models in biology, birth–illness–death processes and manpower planning (§4.5, pp. 113–115). Individuals enter a system as a Poisson stream and move through it independently. Equilibrium results follow from Chapter 3; Theorem 4.2 describes the transient behaviour exactly, starting from an empty system.

Setting

Capacity allocation (§4.1). A network has $J \ge 1$ channels. Channel $j$ receives traffic at average rate $a_j > 0$ and is given capacity $\phi_j$. In equilibrium the number $n_j$ of messages at channel $j$ has the geometric law (4.1),

$$P(n_j = n) = \Big(1 - \frac{a_j}{\phi_j}\Big)\Big(\frac{a_j}{\phi_j}\Big)^n, \qquad n = 0, 1, 2, \dots,$$

which requires $\phi_j > a_j$. Its mean is $a_j/(\phi_j - a_j)$. Capacity on channel $j$ costs $f_j > 0$ per unit and the total budget is $F$, giving the cost constraint (4.2)

$$\sum_j f_j\phi_j = F.$$

The mean number of customers in the network is

$$N(\phi) = \sum_j \frac{a_j}{\phi_j - a_j},$$

and the feasible set is the set of $\phi \in \mathbb{R}^J$ with $\phi_j > a_j$ for every $j$ that satisfy (4.2). In Lean these are meanNumberInNetwork a φ and FeasibleCapacities a f F. The proof works with the Lagrangian lagrangian a f F y φ $= N(\phi) + y(\sum_j f_j\phi_j - F)$.

Compartmental model (§4.5). Individuals arrive in a Poisson stream of rate $\nu > 0$ at a system of $J$ compartments that is empty at time $0$. Let $p_j(s)$ be the probability that an individual is in compartment $j$ a time $s$ after its arrival; $p_j(s) \ge 0$ and $\sum_j p_j(s) \le 1$, since individuals may leave. Let $n_j(t)$ be the number of individuals in compartment $j$ at time $t > 0$, and

$$\alpha_j(t) = \int_0^t p_j(u)\,du.$$

In Lean the model is the predicate IsCompartmentModel P ν t p M T Loc, the counts are compartmentCount M Loc j, and $\alpha_j(t)$ is alpha p j t.

Formalization targets

Goal: Theorem 4.1 (p. 97)

If $J \ge 1$, $a_j > 0$, $f_j > 0$ and $F > \sum_k a_k f_k$, then

$$\phi^*_j = a_j + \frac{\sqrt{a_j f_j}}{\sum_k \sqrt{a_k f_k}}\cdot\frac{F - \sum_k a_k f_k}{f_j}$$

is feasible and minimizes $N$ over the feasible set, and every other feasible $\phi$ has $N(\phi) > N(\phi^*)$.

Milestones toward the goal

1. The mean of the geometric law (4.1) is $a_j/(\phi_j - a_j)$ (p. 97).
2. For $y > 0$ the Lagrangian is minimized over $\{\phi_j > a_j\}$ by $\phi_j = a_j + \sqrt{a_j/(y f_j)}$ (proof of Theorem 4.1).
3. The choice $1/\sqrt y = (F - \sum_k a_k f_k)/\sum_k\sqrt{a_k f_k}$ makes that minimizer equal to $\phi^*$ and feasible for (4.2).

Second result: Theorem 4.2 (pp. 114–115)

The proof's generating-function identity, for $z_j \in [0,1]$,

$$E\big(z_1^{n_1(t)}\cdots z_J^{n_J(t)}\big) = \prod_{j=1}^J \exp\big[-(1 - z_j)\nu\alpha_j(t)\big],$$

and the theorem itself: $n_1(t), \dots, n_J(t)$ are independent and $n_j(t)$ is Poisson with mean $\nu\alpha_j(t)$.

Significance

Theorem 4.1 is a closed-form design rule. Every channel first receives the capacity $a_j$ needed to carry its traffic; the remaining budget is shared in proportion to $\sqrt{a_j f_j}$, not to the traffic $a_j$. Sizing capacity in proportion to the load, which is the obvious rule, is therefore not optimal. The same calculation applies to any network whose stations have the geometric law (4.1), for example a manufacturing job shop (p. 97). The mean number in the network and the mean time a customer spends in it are minimized together.

Theorem 4.2 is the exact transient law of a network of infinite-server queues started empty. It holds however complicated the motion of an individual is, provided individuals move independently, and letting $t \to \infty$ it recovers the equilibrium Poisson law of §4.5.

Both results are classical and proved in the book. Neither is formalized on Prove2Me. The platform has the geometric equilibrium law of the M/M/1 queue (KellyStochasticNetworks.mm1_equilibrium) but not its mean, and no result on Poisson thinning or marking by independent random locations. The formal work for Theorem 4.1 is a strict-convexity and Lagrangian-sufficiency argument in $\mathbb{R}^J$. For Theorem 4.2 it is a Poisson marking theorem in measure-theoretic probability. Both pieces are reusable.

Difficulty

For Theorem 4.1, the book's proof sets the partial derivatives of the Lagrangian to zero. A stationary point is not a global minimizer in general, so the formal proof must show that $L$ is (strictly) convex on the open region $\phi_j > a_j$, and it must use Lagrangian sufficiency, not first-order conditions alone. The region is open and the objective is unbounded near its boundary. Feasibility of $\phi^*$ needs $F > \sum_k a_k f_k$, which the book leaves implicit.

For Theorem 4.2, the steps of the proof that read "conditional on $M$" have to be carried out with measure-theoretic independence. One step averages a product over $M$ independent uniform instants. Another sums the Poisson mixture into an exponential. The last turns a factorized generating function into mutual independence of $J$ counts with Poisson marginals. Mathlib has the Poisson distribution (ProbabilityTheory.poissonMeasure) but no marking or thinning theorem, and no uniqueness theorem for multivariate probability generating functions.

Formalization scope

Channels and compartments are indexed by Fin J; all rates, costs and capacities are real numbers.

Theorem 4.1. The statement carries the book's implicit hypotheses explicitly: $J \ge 1$, $a_j > 0$, $f_j > 0$, $F > \sum_k a_k f_k$. Stability $\phi_j > a_j$ is part of the feasible set. The conclusion is global optimality over the feasible set (IsMinOn) together with feasibility of $\phi^*$, plus strict optimality against every other feasible point. Uniqueness is a slight strengthening of the book's "the optimal allocation is", and it holds by strict convexity. A statement that $\phi^*$ satisfies (4.2), or that it is a stationary point of the Lagrangian, is not the theorem: those are one-line computations or the proof method, and the goal is stated as global optimality to rule them out.

Theorem 4.2. The model is pinned down as in the proof on p. 115:

• the number $M$ of arrivals in $(0,t)$ is Poisson with mean $\nu t$;
• an i.i.d. sequence of (arrival instant, location at time $t$) pairs is independent of $M$, and only its first $M$ entries are used;
• each instant is uniform on $(0,t)$, and an individual arriving at $u$ is in compartment $j$ at time $t$ with probability $p_j(t-u)$, or has left.

"Individuals move independently" is formalized as this conditional independence. The $p_j$ are measurable sub-probabilities, not assumed to sum to one. The conclusion is mutual independence of the $J$ counts (iIndepFun) together with the Poisson probability mass function of each. Infinite time horizons and the point-process description of the system are out of scope.

Useful contributions: a reusable Lagrangian-sufficiency lemma for separable convex objectives under one linear constraint; a Poisson marking (colouring) theorem for finitely many colours; the multivariate generating-function uniqueness lemma for $\mathbb{N}^J$-valued random vectors.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, John Wiley & Sons, 1979, Chapter 4 (§4.1, pp. 95–97; §4.5, pp. 113–115).
• L. Kleinrock, Communication Nets: Stochastic Message Flow and Delay, McGraw-Hill, 1964 (reprinted Dover, 1972).
• J. F. C. Kingman, Poisson Processes, Oxford University Press, 1993 (colouring and marking theorems).

Motivation

A supplier that sells through independent retailers usually loses part of the profit an integrated firm would earn: each retailer orders to maximize its own profit, not the channel's. Supply chain coordination asks which contracts make the decentralized choices coincide with the integrated optimum. Cachon and Lariviere study revenue-sharing contracts, under which a retailer pays a per-unit wholesale price and keeps only a fraction $\phi$ of its revenue, the rest going to the supplier. The contracts were made prominent by the video rental industry around 1998, where studios lowered tape prices in exchange for a share of rental income.

With a single retailer, revenue sharing at the wholesale price $\phi c$ coordinates the channel and splits its profit in the proportion $\phi$. This mission formalizes the extension in Section 3.2 of the paper to competing retailers: several locations whose revenues depend on each other's stock, so that one retailer's order lowers the others' revenue. Competition creates externalities the single-retailer argument does not have, and the question is whether revenue sharing still coordinates, and at what prices. Section 4.1.2 then works out a Cournot example in closed form, measuring how far the supplier's own optimal wholesale price leaves the channel from the integrated profit.

The source is the authors' working paper of June 2000; the published version (Management Science 51(1), 2005) renumbers and revises the results. The working paper numbers no theorem, so results are cited by section, displayed equation and page.

Setting

A single supplier sells one product through $n$ locations $i = 1,\dots,n$, each run by an independent retailer. A stocking profile is $\bar q = (q_1,\dots,q_n)$, and the revenue at location $i$ is $R_i(\bar q)$, which may depend on every location's quantity. The system revenue is $R(\bar q) = \sum_i R_i(\bar q)$, every unit costs the supplier $c > 0$, and the integrated system profit is

$$\Pi(\bar q) = R(\bar q) - c\sum_{i=1}^n q_i .$$

Write $R_j^i(\bar q) = \partial R_j(\bar q)/\partial q_i$: the superscript is the variable differentiated, the subscript the revenue function. The paper assumes that each $R_i$ is continuous, that $\partial^2 R_i/\partial q_i\partial q_j \le 0$ for $j \ne i$ (locations are substitutes), and that $R_i$ is unimodal in $q_i$. The system-optimal profile $\bar q^I$ has positive entries and solves the first-order system

$$R_i^i(\bar q^I) + \sum_{j\ne i} R_j^i(\bar q^I) = c, \qquad i = 1,\dots,n. \tag{6}$$

Under a revenue-sharing contract $(\phi, w_i)$ retailer $i$ earns $\pi_{r_i}(\bar q,\phi,\bar w) = \phi R_i(\bar q) - w_i q_i$ and the supplier earns $\pi_s(\bar q,\phi,\bar w) = \sum_i\big((1-\phi)R_i(\bar q) + w_i q_i\big) - c\sum_i q_i$; the wholesale-price contract is $\phi = 1$, with profits written $\pi_{r_i}(\bar q,\bar w)$ and $\pi_s(\bar q,\bar w)$. A Nash equilibrium in order quantities is a profile $\bar q \ge 0$ from which no retailer gains by changing its own quantity to any $x \ge 0$. The coordinating wholesale prices are

$$w_i^I = c - \sum_{j\ne i} R_j^i(\bar q^I).$$

The Cournot example (7) is $R_i(\bar q) = q_i\big(1 - q_i - \beta\sum_{j\ne i} q_j\big)$ with $0 \le \beta < 1$.

Formalization targets

Goal: revenue sharing supports $\bar q^I$ (Sec. 3.2, p. 14)

For $\phi\in[0,1]$ and $w_i(\phi) = \phi w_i^I$:

$$\bar q^I \text{ is a Nash equilibrium},\quad \pi_{r_i}(\bar q^I,\phi,\phi\bar w^I) = \phi\,\pi_{r_i}(\bar q^I,\bar w^I),\quad \pi_s(\bar q^I,\phi,\phi\bar w^I) = (1-\phi)\Pi(\bar q^I) + \phi\,\pi_s(\bar q^I,\bar w^I).$$

Wholesale-price contracts (Sec. 3.2, pp. 13–14)

An interior equilibrium satisfies $R_i^i(\bar q^N) = w_i$ (Eq. (8)), so marginal-cost pricing does not support $\bar q^I$ when a location imposes a negative externality; the prices $\bar w^I$ make $\bar q^I$ an equilibrium; $w_i^I \ge c$ when cross-effects are nonpositive; and $\bar w^I$ supports exactly the split $\pi_s(\bar q^I,\bar w^I) = \sum_i q_i^I\sum_{j\ne i}(-R_j^i(\bar q^I))$.

Revenue sharing (Sec. 3.2, p. 14)

An interior equilibrium satisfies $\phi R_i^i(\bar q^N) = w_i(\phi)$; the two profit identities hold for every $\phi$; and $\pi_{r_i}(\bar q^I,\bar w^I) \ge 0$.

The Cournot example (Sec. 4.1.2, pp. 19–20)

At a common price $w<1$ the unique equilibrium is $q_i^N = (1-w)/(2+\beta(n-1))$; the integrated optimum is $q_i^I = (1-c)/(2+2\beta(n-1))$; the coordinating price $w^I = c + \beta(n-1)(1-c)/(2+2\beta(n-1))$ increases in $\beta$ and $n$; the supplier's optimal price is $w^* = (1+c)/2$; and the efficiency at $w^*$ is

$$\frac{\Pi(\bar q^N(w^*))}{\Pi(\bar q^I)} = 1 - \frac{1}{(2+\beta(n-1))^2}.$$

Significance

The goal shows that the single-retailer coordination result survives competition, with one change: the coordinating price must charge each retailer for the externality it imposes on the others, so it depends on every location's revenue function, and $w^I_i$ exceeds the production cost. The supplier's profit then moves along a line between what wholesale prices alone give her and the whole system profit, which is how revenue sharing provides a profit split that linear prices cannot. The Cournot results make the comparison quantitative: when retailers compete intensely, the supplier's own optimal wholesale price already achieves most of the integrated profit, so revenue sharing, which has administrative costs, is less attractive.

No machine-checked proof of these results is known. The mission produces a reusable formal description of an $n$-player quantity game under per-retailer linear contracts, equilibrium conditions for it, and a fully worked Cournot instance, including a uniqueness claim for equilibria among all (not only symmetric) profiles.

Difficulty

The equilibrium claims are global: a retailer must not gain from any nonnegative deviation, not only from small ones. A first-order condition at $\bar q^I$ does not give this by itself. The page assumes $R_i$ unimodal in $q_i$, but unimodality does not survive subtracting the linear purchase cost, so the first-order condition is not sufficient under that assumption alone; the formalization uses concavity in the own quantity, under which it is. The participation claim $\pi_{r_i}(\bar q^I,\bar w^I) \ge 0$ is stated on the page without proof and needs a bound on the revenue of a location that stocks nothing.

In the Cournot example, uniqueness of the equilibrium must exclude asymmetric profiles and profiles where some retailers stock nothing, and the supplier's optimal price must be compared against every equilibrium at every price, including prices at which the retailers order nothing.

Formalization scope

Locations are Fin n; a profile is Fin n → ℝ; revenues are R : Fin n → (Fin n → ℝ) → ℝ, and dR i j q is $R_j^i(\bar q) = \partial R_j/\partial q_i$, given as a partial derivative at every profile with all entries positive. A deviation of retailer $i$ to $x$ is Function.update q i x, and Nash equilibria quantify over all $x \ge 0$. The standing assumptions of Section 3.2 are fields of the structure Model: $c > 0$; continuity of $R_i$ on the nonnegative orthant; the partial derivatives; $\partial^2 R_i/\partial q_i\partial q_j \le 0$, encoded as "$R_i^i$ does not increase in $q_j$"; and concavity of $R_i$ in $q_i$, which is the formalization's reading of "unimodal in $q_i$". The paper's assumption that marginal revenue eventually falls below every $\delta > 0$ is used only for existence of an equilibrium, which is not formalized, and is omitted.

Deviations from the page, each disclosed in the item concerned:

• $\bar q^I$ is taken as any positive solution of (6); its optimality for $\Pi$ is not used.
• "$\bar q^*$ is a Nash equilibrium" (p. 13) is read as $\bar q^I$.
• In $\phi(R_i(\bar q^I) - q_i^I w_i)$ (p. 14), $w_i$ is read as $w_i^I$.
• "$R_i^i(\bar q^I) > c$" needs a negative externality $\sum_{j\ne i}R_j^i(\bar q^I) < 0$, which is assumed.
• "$R_j^i(\bar q) \le 0$" is not a standing assumption, so it is a hypothesis of $w_i^I \ge c$, and strictness needs some strictly negative cross-effect.
• $\pi_{r_i}(\bar q^I,\bar w^I) \ge 0$ assumes nonnegative revenue at a location that stocks nothing.
• In the Cournot example the implicit $w < 1$ and $0 < c < 1$ are hypotheses; all retailers pay a common price; "increasing" is strict exactly where it holds ($n \ge 2$ for $\beta$, $\beta > 0$ for $n$).

A formalization that defines "the prices coordinate" as "the prices satisfy the first-order condition at $\bar q^I$" restates (6) and is ruled out: every equilibrium claim here is the game-theoretic statement about unilateral deviations. Contributions welcome: proofs of the equilibrium lemmas from concavity and the derivative, the Cournot uniqueness argument, and a general existence theorem for the quantity game.

Selected references

• G. P. Cachon, M. A. Lariviere, Supply Chain Coordination with Revenue-Sharing Contracts: Strengths and Limitations, working paper, June 2000. Published version: Management Science 51(1):30–44, 2005. https://doi.org/10.1287/mnsc.1040.0215
• D. Fudenberg, J. Tirole, Game Theory, MIT Press, 1991 (Theorem 1.2, existence of pure-strategy equilibria).
• F. Bernstein, A. Federgruen, Pricing and Replenishment Strategies in a Distribution System with Competing Retailers, Operations Research 51(3):409–426, 2003. https://doi.org/10.1287/opre.51.3.409.14957
• J. Tirole, The Theory of Industrial Organization, MIT Press, 1988.

Motivation

Many problems in optimization, image reconstruction and statistics reduce to the convex feasibility problem: given closed convex sets $A_i$, $i\in I$, find a point of their intersection $R=\bigcap_{i\in I}A_i$. A classical approach is the relaxation method: from the current point, move to the nearest point of one of the sets, and repeat. For Euclidean distance and half-spaces this is the method of Agmon and of Motzkin and Schoenberg (1954); for hyperplanes it is Kaczmarz's method.

L. M. Bregman's 1967 paper replaced the Euclidean distance by an abstract function $D(x,y)$ satisfying six conditions. The resulting D-projections include what are now called Bregman projections, and the paper is the origin of the Bregman divergence $D(x,y)=f(x)-f(y)-\langle\nabla f(y),x-y\rangle$, used today in mirror descent, entropy maximization and the theory of row-action methods (Censor and Zenios, 1997).

The paper proves convergence for two rules for choosing which set to project onto. This mission covers the second one, Theorem 2: always project onto the set that is farthest from the current point in the sense of $D$ (the "remotest-set" or maximal-distance control).

Setting

Let $X$ be a real linear topological space and $(A_i)_{i\in I}$ a family of closed convex subsets of $X$; the index set $I$ is arbitrary and may be infinite. Let $S\subseteq X$ be convex with $S\cap R\ne\emptyset$, and let $D:S\times S\to\mathbb R$ satisfy:

• (I) $D(x,y)\ge0$, with equality if and only if $x=y$;
• (II) for every $i$ and $y\in S$ there is a point $P_iy\in A_i\cap S$ minimizing $D(\cdot,y)$ over $A_i\cap S$, the D-projection of $y$ onto $A_i$;
• (III) $z\mapsto D(z,y)-D(z,P_iy)$ is convex on $A_i\cap S$;
• (IV) $D(y+tz,y)/t\to0$ as $t\to0$;
• (V) for each $z\in R\cap S$ and real $L$, the set $\{x\in S: D(z,x)\le L\}$ is compact;
• (VI) if $D(x^n,y^n)\to0$, $y^n\to y^*\in\overline S$, and $\{x^n\}$ lies in a compact set, then $x^n\to y^*$.

A relaxation sequence starts at $x^0\in S$ and sets $x^{n+1}=P_{i_n}x^n$; the sequence of indices $(i_n)$ is the control. The control is remotest-set if at every step $i_n$ realizes

$$\max_{j\in I}\ \min_{x\in A_j}D(x,x^n)=\max_{j\in I}D(P_jx^n,x^n).$$

In the Lean development these objects are DConditions A S D P (conditions I–IV and VI), CondV S D ((⋂ j, A j) ∩ S) (condition V), IsRelaxSeq S P i x (in the series' shared namespace BregmanRelax.Cyclic) and IsRemotestControl D P i x (in BregmanRelax.Remotest).

Formalization targets

Goal: Theorem 2 (p. 203)

For every remotest-set control and every relaxation sequence it generates, every limiting point is a common point:

$$x^{n_k}\to x^*\ \Longrightarrow\ x^*\in\bigcap_{i\in I}A_i .$$

Milestones

• Lemma 1 (pp. 201–202): for $z\in A_i\cap S$ and $y\in S$, $D(P_iy,y)\le D(z,y)-D(z,P_iy)$.
• Lemma 2 (p. 202), for any control: (1) the iterates lie in a compact set; (2) $\lim_n D(z,x^n)$ exists for each $z\in R\cap S$; (3) $D(x^{n+1},x^n)\to0$.

Significance

Theorem 2 is the first convergence result for greedy (most-violated-constraint) selection in projection methods with a non-Euclidean distance. Unlike the cyclic Theorem 1 of the same paper, it applies to infinite families of sets, which covers semi-infinite systems of convex inequalities. Lemma 1, the generalized Pythagorean inequality, is the basic estimate for Bregman projections and recurs throughout mirror-descent and row-action analyses; Lemma 2 records the Fejér-type monotonicity of the iterates with respect to $D$.

The results are classical and proved in the paper. To our knowledge they are not formalized in Lean or another proof assistant at this level of generality. The mission produces a machine-checked version of the abstract D-projection framework, with the conditions stated so that the Bregman divergence of §2 of the paper, and the Euclidean distance, are instances.

Difficulty

The obvious argument for Euclidean projections uses Fejér monotonicity and the fact that a bounded sequence in $\mathbb R^p$ has convergent subsequences. Here neither the triangle inequality nor symmetry of $D$ is available, and $X$ need not be normed or finite-dimensional. The remotest-set rule controls only the D-distance $D(P_jx^n,x^n)$ from the iterate to each projection, in that argument order; turning "these distances tend to zero along a subsequence" into "the limit lies in every $A_j$" requires the interplay of conditions V and VI, and it must hold uniformly over a possibly infinite index set.

Formalization scope

Conventions committed to in Lean:

• The D-projection is a fixed map $P:I\to X\to X$; condition II says $P_iy$ is a minimizer over $A_i\cap S$. The paper's misprint in II ("$\min_{z\in A_i\cap S}D(z,x)$", "$i\in T$") is read as $\min D(z,y)$, $i\in I$.
• Condition IV is assumed only as a vanishing right derivative at $y\in S$ in directions $w-y$ with $w\in S$. The paper's IV implies this, so the theorems are at least as strong as the paper's.
• "Compact" in V, VI and Lemma 2 (1) is sequential compactness (the proofs extract convergent subsequences); "the set of elements of $\{x^n\}$ is compact" means all $x^n$ lie in one sequentially compact set.
• "Limiting point" is the limit of a subsequence $x^{\varphi(k)}$ with $\varphi$ strictly increasing.
• The paper assumes that $\max_i\min_{x\in A_i}D(x,y)$ exists for each $y\in S$, so that a remotest-set control exists. The goal is stated for every control with the maximizing property, which covers every choice of maximizer; the existence assumption is therefore not a hypothesis.
• The index type is arbitrary: no finiteness is assumed. No Hausdorff assumption on $X$ is made.
• $D$ is a total function $X\to X\to\mathbb R$, but every condition and every statement only evaluates it on $S\times S$.

A trivializing formalization is ruled out: the hypotheses are jointly satisfiable with a genuine run (in $\mathbb R$ with $D(x,y)=(x-y)^2$, $A_0=[0,1]$, $A_1=[1,2]$, and $x^0=3$), checked locally without sorry, so neither the goal nor the lemmas holds vacuously.

A complete development needs subsequence extraction from sequentially compact sets, one-sided limits of difference quotients, and monotone convergence of real sequences — all available in Mathlib. The D-projection framework, Lemma 1 and Lemma 2 are shared with the cyclic-control mission of the same paper and are reusable for any Bregman-projection algorithm. Proofs of the lemmas, of Theorem 2, and of the instance showing the Euclidean distance satisfies conditions I–VI are welcome.

Selected references

• L. M. Bregman, The relaxation method of finding the common point of convex sets and its application to the solution of problems in convex programming, USSR Computational Mathematics and Mathematical Physics 7(3), 200–217, 1967. https://doi.org/10.1016/0041-5553(67)90040-7
• T. S. Motzkin and I. J. Schoenberg, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6, 393–404, 1954. https://doi.org/10.4153/CJM-1954-038-x
• S. Agmon, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6, 382–392, 1954. https://doi.org/10.4153/CJM-1954-037-2
• Y. Censor and S. A. Zenios, Parallel Optimization: Theory, Algorithms, and Applications, Oxford University Press, 1997, ISBN 978-0-19-510062-4.

Motivation

Discounted dynamic programming with bounded cost per stage is the standard setting in which infinite-horizon sequential decision problems are well posed: the optimal cost exists, satisfies Bellman's equation, and can be computed by iterating the DP operator. Shapley proved this for stochastic games in 1953 (Shapley 1953), Blackwell for discounted Markov decision processes in 1965 (Blackwell 1965), and Denardo observed in 1967 that the arguments use only two properties of the DP operator: monotonicity and contraction in the supremum norm (Denardo 1967). Bertsekas (1975, 1977) and Bertsekas and Shreve (1978) turned this observation into an abstract dynamic programming framework, in which a single mapping $H$ encodes stochastic, deterministic, minimax and multiplicative-cost problems at once (Bertsekas 1977).

Chapter 4 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case, is the contraction part of that framework. Its results are the abstract form of what every course on Markov decision processes proves for the discounted case, and they are what later work on abstract DP (Bertsekas, Abstract Dynamic Programming, 2022) and on robust and regularized MDPs builds on.

Setting

A model consists of a state space $S$, a control space $C$, a nonempty constraint set $U(x)\subseteq C$ for each $x\in S$, a mapping $H:S\times C\times F\to[-\infty,\infty]$, where $F$ is the set of functions $S\to[-\infty,\infty]$, and a function $J_0\in F$ with $J_0>-\infty$. $H$ is monotone: $J\le J'$ implies $H(x,u,J)\le H(x,u,J')$.

A selector is a function $\mu:S\to C$ with $\mu(x)\in U(x)$; $M$ is the set of selectors, and a policy is a sequence $\pi=(\mu_0,\mu_1,\dots)$ in $M$. The operators are

$$T_\mu(J)(x)=H(x,\mu(x),J),\qquad T(J)(x)=\inf_{u\in U(x)}H(x,u,J).$$

The cost of $\pi$ is $J_\pi(x)=\lim_{N\to\infty}(T_{\mu_0}\cdots T_{\mu_{N-1}})(J_0)(x)$, the optimal cost is $J^*(x)=\inf_{\pi}J_\pi(x)$, and $J_\mu$ is the cost of the stationary policy $(\mu,\mu,\dots)$.

$B$ is the Banach space of bounded real functions on $S$ with $\|J\|=\sup_x|J(x)|$. Assumption C asks for a closed set $\bar B\subseteq B$ containing $J_0$ and invariant under $T$ and every $T_\mu$; that every limit defining $J_\pi$ exist and be real; and that for some integer $m\ge1$ and scalars $0<\rho<1$, $\alpha>0$,

$$\|T_\mu(J)-T_\mu(J')\|\le\alpha\|J-J'\|\quad(J,J'\in B),\qquad \|(T_{\mu_0}\cdots T_{\mu_{m-1}})(J)-(T_{\mu_0}\cdots T_{\mu_{m-1}})(J')\|\le\rho\|J-J'\|\quad(J,J'\in\bar B).$$

Formalization targets

Goal: Proposition 4.2

Under Assumption C,

$$J^*\in\bar B,\qquad J^*=T(J^*),\qquad J'\in\bar B,\ J'=T(J')\ \Rightarrow\ J'=J^*,$$

$T(J')\le J'$ implies $J^*\le J'$ and $J'\le T(J')$ implies $J'\le J^*$ for $J'\in\bar B$; each $J_\mu$ is the unique fixed point of $T_\mu$ in $\bar B$; and for every $J\in\bar B$

$$\lim_{N\to\infty}\|T^N(J)-J^*\|=0,\qquad\lim_{N\to\infty}\|T_\mu^N(J)-J_\mu\|=0.$$

The statement carries no constants beyond those of Assumption C.

Milestones

• Fixed Point Theorem (p. 55): an $m$-step contraction of a nonempty closed subset of a Banach space has a unique fixed point, which attracts every orbit.
• Proposition 4.1 (p. 53): $J_\pi$ does not depend on the terminal function in $\bar B$; $\inf_\pi(T_{\mu_0}\cdots T_{\mu_{N-1}})(J)=T^N(J)$; $T^m$ and $T_\mu^m$ are $\rho$-contractions on $\bar B$.
• Proposition 4.3 (p. 56): $(\mu^*,\mu^*,\dots)$ is optimal iff $T_{\mu^*}(J^*)=T(J^*)$; pointwise optimal policies yield a stationary optimal one; stationary $\varepsilon$-optimal policies exist.
• Proposition 4.4 (p. 57): compactness of the sets $\{u\in U(x)\mid H[x,u,T^k(\bar J)]\le\lambda\}$ gives policies attaining the DP infimum, and their accumulation points are optimal stationary policies.
• Proposition 4.11 (p. 69): the discounted minimax model with $0\le g\le b$ and $\alpha<1$ satisfies Assumption C with $\bar B=B$, $m=1$, $\rho=\alpha$.

Further result

• Proposition 4.5 (p. 59), a draft theorem of this mission that is not a milestone: the error bound $J^*\le J_\mu\le J^*+(2\alpha\varepsilon_1+\varepsilon_2)(1+\alpha+\cdots+\alpha^{m-1})/(1-\rho)$.

Significance

Proposition 4.2 is the existence-and-uniqueness theorem for Bellman's equation in the contraction regime, together with the convergence of value iteration from an arbitrary start in $\bar B$. Propositions 4.3 to 4.5 turn it into statements about policies: when a stationary optimal policy exists, how one is found from the DP algorithm, and how much is lost when Bellman's equation is solved only approximately. Proposition 4.11 shows the assumption is met by a concrete class of problems, discounted minimax control, and so certifies that the abstract theorems are not vacuous.

The results are classical and have been proved in print since 1978; none of them is open. What this mission adds is a machine-checked version of the abstract theory itself, rather than of a single model. Mathlib has the Banach fixed point theorem for a contracting map of a complete space (ContractingWith) and a lemma for contracting iterates, but not the version on a closed subset with norm convergence of every orbit, and nothing on abstract DP. The platform has proved the finite-state discounted case for a concrete model (BertsekasDP.discounted_main_theorem); the abstract statements here cover infinite state spaces, minimax problems and $m$-step contractions, and are reused by the later missions of this series (generalized models, Chapter 6) and by papers that cite the book.

Difficulty

The first idea is to apply the contraction mapping principle to $T$ and read off $J^*$ as its fixed point. That gives a fixed point of $T$ but says nothing about $J^*$, which is defined as an infimum over all, generally nonstationary, policies of limits of compositions. The identification of the fixed point with $J^*$ is the content of the proposition, and it is where the Lipschitz condition (2) on all of $B$, not only on $\bar B$, enters.

Two further features block a direct appeal to Mathlib. The contraction is only $m$-step, so neither $T$ nor $T_\mu$ need be a contraction. And $H$ takes extended-real values, so every passage between $F$ and the Banach space $B$ must be justified by the invariance of $\bar B$.

Formalization scope

The state and control spaces are arbitrary types. $F$ is S → EReal; $B$ is Mathlib's lp (fun _ : S => ℝ) ⊤, whose norm is the supremum norm, and toF embeds $B$ into $F$. $\bar B$ is an arbitrary closed subset of $B$, not $B$ itself, and uniqueness of fixed points is asserted within $\bar B$. Policies are sequences ℕ → M; $(T_{\mu_0}\cdots T_{\mu_{N-1}})(J)$ applies $T_{\mu_{N-1}}$ first. $J_\pi$ is the pointwise limit (limUnder), which exists and is real under Assumption C; $J^*$ is the infimum over all policies.

The book computes in $[-\infty,\infty]$ with $\infty-\infty=\infty$, whereas Mathlib's EReal has $\bot+\top=\bot$. No statement adds infinities of opposite sign. A norm bound $\|J-J'\|\le c$ between functions of $F$ is the predicate SupDistLe: both functions are real at every point and differ by at most $c$, which is what the bound means under the book's arithmetic. Condition (2) is imposed on all of $B$, as on p. 53. The scalars $m,\rho,\alpha$ of Assumption C are explicit parameters, so the constant of Proposition 4.5 is the book's exact expression. The Fixed Point Theorem assumes $\bar B$ nonempty, which the page leaves implicit and without which the statement is false.

Defining $J^*$ as the fixed point of $T$, or replacing it by the infimum over stationary policies, would make the goal trivial. Neither is done here: $J^*$ is the infimum of the policy costs, exactly as in Eq. (8) of Chapter 2.

A complete development needs the $m$-step fixed point theorem on closed subsets of a Banach space, which can be reused well beyond dynamic programming; the elementary calculus of SupDistLe and of the embedding of $B$ into S → EReal; and the monotone-operator inequalities of Section 2.1. Contributions of any of these, or alternative proofs of the milestones, are welcome.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press 1978; Athena Scientific reprint 1996, Chapter 4. http://web.mit.edu/dimitrib/www/soc.html
• D. P. Bertsekas, Monotone mappings with application in dynamic programming, SIAM J. Control Optim. 15 (1977) 438–464. https://doi.org/10.1137/0315031
• E. V. Denardo, Contraction mappings in the theory underlying dynamic programming, SIAM Review 9 (1967) 165–177. https://doi.org/10.1137/1009030
• D. Blackwell, Discounted dynamic programming, Ann. Math. Statist. 36 (1965) 226–235. https://doi.org/10.1214/aoms/1177700285
• L. S. Shapley, Stochastic games, Proc. Natl. Acad. Sci. USA 39 (1953) 1095–1100. https://doi.org/10.1073/pnas.39.10.1095
• D. P. Bertsekas, Abstract Dynamic Programming, 3rd ed., Athena Scientific 2022. https://web.mit.edu/dimitrib/www/abstractdp_MIT.html