Operations Research

Why symmetric queues

The classical product-form results for queueing networks (Jackson, Kelly, Baskett–Chandy–Muntz–Palacios) assume exponentially distributed service requirements, because then the state of a queue need not record how much service each customer has received. Real service times are rarely exponential: telephone call lengths, job sizes in time-shared computers and web transfers are far from it. Symmetric queues, introduced in §3.3 of F. P. Kelly, Reversibility and Stochastic Networks (Wiley, 1979), form the class of single queues for which the stationary distribution of the number of customers, and of their classes, depends on the service requirement distribution only through its mean. This property, insensitivity, is what makes Erlang's loss formula valid for arbitrarily distributed call lengths (Kelly, p. 79), and it is the reason processor-sharing, last-come-first-served preemptive and infinite-server stations may appear with general service in product-form networks.

Timeline. Sevastyanov (1957) proved that Erlang's loss formula holds for arbitrarily distributed call lengths. Kelly (1975, 1976) introduced queues with customers of different types whose effort and arrival-position functions coincide, and showed product form for networks of them with non-exponential service built from exponential stages; Barbour (1976) extended the method of stages; Baskett, Chandy, Muntz and Palacios (1975) gave product form for networks containing processor-sharing, LCFS-preemptive and infinite-server stations with phase-type service. Kelly's 1979 book presents the symmetric queue in the form formalized here.

Setting

A symmetric queue holds customers in positions $1, 2, \dots, n$, where $n$ is the number present. It operates as follows (Kelly, p. 72):

1. the service requirement of a customer is a random variable whose distribution may depend on the class of the customer;
2. a total service effort is supplied at rate $\phi(n)$, with $\phi(n) > 0$ for $n > 0$;
3. a proportion $\gamma(l, n)$ of this effort, $\sum_{l=1}^n \gamma(l, n) = 1$, goes to the customer in position $l$; when he leaves, the customers in positions $l+1, \dots, n$ move down by one;
4. an arriving customer moves into position $l \in \{1, \dots, n+1\}$ with probability $\gamma(l, n+1)$ — the same function — and the customers in positions $l, \dots, n$ move up by one.

Server-sharing ($\gamma(l, n) = 1/n$), the stack ($\gamma(n, n) = 1$, last come first served preemptive), the queue with no waiting room and the infinite-server queue are examples (pp. 73–74).

Customers of class $c$ arrive in a Poisson stream of rate $\nu(c)$. On arrival a class-$c$ customer receives a refined class $(c, z)$ with probability $p(c, z)$, $\sum_z p(c, z) = 1$, and then needs $w(c, z) \ge 1$ independent stages of service, each exponentially distributed with mean $d(c, z) > 0$. The class-$c$ service requirement is therefore a mixture of gamma distributions with mean

$$a(c) = \sum_z p(c, z)\, w(c, z)\, d(c, z),$$

and the work arriving per unit time is $a = \sum_c \nu(c) a(c)$. The record of the customer in position $l$ is $\mathbf c(l) = (c(l), z(l), u(l))$, $u(l)$ the stage in progress, and $\mathbf c = (\mathbf c(1), \dots, \mathbf c(n))$ is a Markov process. Its transitions are: an arrival of class $(c,z)$ into position $l$ at stage $1$, at rate $\nu(c)p(c,z)\gamma(l, n+1)$; and, at rate $\phi(n)\gamma(l,n)/d(c(l),z(l))$, completion of the current stage of the customer in position $l$, which moves him to the next stage or, after stage $w(c(l), z(l))$, out of the queue. The normalizing constant is

$$b^{-1} = \sum_{n=0}^{\infty} \frac{a^n}{\prod_{l=1}^n \phi(l)}. \tag{3.15}$$

Formalization targets

Goal: Theorem 3.8

When (3.15) converges, the distribution

$$\pi(\mathbf c) = b \prod_{l=1}^n \frac{\nu(c(l))\, p(c(l), z(l))\, d(c(l), z(l))}{\phi(l)} \tag{3.18}$$

is the equilibrium distribution of $\mathbf c$, and under it

$$\mathbb P(n \text{ customers}) = \frac{b\,a^n}{\prod_{l=1}^n \phi(l)}, \qquad \mathbb P(\text{classes } c_1, \dots, c_n \mid n) = \prod_{l=1}^n \frac{\nu(c_l)\, a(c_l)}{a},$$

and the queue is quasi-reversible with respect to the classification $c$ and to $(c, z)$: from every state, the rate of arrivals of each class does not depend on the state, both for the process and its time reversal (relations (3.8) and (3.10) of p. 67).

Milestones

• Eqs. (3.14)–(3.15): the case of one refinement per class, $\pi(\mathbf c) = b\prod_l \nu(c(l))d(c(l))/\phi(l)$ with $a = \sum_c \nu(c)d(c)w(c)$.
• Eqs. (3.16)–(3.17): in that case, the law of $n$, and given $n$ independent positions of class $c$ with probability $\nu(c)d(c)w(c)/a$ and uniform stage.
• Eq. (3.18): the equilibrium distribution under gamma-mixture service.
• Lemma 3.9: mixtures of gamma distributions approximate, at continuity points, the distribution function of any positive random variable.

Significance

Theorem 3.8 gives the stationary law of a symmetric queue in closed form and shows that it depends on the service requirement distributions only through their means $a(c)$. Quasi-reversibility (part (iii)) is the property that lets symmetric queues be placed in networks: Kelly's §3.2 shows that a network of quasi-reversible queues has a product-form equilibrium, so Theorem 3.8 is the single-queue input to product-form networks with processor-sharing, LCFS-preemptive and infinite-server stations and class-dependent, non-exponential service. Lemma 3.9 is the approximation step behind the extension to arbitrary service distributions (Theorem 3.10).

These results are classical and proved in the book. To our knowledge none of them is machine-checked; Mathlib has the gamma distribution and distribution functions but no queueing theory. The mission produces a formal model of the symmetric queue as a countable-state Markov process, its equilibrium distribution, the insensitive marginals and the rate characterization of quasi-reversibility, all reusable by the chapter on networks of quasi-reversible queues.

Difficulty

The obvious first attempt, detailed balance, fails: the stage process is not reversible in general, since an intermediate stage completion has no transition back. The equilibrium equations must be verified in full, over a countable state space in which a single state is reached from infinitely many others. The symmetry condition $\gamma \equiv \delta$ is essential and must enter the argument: without it (for first-come-first-served, say) the distribution (3.18) is false for non-exponential service. Positions shift on every arrival and departure, so the bookkeeping of which list results from which event, including coincidences when neighbouring customers have identical records, is the main formal burden. The marginal computations sum (3.18) over lists of records, where convergence must be tracked, and Lemma 3.9 needs an explicit construction of approximating gamma mixtures.

Formalization scope

• The state is a List of customer records (class, refined class, stage); list index $i$ is position $l = i + 1$, and $\gamma(l, n)$, $\phi(n)$ keep the book's $1$-based indexing. The state space consists of the lists whose records have $\nu(c)p(c,z) > 0$ and $1 \le u \le w(c, z)$: records of a refined class arriving at rate zero are unreachable and excluded.
• Classes $\mathcal C$ and refinements $\mathcal Z$ are arbitrary countable types. All infinite sums are HasSum or tsum with explicit convergence hypotheses: $\sum_c \nu(c) < \infty$ (finite exit rates, the book's standing assumption of §1.1), convergence of $a(c)$, of $a$, and of (3.15). "Equilibrium distribution" means positive, summing to one, and satisfying the equilibrium equations with convergent series.
• The statement is rate level: (3.18) is shown to satisfy the equilibrium equations of the stage process, and quasi-reversibility is its rate characterization (3.8), (3.10). That these describe the stationary process and its time reversal is the book's Chapter 1 and is not reformalized.
• Trivializing readings ruled out: the goal keeps $p$, $w$ and $d$ general (not $w \equiv 1$, which would make the result Section 3.1's exponential case); the arrival position uses the same $\gamma$ as the service split; and in Lemma 3.9 the approximants must be genuine gamma mixtures with integer shapes, which a point mass is not.
• Not planned: Theorem 3.10 (arbitrary service distributions; only an outline of proof and a continuous state space the book does not construct) and Theorem 3.11 (reversibility of the number in queue, a non-Markov process).

Welcome contributions: proofs of the milestones, lemmas about List.insertIdx/List.eraseIdx bookkeeping for queues with positions, and summation over lists of records.

Selected references

• F. P. Kelly, Reversibility and Stochastic Networks, Wiley, Chichester, 1979, §3.3, pp. 72–82. https://www.statslab.cam.ac.uk/~frank/BOOKS/kelly_book.html
• F. P. Kelly, Networks of queues with customers of different types, Journal of Applied Probability 12 (1975), 542–554. https://www.jstor.org/journal/japplprob
• F. P. Kelly, Networks of queues, Advances in Applied Probability 8 (1976), 416–432. https://www.jstor.org/journal/advaapplprob
• A. D. Barbour, Networks of queues and the method of stages, Advances in Applied Probability 8 (1976), 584–591. https://www.jstor.org/journal/advaapplprob
• B. A. Sevastyanov, An ergodic theorem for Markov processes and its application to telephone systems with refusals, Theory of Probability and its Applications 2 (1957), 104–112.
• F. Baskett, K. M. Chandy, R. R. Muntz, F. G. Palacios, Open, closed, and mixed networks of queues with different classes of customers, Journal of the ACM 22 (1975), 248–260. https://doi.org/10.1145/321879.321887

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

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

Motivation

Many selection problems assign a value to each subset of a finite collection: the coverage supplied by chosen facilities, the influence reached by chosen seeds, or the value of a coalition. A submodular set function has diminishing returns in the precise sense that the combined value of two sets, counting their overlap once, does not exceed the sum of their separate values. When the function is also monotone, taking more elements never hurts. The unconstrained problem studied here permits nonmonotone functions, so both accepting and rejecting an element can matter. The question is what a single pass through the elements can guarantee when the function is available through value queries. Buchbinder et al., FOCS 2012

The randomized algorithm in this mission attains an expected one-half approximation for every nonnegative submodular function. The paper presents this as tight in the value-oracle setting: it recalls the earlier result of Feige, Mirrokni and Vondrák that a fixed improvement beyond one-half requires exponentially many queries. The contribution here is therefore both the guarantee and a short adaptive rule that attains it in a linear number of iterations. The local proposal follows the FOCS 2012 version of the paper; its theorem numbering differs from the later SIAM Journal on Computing article. Buchbinder et al., §I.A and Theorem I.2

Setting

Let $\mathcal N$ be a finite ground set, and let $f:2^{\mathcal N}\to\mathbb R_{\ge0}$ assign a nonnegative real value to every subset. The unconstrained submodular maximization problem asks for the largest value $f(S)$ among all $S\subseteq\mathcal N$. Write $OPT$ for that value when no confusion arises, and $O$ for a set attaining it. Submodularity means

$$f(A\cup B)+f(A\cap B)\le f(A)+f(B)\qquad(A,B\subseteq\mathcal N).$$

There is no monotonicity or normalization assumption: $f(\varnothing)$ and $f(\mathcal N)$ may both be positive. A value oracle returns $f(S)$ for a requested subset $S$. The paper's complexity claim counts such queries, assuming a query takes constant time. Buchbinder et al., §I and footnotes 1–2

Algorithm 2 visits the elements once in an arbitrary order $u_1,\ldots,u_n$. It keeps two sets, starting at $X_0=\varnothing$ and $Y_0=\mathcal N$. At step $i$, it measures the gain $a_i$ from adding $u_i$ to $X_{i-1}$ and the gain $b_i$ from removing $u_i$ from $Y_{i-1}$. It clips each gain at zero, giving $a'_i=\max(a_i,0)$ and $b'_i=\max(b_i,0)$. It adds $u_i$ to $X$ with probability $a'_i/(a'_i+b'_i)$ and otherwise removes it from $Y$. When both clipped gains vanish, the paper defines the add probability as one. After all elements have been processed, the two sets coincide, and the algorithm returns their common value. The state law is adaptive: its probability at step $i$ depends on the actual pair of sets produced by earlier choices. Buchbinder et al., Algorithm 2

Formalization targets

The main target is Theorem I.2 for this exact algorithm and for every enumeration of the ground set:

$$\max_{S\subseteq\mathcal N}f(S)\le 2\,\mathbb E[f(X_n)].$$

The milestone statements retain the paper's key local quantities. For a comparison optimum $O$, set $OPT_i=(O\cup X_i)\cap Y_i$. Lemma II.1 asserts $a_i+b_i\ge0$. The endpoint statement identifies $OPT_0=O$ and $OPT_n=X_n=Y_n$. Inequality (3) bounds the conditional loss in the positive-gain case; Lemma III.1 compares the expected change of $OPT_i$ with the expected combined change of $X_i$ and $Y_i$. The telescoped display keeps the initial endpoint values $f(\varnothing)$ and $f(\mathcal N)$ before using nonnegativity. Buchbinder et al., Lemmas II.1 and III.1, inequality (3), proof of Theorem I.2

A companion target is Theorem I.4 via its second proof. For two normalized monotone submodular utilities $f_1,f_2$, let $g(S)=f_1(S)+f_2(\mathcal N\setminus S)$. The maximum of $g$ is exactly the optimal welfare of a two-player partition. Algorithm 2 on $g$ is asked to satisfy

$$3\max_{S\subseteq\mathcal N}g(S)\le4\,\mathbb E[g(X_n)].$$

This is the paper's three-quarter guarantee in its welfare application. Buchbinder et al., Theorem I.4 and Proof (2)

Significance

The main theorem gives a specific randomized rule whose expected value is at least half the best subset value, even when accepting an element can lower the objective. It applies without restricting the cardinality or shape of the chosen subset. The welfare corollary shows that keeping the initial endpoint values in the analysis yields a stronger guarantee for the objective formed from two monotone players. Buchbinder et al., Theorems I.2 and I.4

This mission formalizes the statement of the algorithm, its intermediate state laws, its comparison set, and the paper's numbered proof targets. The algorithmic guarantee is proved in the source paper; the local Lean theorem files are open statements with sorry and do not yet give machine-checked proofs of these results. A completed development would supply a reusable formal model of an adaptive finite random process over pairs of subsets, as well as the specific submodular inequalities. The published Submodular and OPT definitions from the earlier Feige–Mirrokni–Vondrák formalization are reused here.

Difficulty

The two possible updates cannot be assessed independently. The probability of each choice depends on the current state, and the comparison set $OPT_i$ can gain or lose the processed element in a way that differs from the two algorithm sets. A bound on the expected value of $X_i$ alone does not control the movement of $OPT_i$. The proof must handle the clipped gains, including the case when both are zero, while preserving the exact joint law of $(X_i,Y_i)$. Buchbinder et al., proof of Lemma III.1

Formalization scope

The ground set is a finite Lean type; subsets are Finset X, and values are real numbers. An order is a list with no repeated elements that covers the type, including the empty type. The run is an explicit finite mass function on pairs of subsets after every prefix of the list. Expectation is a finite weighted sum, so it has no integrability exception. The transition clips the two real marginal gains and handles $0/0$ by assigning probability one to the add branch, exactly as Algorithm 2 specifies. The optimum is the published maximum over all subsets. No ratio divides by a possibly zero optimum.

The theorem fixes Algorithm 2 itself; an arbitrary process with nested sets or a process defined by its desired approximation property does not satisfy this scope. The Lean goal states the value bound and leaves the paper's linear-time claim outside the formal theorem. The algorithm uses four value evaluations per processed element in its printed rule; the Lean development represents those evaluations, not an implementation cost model. The statement that its two final sets coincide is a separate milestone.

The source's main-text decreasing-returns definition has an overbroad quantifier on the added element. This development uses the equivalent lattice inequality given in the paper's footnote, which permits nonmonotone functions. The proof of Lemma II.1 also has a set-index slip, and the proof of Theorem I.2 prints $F$ for $f$ in one display; neither slip is copied into a formal statement. The one-step inequality (3) is stated for any nested pair with the processed element in $Y\setminus X$, a generalization of the conditioned reachable states in the paper. Contributions proving the endpoint invariant, conditional inequality, one-step expected estimate, and final bound are all within scope.

Selected references

• Niv Buchbinder, Moran Feldman, Joseph Naor and Roy Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, Proceedings of the 53rd IEEE Symposium on Foundations of Computer Science, 2012. FOCS version used here.
• Niv Buchbinder, Moran Feldman, Joseph Naor and Roy Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM Journal on Computing 44(5), 2015. DOI: 10.1137/130929205. The cited statement indices above refer to the FOCS version.

Motivation

A stochastic approximation algorithm is a recursion

$$x_{n+1}-x_n=\gamma_{n+1}\big(F(x_n)+U_{n+1}\big)$$

in $\mathbb R^d$, where $F$ is a vector field, $\gamma_n$ are small step sizes and $U_{n+1}$ is noise. Such recursions go back to Robbins and Monro's root-finding scheme (Robbins–Monro 1951) and underlie stochastic gradient descent, temporal-difference learning, adaptive control and learning in games. The ODE method studies them by comparing the iterates with the trajectories of $\dot x=F(x)$.

Benaïm's lecture notes (Benaïm 1999) organize the ODE method in two steps. A deterministic step, Proposition 4.1, shows that whenever the noise satisfies a condition called A1 (together with a boundedness condition on the iterates), the interpolated process is an asymptotic pseudotrajectory of the flow of $F$. A probabilistic step then verifies A1 for concrete noise models. Proposition 4.2 does this for martingale difference noise with bounded $q$-th moments, at the price of step sizes with $\sum_n\gamma_n^{1+q/2}<\infty$. This mission formalizes the second verification, Proposition 4.4: when the noise is subgaussian, A1 holds almost surely under the much weaker requirement that $\sum_ne^{-c/\gamma_n}<\infty$ for every $c>0$, which allows step sizes decaying only slightly faster than $1/\log n$. The notes attribute the result to Duflo (1997), see also Kushner and Yin (1997) and Benaïm and Hirsch (1996).

Setting

Let $\{\gamma_n\}_{n\ge1}$ be a deterministic sequence with $\gamma_n\ge0$, $\sum_n\gamma_n=\infty$ and $\gamma_n\to0$ (a step sequence). Put $\tau_0=0$, $\tau_n=\sum_{i=1}^n\gamma_i$, and let

$$m(t)=\sup\{k\ge0:\ t\ge\tau_k\}$$

be the index of the step that contains time $t\ge0$. For a sequence $\{U_n\}_{n\ge1}$ define the piecewise constant processes $\bar U(t)=U_{m(t)+1}$ and $\bar\gamma(t)=\gamma_{m(t)+1}$, so that step $n+1$ occupies the time interval $[\tau_n,\tau_{n+1})$ of length $\gamma_{n+1}$.

Assumption A1 asks that for every $T>0$

$$\lim_{n\to\infty}\sup\Big\{\Big\|\sum_{i=n}^{k-1}\gamma_{i+1}U_{i+1}\Big\|:\ k=n+1,\dots,m(\tau_n+T)\Big\}=0,$$

or, in the form the notes call equivalent, $\lim_{t\to\infty}\Delta(t,T)=0$ for every $T>0$, where

$$\Delta(t,T)=\sup_{0\le h\le T}\Big\|\int_t^{t+h}\bar U(s)\,ds\Big\|.$$

Let $(\Omega,\mathcal F,P)$ be a probability space with a nondecreasing sequence $\{\mathcal F_n\}$ of sub-$\sigma$-algebras, and $F:\mathbb R^d\to\mathbb R^d$ continuous. A sequence $\{x_n\}$ given by the recursion above is a Robbins–Monro algorithm if $\gamma$ is deterministic, $U_n$ is $\mathcal F_n$-measurable, and $E(U_{n+1}\mid\mathcal F_n)=0$. The noise is subgaussian if there is a number $\Gamma>0$ such that for all $n$ and all $\theta\in\mathbb R^d$

$$E\big(\exp\langle\theta,U_{n+1}\rangle\,\big|\,\mathcal F_n\big)\le\exp\Big(\frac\Gamma2\|\theta\|^2\Big).$$

Bounded noise, $\|U_n\|\le\sqrt\Gamma$, is an example.

Formalization targets

Goal: Proposition 4.4

For a Robbins–Monro algorithm with subgaussian noise and a deterministic step sequence such that

$$\sum_ne^{-c/\gamma_n}<\infty\qquad\text{for each }c>0,$$

with probability one the realised noise sequence satisfies A1, in both of its forms, simultaneously for all $T>0$.

Milestones

1. The exponential supermartingale. For every $\theta\in\mathbb R^d$,

$$Z_n(\theta)=\exp\Big[\sum_{i=1}^n\langle\theta,\gamma_iU_i\rangle-\frac\Gamma2\sum_{i=1}^n\gamma_i^2\|\theta\|^2\Big]$$

is a supermartingale. 2. Directional maximal tail bound. For every unit vector $e$, $\alpha>0$, $n$ and $T>0$,

$$P\Big(\sup_{n<k\le m(\tau_n+T)}\Big\langle e,\sum_{i=n}^{k-1}\gamma_{i+1}U_{i+1}\Big\rangle\ge\alpha\Big)\le\exp\Big(\frac{-\alpha^2}{2\Gamma\sum_{i=n}^{m(\tau_n+T)-1}\gamma_{i+1}^2}\Big).$$

3. Eq. (18). There are $C,C'>0$ depending only on $d$ and $\Gamma$ with

$$P(\Delta(t,T)\ge\alpha)\le C\exp\Big(\frac{-\alpha^2}{C'\int_t^{t+T}\bar\gamma(s)\,ds}\Big)\qquad(t\ge0,\ T>0,\ \alpha>0).$$

4. Block comparison. $\Delta(t,T)\le2\Delta(kT,T)+\Delta((k+1)T,T)$ for $kT\le t<(k+1)T$.

Significance

Proposition 4.4 is the sufficient condition for the ODE method when the noise has Gaussian-type tails. Its step-size condition holds whenever $\gamma_n\log n\to0$, so it admits steps that decrease far more slowly than the $\sum\gamma_n^2<\infty$ of the classical $L^2$ theory; slowly decreasing steps are what practitioners use to keep algorithms responsive. Combined with Proposition 4.1 it shows that the interpolated process of such an algorithm, with bounded iterates, is almost surely an asymptotic pseudotrajectory of the flow of $F$, and the limit set theorems of the notes then locate the limit points of the algorithm.

The result is proved in the notes and in the cited literature; it has not, to our knowledge, been machine-checked. A formal proof would add reusable pieces: an exponential supermartingale and maximal inequality for vector-valued martingale differences with a conditional subgaussian bound (Mathlib's conditional subgaussian notion is scalar), a Borel–Cantelli argument along the grid $kT$, and the continuous-time bookkeeping of $\bar U$, $\bar\gamma$ and $\Delta$ shared with the other missions of this series.

Difficulty

The moment method of Proposition 4.2 does not reach this regime: any fixed polynomial moment of the window sums decays only polynomially in the window's step sizes, and under $\sum e^{-c/\gamma_n}<\infty$ alone polynomial bounds are not summable over windows. Exponential tail bounds are needed, and they must be maximal (uniform over the window) and must hold for the norm of a vector, not only for a scalar. The continuous-time deviation $\Delta(t,T)$ involves partial steps at both ends of $[t,t+h]$, so the bound must be stated in terms of $\int_t^{t+T}\bar\gamma$ rather than a sum over whole steps, with constants that do not depend on $t$, $T$ or $\alpha$. Finally, A1 quantifies over all $T>0$: the almost-sure statement must hold on a single event of full probability for every $T$.

Formalization scope

The space is $\mathbb R^d$ as EuclideanSpace ℝ (Fin d) (the paper writes $\mathbb R^m$); time is real. The sequences $\gamma$ and $U$ are indexed by $\mathbb N$, and their values at $0$ are unused, as the paper indexes them from $1$. The filtration is a Mathlib Filtration ℕ; $U_{n+1}$ is $\mathcal F_{n+1}$-strongly measurable and integrable, and $E(U_{n+1}\mid\mathcal F_n)=0$ almost surely. The subgaussian condition requires $\exp\langle\theta,U_{n+1}\rangle$ to be integrable for every $\theta$ and $n$. The summand $e^{-c/\gamma_n}$ is taken to be $0$ when $\gamma_n=0$, its limiting value. The suprema in A1 and $\Delta$ are taken in $[0,\infty]$; the supremum over an empty range of $k$ is $0$. In Eq. (18) the constants are chosen before the probability space, the algorithm and $t,T,\alpha$.

The following readings are excluded and are not acceptable formalizations: a subgaussian condition that holds vacuously because the exponential is not integrable (Lean's conditional expectation of a non-integrable function is $0$); a summability condition made trivial or false by the convention $c/0=0$; and the conclusion "for each $T$, A1 holds almost surely" in place of "almost surely, A1 holds for all $T$". The second sentence of Proposition 4.4 (the asymptotic pseudotrajectory conclusion) is outside this mission.

All hypotheses are satisfiable: $U=0$, $x=0$, $F=0$, $\Gamma=1$ and $\gamma_n=1/n$ satisfy every one of them.

Contributions welcome: a maximal inequality for nonnegative supermartingales in the form needed here, vector subgaussian tail bounds for martingale transforms with deterministic weights (reusable well beyond this mission), lemmas on the step processes and $\Delta$ (measurability, local integrability, additivity), and the proofs of the milestones.

Selected references

• M. Benaïm, Dynamics of Stochastic Approximation Algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Mathematics 1709, Springer, 1999, pp. 1–68. https://doi.org/10.1007/BFb0096509
• M. Duflo, Random Iterative Models, Applications of Mathematics 34, Springer, 1997.
• H. J. Kushner and G. G. Yin, Stochastic Approximation Algorithms and Applications, Springer, 1997.
• M. Benaïm and M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, Journal of Dynamics and Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617
• H. Robbins and S. Monro, A stochastic approximation method, Annals of Mathematical Statistics 22 (1951), 400–407. https://doi.org/10.1214/aoms/1177729586

Motivation

Dynamic programming over uncountable state and control spaces needs two things at every stage: the optimal cost-to-go, obtained by minimizing over the control, must be a function that can be integrated against the next stage's transition probabilities, and a policy that nearly attains the minimum must be measurable, so that it defines a stochastic process. With Borel-measurable costs and Borel-measurable policies both requirements fail. Minimizing a Borel function of $(x,y)$ over $y$ produces a function whose level sets are projections of Borel sets, and such projections need not be Borel (Suslin, 1917). The repair, developed by Blackwell, Freedman and Orkin (1974), Shreve and Bertsekas, and set out in Chapter 7 of Bertsekas and Shreve's Stochastic Optimal Control: The Discrete-Time Case (1978), is to enlarge the class of costs to the lower semianalytic functions and the class of policies to the analytically or universally measurable ones. Sections 7.6–7.7 of the book establish that this class is closed under partial minimization and admits measurable ε-optimal selectors. Chapters 8–10 of the book, and much of the later literature on Borel-space Markov decision processes (Hernández-Lerma and Lasserre; Feinberg and coauthors), build on these results.

Timeline:

• 1917: Suslin shows that projections of Borel sets need not be Borel and introduces analytic sets; Lusin proves that analytic sets are universally measurable.
• 1941–1949: Jankov and von Neumann independently prove that an analytic subset of a product admits a selector measurable with respect to the σ-algebra generated by analytic sets.
• 1974: Blackwell, Freedman and Orkin use analytic sets to construct ε-optimal policies in Borel dynamic programming.
• 1978: Bertsekas and Shreve give the treatment used here (§7.6–7.7), including the selection theorem for lower semianalytic functions, Proposition 7.50.

Setting

A Borel space is a topological space homeomorphic to a Borel subset of a complete separable metric space (Definition 7.7); its Borel σ-algebra is $\mathscr B_X$. The Baire space is $\mathscr N=\mathbb N^{\mathbb N}$ with the product topology. A set $A\subseteq X$ is analytic if it is empty or the image of $\mathscr N$ under a continuous map; by Proposition 7.41 this is the book's Definition 7.16 (the Suslin operation applied to closed sets). Every Borel set is analytic, and the converse fails when $X$ is uncountable.

Three σ-algebras on $X$ are in play. The analytic σ-algebra $\mathscr A_X$ is generated by the analytic sets (Definition 7.19). The universal σ-algebra is $\mathscr U_X=\bigcap_{p}\mathscr B_X(p)$, the intersection over all probability measures $p$ on $(X,\mathscr B_X)$ of the $p$-completions of $\mathscr B_X$ (Definition 7.18). For a function $f$ from $D\subseteq X$ into a Borel space $Y$, $f$ is analytically measurable if $D\in\mathscr A_X$ and $f^{-1}(B)\in\mathscr A_X$ for every $B\in\mathscr B_Y$, and universally measurable if the same holds with $\mathscr U_X$ (Definition 7.20).

Let $R^*=[-\infty,\infty]$. A function $f:D\to R^*$ is lower semianalytic if $D$ is analytic and $\{x\in D\mid f(x)<c\}$ is analytic for every real $c$ (Definition 7.21). For $D\subseteq X\times Y$ write $D_x=\{y\mid (x,y)\in D\}$, $\mathrm{proj}_X(D)=\{x\mid D_x\neq\emptyset\}$, and define the partial infimum

$$f^*(x)=\inf_{y\in D_x}f(x,y),\qquad x\in\mathrm{proj}_X(D).$$

A selector is a function $\varphi:\mathrm{proj}_X(D)\to Y$ whose graph $\mathrm{Gr}(\varphi)$ lies in $D$.

Formalization targets

Goal: Proposition 7.50

Let $X,Y$ be Borel spaces, $D\subseteq X\times Y$ analytic, and $f:D\to R^*$ lower semianalytic.

(a) For every $\varepsilon>0$ there is an analytically measurable selector $\varphi$ with

$$f[x,\varphi(x)]\le\begin{cases}f^*(x)+\varepsilon&\text{if }f^*(x)>-\infty,\\-1/\varepsilon&\text{if }f^*(x)=-\infty.\end{cases}$$

(b) The set $I$ of points where the infimum is attained is universally measurable, and for every $\varepsilon>0$ there is a universally measurable selector $\varphi$ with $f[x,\varphi(x)]=f^*(x)$ on $I$ and the bounds of (a) off $I$.

The goal fixes no constant beyond the book's $\varepsilon$ and $-1/\varepsilon$.

Milestones

In attack order: Proposition 7.40 (Borel images and preimages of analytic sets are analytic), Corollary 7.42.1 ($\mathscr A_X\subseteq\mathscr U_X$), Corollary 7.44.2 (composites of analytically measurable maps are universally measurable), and Proposition 7.49, the Jankov–von Neumann theorem:

$$A\subseteq X\times Y\text{ analytic}\ \Longrightarrow\ \exists\,\varphi:\mathrm{proj}_X(A)\to Y\ \text{analytically measurable},\ \mathrm{Gr}(\varphi)\subseteq A.$$

Further items of the mission, on the same definitions: Proposition 7.39 (projections of analytic sets are analytic, and every analytic set is a projection of a Borel set), Lemma 7.30(1) (strict and non-strict, real and extended level sets give the same class) and Proposition 7.47 (lower semianalytic functions are exactly partial infima of Borel functions).

Significance

Proposition 7.50 is the selection theorem behind the existence of ε-optimal policies in Borel-space dynamic programming. In the finite-horizon model of Chapter 8 the optimal cost-to-go at each stage is lower semianalytic, by Propositions 7.47 and 7.48. Proposition 7.50 then turns the one-stage minimization into a measurable policy, analytically measurable when only ε-optimality is required and universally measurable when the minimum is attained. Chapters 8–9 of the book (the finite-horizon recursion $J^*_K=T^K(J_0)$ and the optimality equation under (P), (N), (D)) use it at every step. Downstream catalog papers on average-cost and stochastic shortest-path problems over Borel spaces cite these results.

All results here are proved in the book and in the descriptive set theory literature (Kechris, Classical Descriptive Set Theory, §18 and §29). None is formalized on Prove2Me. Mathlib has analytic sets in Polish-type settings, the Lusin separation theorem and Suslin's theorem, but it has no universal σ-algebra, no analytic σ-algebra, no lower semianalytic functions and no Jankov–von Neumann uniformization. The definitions in this mission are reusable by the later missions of the series (Chapters 8–10), which restate them locally until these are published.

Difficulty

The obvious route to a selector is to choose, for each $x$, a minimizing or near-minimizing $y$. The axiom of choice provides such a function, but nothing makes it measurable, and the conclusion of the theorem is exactly that measurability. The Borel route fails too: the set $\{x\mid f^*(x)<c\}$ is a projection of a Borel set, which is analytic but in general not Borel, so no Borel-measurable selector exists in general. The Jankov–von Neumann theorem needs a lexicographically least branch of a continuous parametrization of $A$ by $\mathscr N$, and an argument that the resulting map is measurable with respect to $\mathscr A_X$, which is generated by sets that are not closed under complementation. Part (b) adds a further obstacle: the composite of two analytically measurable maps need not be analytically measurable, so the exact selector is only universally measurable. Proving that requires Lusin's theorem that analytic sets are measurable for every completed probability measure.

Formalization scope

• A Borel space is a type with a topology satisfying the class IsBorelSpace (Definition 7.7, the ambient complete separable metric space taken in the same universe), together with Mathlib's [MeasurableSpace X] [BorelSpace X], so measurable sets are exactly the Borel sets. On $X\times Y$ the product σ-algebra is used; it coincides with $\mathscr B_{X\times Y}$ for separable metrizable spaces (Proposition 7.13).
• Analytic sets are Mathlib's MeasureTheory.AnalyticSet (empty or a continuous image of ℕ → ℕ).
• $R^*$ is EReal. The book uses $\infty-\infty=\infty$, and Mathlib's EReal uses $\bot+\top=\bot$. No statement of this mission adds infinities of opposite sign; $f^*(x)+\varepsilon$ adds a real number.
• Functions on $D$ and on $\mathrm{proj}_X(D)$ are functions on subtypes. The graph condition $\mathrm{Gr}(\varphi)\subseteq D$ is part of every selector statement.
• Universally measurable means NullMeasurableSet E p for every probability measure p.
• "Analytically measurable" refers to the σ-algebra generated by analytic sets. Replacing it by the power set, dropping the graph condition, or dropping the $-1/\varepsilon$ case would make the selection theorems a consequence of the axiom of choice. The statements rule all three out.

Not included: Lusin's theorem in Suslin-scheme form (Proposition 7.42, which needs the Suslin operation as a definition), Proposition 7.43 on $P(X)$, the integration results of Propositions 7.46 and 7.48, and Lemma 7.30(2)–(4). None is used in the proof of the goal. Contributions welcome: the bridge between IsBorelSpace and Mathlib's StandardBorelSpace, the universal σ-algebra API, and the Jankov–von Neumann theorem itself.

Selected references

• D. P. Bertsekas and S. E. Shreve, Stochastic Optimal Control: The Discrete-Time Case, Academic Press 1978; Athena Scientific 1996, §7.6–7.7. https://web.mit.edu/dimitrib/www/soc.html
• D. Blackwell, D. Freedman and M. Orkin, The optimal reward operator in dynamic programming, Annals of Probability 2 (1974) 926–941. https://doi.org/10.1214/aop/1176996558
• A. S. Kechris, Classical Descriptive Set Theory, Graduate Texts in Mathematics 156, Springer 1995, §18 (Jankov–von Neumann uniformization), §29 (measurability of analytic sets). https://doi.org/10.1007/978-1-4612-4190-4
• 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

Why revenue sharing

A supplier who sells to an independent retailer through a plain per-unit wholesale price faces double marginalization: the retailer orders less than the quantity that maximizes the profit of the supply chain as a whole, because each unit costs him the wholesale price rather than the production cost. Supply chain contracting studies payment schemes under which the retailer's own optimum coincides with the system optimum. Such a scheme is said to coordinate the channel. The usual examples are buy-back contracts (Pasternack, 1985), quantity-flexibility contracts (Tsay and Lovejoy, 1999) and quantity discounts (Jeuland and Shugan, 1983; Moorthy, 1987).

Cachon and Lariviere study revenue sharing, in which the retailer pays a low wholesale price and also hands over a fixed fraction of his revenue. The scheme was common in video-cassette rental in the late 1990s, where it let rental chains stock far more copies of new releases. This mission formalizes the paper's single-retailer result: revenue sharing coordinates the channel, and the supplier can choose any split of the channel's maximal profit. It also includes the three further results of the paper that use the same argument.

The source is the authors' working paper of June 2000. Its results are unnumbered, so every item cites a section, a displayed equation and a printed page. The 2005 Management Science version renumbers and revises the material.

Setting

A supplier sells to one retailer, who orders $q \ge 0$ units before a selling season. The retailer's expected revenue is a function $R(q)$ of the quantity alone. Leftover units have zero salvage value, and the supplier produces each unit at cost $c > 0$. The paper's standing assumptions (Sec. 1, p. 5) are:

• $R$ is strictly concave and differentiable for $q \ge 0$, with marginal revenue $R'(q)$;
• the product is viable: $R'(0) > c$;
• a finite quantity is optimal: $R'(\infty) < c$.

A revenue-sharing contract $\{\phi, w\}$ has two terms. The retailer pays the wholesale price $w \ge 0$ per unit, and he keeps the share $\phi$ of the revenue and transfers $(1-\phi)R(q)$ to the supplier. The case $\phi = 1$ is the plain wholesale-price contract. The profits of the supply chain, the retailer and the supplier are

$$\Pi(q) = R(q) - qc,\qquad \pi_r(q) = \phi R(q) - qw,\qquad \pi_s(q) = (1-\phi)R(q) + qw - qc .$$

The integrated channel quantity $q_I$ is the maximizer of $\Pi$ over $q \ge 0$. In Lean these objects are RevShareCoord.Single.Model (fields R, R', c and the three assumptions) and its functions Pi, retailerProfit and supplierProfit.

Formalization targets

Goal: revenue sharing coordinates the channel (Sec. 2.2, p. 6)

Let $\phi \in (0,1]$ and $w(\phi) = \phi c$. Then

$$q_I = \operatorname*{arg\,max}_{q\ge 0}\ \pi_r(q) \ \text{(uniquely)},\qquad w(\phi)\le c,\qquad \pi_r(q_I) = \phi\,\Pi(q_I),\qquad \pi_s(q_I) = (1-\phi)\,\Pi(q_I).$$

The statement fixes no revenue function and no share. It holds for every model and every $\phi \in (0, 1]$, which is what "the supplier can take any share of the channel profit" means.

Milestones on the way

1. Eq. (1), p. 6. $q_I$ exists, is unique and positive, and is the only positive root of $R'(q_I) = c$.
2. Retailer's first-order condition, p. 6. If $R'(0) > w/\phi$, an order $\hat q \ge 0$ is optimal for the retailer exactly when $\hat q > 0$ and $\phi R'(\hat q) = w$. The retailer has at most one optimal order.
3. Profit identities, p. 6. Under $\{\phi, \phi c\}$, $\pi_r(q) = \phi\Pi(q)$ and $\pi_s(q) = (1-\phi)\Pi(q)$ at every $q$.
4. Heterogeneous retailers, p. 7. Given $c$ and $\phi$, a single wholesale price, chosen before the revenue function, coordinates every retailer of the model.

Further results on the same argument

5. Buy-back equivalence, Sec. 2.3, p. 9. Take the fixed-price newsvendor and the buy-back contract $b^* = p(1-\phi)$, $w_b^* = p(1-\phi)+\phi c$. It gives the retailer and the supplier the same realized profits as $\{\phi, \phi c\}$, for every order and every demand realization.
6. Endogenous price, Sec. 3.1 and footnote 3, p. 11. Let revenue $\mathrm{Rev}(q,p)$ be any function of quantity and price, with costs linear in quantity. Then $\pi_r(q,p) = \phi\,\Pi(q,p)$ under $\{\phi,\phi c\}$, and the integrated optimum $(q_I,p_I)$, assumed unique, is the retailer's unique optimum.

Significance

The result separates coordination from profit division. A contract family coordinates for every value of a parameter, and that parameter then moves profit between the firms without changing the quantity, so the contract terms can be settled by bargaining power alone. The heterogeneous-retailer milestone gives the practical advantage over quantity discounts: the coordinating terms do not depend on the retailer's demand, so one price list serves retailers who face different markets. The Sec. 2.3 equivalence shows that, in the fixed-price newsvendor, buy-backs are a special case of revenue sharing. The Sec. 3.1 statement shows that revenue sharing still coordinates when the retailer also sets the price, a setting in which Emmons and Gilbert (1998) showed buy-backs fail.

All of these results are proved in the paper, and none is open. The mission adds a machine-checked version of the single-retailer theory for a general strictly concave revenue function. A related newsvendor version is already formalized on the platform: SupplyChainTheory.revenue_sharing_coordinates, from Snyder and Shen, Fundamentals of Supply Chain Theory, Thm 14.6. That version has a newsvendor revenue with salvage values and goodwill costs, and it concludes the optimality of three profits, not the $\phi$-split of this paper. It is a different statement, so it is not reused here.

Difficulty

The algebra is short. The identity $\pi_r = \phi\Pi$ under $w = \phi c$ is a single line, and it is a milestone, not the goal. The work lies in the optimization claims over a half-line with only one-sided information at $0$. The integrated optimum must be shown to exist. $R'(\infty) < c$ gives only an eventual bound on the derivative, so the existence argument needs the continuity of a concave function and its supergradient inequality. It must also be shown positive, which uses $R'(0) > c$ as a one-sided derivative. Its uniqueness rests on strict concavity. The retailer's first-order condition needs the same machinery for $\phi R - wq$, including the observation that the boundary point $0$ is never optimal. A stationary point of $\pi_r$ is not enough. The goal asserts that $q_I$ is the unique maximizer over all of $[0,\infty)$.

Formalization scope

• Quantities, prices and shares are real numbers. $R$ and $R'$ are functions $\mathbb R \to \mathbb R$, constrained only on $[0,\infty)$. Differentiability is HasDerivWithinAt R (R' q) (Set.Ici 0) q for $q \ge 0$, so it is one-sided at $0$. Strict concavity is StrictConcaveOn ℝ (Set.Ici 0) R.
• $R'(\infty) < c$ is encoded as "$R'(Q) < c$ for some $Q \ge 0$". For a decreasing $R'$ this is equivalent, and it allows $R' \to -\infty$.
• "Optimal" means IsMaxOn over $[0,\infty)$ (over $[0,\infty)\times P$ in Sec. 3.1), and "unique" means every other maximizer equals it.
• The supplier's profit $\pi_s$ is not displayed in the paper. It is read off the sequence of events of Sec. 1.
• The goal and the first-order condition take $\phi \in (0,1]$. At $\phi = 0$ the retailer's profit is identically zero and $q_I$ is not the unique optimum. The profit identities and the buy-back identities hold for all real parameters and are stated that way.
• Corrected slips. (a) Eq. (1) is introduced with "$R'(0) \ge c$". This contradicts the standing assumption $R'(0) > c$: with equality, $q_I = 0$ is not positive. The statement uses $R'(0) > c$. (b) The display $\pi_r(q_I) = \phi R(q_I) - q_I c = \phi\Pi(q_I)$ has a wrong middle term, which should read $\phi R(q_I) - q_I\phi c$. The outer equality is stated.
• The first-order-condition milestone adds the converse direction and uniqueness to the paper's "must satisfy". It does not claim that an optimum exists, which may fail when $w/\phi < c$.
• Sec. 3.1 is stated in the generality of footnote 3: an arbitrary revenue function $\mathrm{Rev}(q,p)$ and a set $P$ of admissible prices, with the integrated optimum's uniqueness as a hypothesis, as the paper assumes it. The paper's monotonicity of $F(x,p)$ in $p$ is unused and omitted.
• Sec. 2.3 is formalized pathwise. The expected-profit equations (2)–(4) are not part of the mission.
• A goal that only asserts $\pi_r(\phi, \phi c, q) = \phi\,\Pi(q)$ would be an unfolding of definitions. The goal therefore carries the argmax-and-uniqueness claim, which needs strict concavity and the model's assumptions.
• Needed infrastructure: first-order conditions for concave functions on a closed half-line with one-sided derivatives, and existence of maximizers from an eventual derivative bound. Both are reusable beyond this mission. Contributions of that general kind are welcome.

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
• B. A. Pasternack, Optimal pricing and return policies for perishable commodities, Marketing Science 4(2):166–176, 1985. https://doi.org/10.1287/mksc.4.2.166
• K. S. Moorthy, Managing channel profits: Comment, Marketing Science 6(4):375–379, 1987. https://doi.org/10.1287/mksc.6.4.375
• A. A. Tsay, W. S. Lovejoy, Quantity flexibility contracts and supply chain performance, Manufacturing & Service Operations Management 1(2):89–111, 1999. https://doi.org/10.1287/msom.1.2.89
• H. Emmons, S. M. Gilbert, Note: The role of returns policies in pricing and inventory decisions for catalogue goods, Management Science 44(2):276–283, 1998. https://doi.org/10.1287/mnsc.44.2.276
• L. V. Snyder, Z.-J. M. Shen, Fundamentals of Supply Chain Theory, 2nd ed., Wiley, 2019, Ch. 14. https://doi.org/10.1002/9781119584445