All missions

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

Motivation

Many problems in optimization and numerical analysis reduce to finding a point in the intersection of finitely many closed convex sets: solving a system of linear equations or inequalities, reconstructing an image from projections, or finding a feasible point of a convex program. The classical methods for this convex feasibility problem project the current point onto one set at a time, in Euclidean distance: Kaczmarz (1937) for linear equations, Agmon and Motzkin–Schoenberg (1954) for linear inequalities, and the cyclic projection method for general convex sets studied by Gubin, Polyak and Raik (1967).

L. M. Bregman's 1967 paper replaces the Euclidean distance by a general function $D(x,y)$ satisfying a short list of axioms, and shows that the projection method still works. The functions $D(x,y)=f(x)-f(y)-\langle\nabla f(y),x-y\rangle$ built from a strictly convex $f$ are the ones now called Bregman divergences, and the paper is the origin of Bregman projections, of the row-action methods of Censor and collaborators, and indirectly of mirror descent. Its §2 uses the abstract result to solve convex programs with linear constraints by relaxation.

This mission formalizes §1 of the paper for the cyclic control, in which the sets are visited in a fixed round-robin order. A companion mission treats the remotest-set control of Theorem 2, and two further missions treat the convex-programming results of §2.

Setting

Let $X$ be a real linear topological space and $A_0,\dots,A_{m-1}$ closed convex subsets of $X$, with intersection $R=\bigcap_i A_i$. Let $S\subset X$ be a convex set with $S\cap R\ne\emptyset$, and let $D:S\times S\to\mathbb R$. The paper requires:

• I. $D(x,y)\ge 0$, with equality if and only if $x=y$.
• II. For every $y\in S$ and every $i$ there is a point $P_iy\in A_i\cap S$ minimizing $D(\cdot,y)$ over $A_i\cap S$; it is the $D$-projection of $y$ onto $A_i$.
• III. For every $i$ and $y\in S$, the function $z\mapsto D(z,y)-D(z,P_iy)$ is convex on $A_i\cap S$.
• IV. $D(\cdot,y)$ has derivative $0$ at the point $y$.
• V. For every $z\in R\cap S$ and real $L$, the sublevel set $\{x\in S\mid D(z,x)\le L\}$ is compact.
• VI. If $D(x^n,y^n)\to 0$, $y^n\to y^*\in\bar S$, and $\{x^n\}$ lies in a compact set, then $x^n\to y^*$.

The relaxation sequence with control $(i_n)$ starts at any $x^0\in S$ and sets $x^{n+1}=P_{i_n}x^n$. Under the cyclic control $i_n=n\bmod m$, the sets are projected onto in the order $A_0,A_1,\dots,A_{m-1},A_0,\dots$. A limiting point of $\{x^n\}$ is the limit of a convergent subsequence $x^{n_k}$.

The Lean development uses the namespace BregmanRelax.Cyclic: DConditions A S D P bundles conditions I–IV and VI together with the closedness and convexity of the sets, CondV S D Z is condition V for the points of $Z$, IsRelaxSeq S P i x is the relaxation sequence with control $i$, and cyclicControl hm is $n\mapsto n\bmod m$.

Formalization targets

Goal: Theorem 1 (p. 203)

Under conditions I–VI, with the cyclic control, every limiting point of every relaxation sequence lies in every set:

$$x^{n_k}\to x^* \quad\Longrightarrow\quad x^*\in\bigcap_{i=0}^{m-1}A_i .$$

The statement is about every starting point $x^0\in S$ and every convergent subsequence. It does not assert that the whole sequence converges.

Milestones

1. 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).$$

2. Lemma 2 (2) (p. 202): for any control and any $z\in R\cap S$, $\lim_{n\to\infty}D(z,x^n)$ exists.
3. Lemma 2 (3) (p. 202): for any control, $D(x^{n+1},x^n)\to 0$.
4. Lemma 2 (1) (p. 202): for any control, $\{x^n\}$ lies in a compact set.

Further result: Note 1, condition (1) (pp. 204–205)

For any control whose relaxation sequence has all its limiting points in $R$ (the cyclic control, by Theorem 1), if in addition $S$ is closed and $y\mapsto D(z_1,y)-D(z_2,y)$ is continuous on $S$ for all $z_1,z_2\in R\cap S$, then the relaxation sequence converges to a point of $R$.

Significance

Theorem 1 is the abstract convergence theorem behind cyclic Bregman projections. With $D(x,y)=\|x-y\|^2$ in a Hilbert space it gives the convergence of cyclic orthogonal projections onto finitely many closed convex sets in the weak topology (the paper's Example 1). With $D$ given by a Bregman divergence it gives the method that the paper's §2 turns into an algorithm for convex programs with linear equality and inequality constraints, including entropy maximization. Lemma 1, the generalized Pythagorean inequality, is used throughout the later literature on Bregman projections, mirror descent and online learning.

The results are proved in the paper and are classical. To our knowledge no machine-checked version exists: Mathlib has orthogonal projections onto closed convex sets in Hilbert spaces, but no Bregman projections and no convergence theorem for cyclic projection methods. A formalization supplies an axiomatic interface (conditions I–VI) that does not depend on any particular divergence, so special cases (Euclidean distance, Kullback–Leibler divergence, Bregman divergences of Legendre functions) can be obtained by checking the conditions.

Difficulty

There is no norm and no metric: $D$ is neither symmetric nor subject to a triangle inequality, and $X$ is only a topological vector space. The usual Fejér-monotonicity argument for Euclidean projections, which compares distances to a fixed point of $R$, works only one way in $D$. Convergence of a subsequence $x^{n_k}$ does not by itself say anything about the shifted subsequences $x^{n_k+1},\dots,x^{n_k+m-1}$, and these are needed to reach every set $A_i$. That step requires condition VI together with compactness, and condition VI has a compactness premise that has to be supplied separately. Throughout, convergence is in a general topology where "compact" and "sequentially compact" may differ.

Formalization scope

The formalization commits to the following readings, each recorded in the items' Formalization Notes.

• The projection is a map. $P:\iota\to X\to X$ is fixed, and condition II states that $P_iy$ is a minimizer. Condition III is stated for this map.
• Condition IV, one-sided. The paper asks for $\lim_{t\to0}D(y+tz,y)/t=0$ for every $z\in X$. The formalization assumes only the right-hand limit in the directions $w-y$ with $w\in S$, which is what the proofs use and what the paper's IV implies. Every theorem is therefore at least as strong as the paper's.
• Compactness is sequential. "Compact" in V, VI and Lemma 2 (1) is IsSeqCompact. The set of elements of $\{x^n\}$ being compact is read as $\{x^n\}$ lying in a sequentially compact set.
• Hausdorff space. The proof of Theorem 1 identifies two limits of one sequence, so T2Space X is assumed. $X$ is a real topological vector space (IsTopologicalAddGroup, ContinuousSMul ℝ).
• Limiting point means the limit of x ∘ φ for a strictly increasing φ : ℕ → ℕ.
• Index base. The sets are indexed by Fin m with $0<m$, and the cyclic control is $n\mapsto n\bmod m$, the paper's $i_n=(n\bmod m)+1$ shifted by one.
• Translation typos. Condition II is printed as "$D(x,y)=\min_{z\in A_i\cap S}D(z,x)$" with "$i\in T$". The formalization reads $\min_z D(z,y)$ and $i\in I$. In Lemma 2 (2) the faint set symbol is read as $R$, and $z$ is taken in $R\cap S$, as in the proof.
• Domain of $D$. $D$ is a total function X → X → ℝ; every condition constrains it on $S\times S$ only, and the standing assumption $S\cap R\ne\emptyset$ is an explicit hypothesis.

A trivializing formalization is ruled out: the hypotheses are satisfiable (a sorry-free local check takes $X=\mathbb R$, $D(x,y)=(x-y)^2$, two overlapping closed intervals and the clamp projections), the conclusion concerns every limiting point of every cyclic run, and the goal neither assumes convergence nor restricts the control.

Contributions welcome: proofs of the milestones, a proof of the goal, and instances of DConditions for concrete divergences (squared Euclidean distance in finite dimension, Bregman divergences of strictly convex differentiable functions). These instances are reusable by the companion missions of this paper.

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) (1967) 200–217. https://doi.org/10.1016/0041-5553(67)90040-7
• L. G. Gubin, B. T. Polyak, E. V. Raik, The method of projections for finding the common point of convex sets, USSR Computational Mathematics and Mathematical Physics 7(6) (1967) 1–24. https://doi.org/10.1016/0041-5553(67)90113-9
• T. S. Motzkin, I. J. Schoenberg, The relaxation method for linear inequalities, Canadian Journal of Mathematics 6 (1954) 393–404. https://doi.org/10.4153/CJM-1954-038-x
• Y. Censor, A. Lent, An iterative row-action method for interval convex programming, Journal of Optimization Theory and Applications 34 (1981) 321–353. https://doi.org/10.1007/BF00934676

Motivation

Every step of the dynamic programming algorithm on a general state space does three things: it takes a conditional expectation of the cost-to-go under a transition kernel, it minimizes the resulting function of state and control over the control, and, if a policy is to be produced, it picks a control for each state that attains or nearly attains that minimum. On a finite or countable state space all three are harmless. On an uncountable state space each can destroy the measurability needed to take the next expectation: the infimum over an uncountable family of measurable functions need not be measurable, and a minimizer chosen state by state need not be a measurable function of the state, so it does not define a policy at all.

Section 7.5 of Bertsekas and Shreve, Stochastic Optimal Control: The Discrete-Time Case (1978; Athena Scientific reprint 1996), settles the three operations for semicontinuous costs and continuous kernels. The results are the topological half of the book's measurability theory; the descriptive set theory half (lower semianalytic functions and analytically measurable selectors, §7.6–7.7) is a separate mission in this series. The semicontinuous results are what Propositions 8.6–8.7 and Corollaries 9.17.2–9.17.3 of the book use to obtain Borel-measurable optimal policies for finite-horizon and infinite-horizon models with lower semicontinuous costs and compact control sets.

Timeline. The exact selection theorem for lower semicontinuous functions (Proposition 7.33 below) is credited by the book's notes to Dubins and Savage, How to Gamble If You Must (1965). The Hausdorff metric on closed sets goes back to Hausdorff's Set Theory. Measurable selection in the closed-valued setting was later systematized by Kuratowski and Ryll-Nardzewski (1965), whose theorem gives a different route to results of this kind.

Setting

Throughout, $R^*=[-\infty,+\infty]$ is the extended real line. A function $f:X\to R^*$ on a metrizable space $X$ is lower semicontinuous if every sublevel set $\{x\mid f(x)\le c\}$, $c\in\mathbb R$, is closed, and upper semicontinuous if every superlevel set $\{x\mid f(x)\ge c\}$ is closed (Definition 7.13). $C(X)$ is the space of bounded continuous real-valued functions on $X$.

For a separable metrizable space $Y$, $P(Y)$ is the set of Borel probability measures on $Y$ with the weak topology (convergence of integrals of functions in $C(Y)$). A stochastic kernel $q(dy\mid x)$ on $Y$ given $X$ is a map $x\mapsto q(dy\mid x)$ from $X$ to $P(Y)$, and it is continuous if this map is continuous (Definition 7.12). The integral of a Borel-measurable $f:Y\to R^*$ is $\int f\,dp=\int f^+dp-\int f^-dp$ with the convention $-\infty+\infty=+\infty-\infty=+\infty$ (Eq. (43) of Chapter 7).

For a compact metric space $Y$, $2^Y$ is the collection of closed subsets of $Y$ with the topology of the Hausdorff metric (Appendix C). For $D\subseteq X\times Y$, the section at $x$ is $D_x=\{y\mid (x,y)\in D\}$, the projection is $\mathrm{proj}_X(D)=\{x\mid D_x\neq\emptyset\}$, and a function $\varphi:\mathrm{proj}_X(D)\to Y$ has its graph in $D$ if $(x,\varphi(x))\in D$ for every $x\in\mathrm{proj}_X(D)$. "Borel-measurable" refers to the Borel σ-algebras of the topologies in question; on $\mathrm{proj}_X(D)$ this is the Borel σ-algebra of the subspace topology.

Formalization targets

Goal: Proposition 7.33

Let $X$ be metrizable, $Y$ compact metrizable, $D\subseteq X\times Y$ closed, and $f:D\to R^*$ lower semicontinuous. Put

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

Then $\mathrm{proj}_X(D)$ is closed, $f^*$ is lower semicontinuous, and there is a Borel-measurable $\varphi:\mathrm{proj}_X(D)\to Y$ with graph in $D$ and

$$f\bigl(x,\varphi(x)\bigr)=f^*(x)\qquad\forall x\in\mathrm{proj}_X(D).$$

Milestones

• Proposition 7.32: for $f^*(x)=\inf_{y\in Y}f(x,y)$, lower semicontinuity of $f$ and compactness of $Y$ give lower semicontinuity of $f^*$ and attainment; upper semicontinuity of $f$ gives upper semicontinuity of $f^*$.
• Lemma 7.18: there is a Borel-measurable $\sigma:2^Y-\{\emptyset\}\to Y$ with $\sigma(A)\in A$.
• Lemma 7.20: for lower semicontinuous $f$ on a nonempty compact $Y$, the argmin map $x\mapsto\{y\mid f(x,y)\le f^*(x)\}$ is Borel-measurable into $2^Y$.
• Lemma 7.14: $f$ is lower semicontinuous and bounded below iff $f_n\uparrow f$ for some $f_n\in C(X)$ (and dually).
• Proposition 7.30: $x\mapsto\int f(x,y)\,q(dy\mid x)$ is continuous for $f\in C(X\times Y)$ and continuous $q$.
• Proposition 7.31: the same map is lower (upper) semicontinuous and bounded below (above) when $f$ is.
• Lemma 7.21: an open $G\subseteq X\times Y$, $Y$ separable, has open projection and a Borel-measurable selector with graph in $G$.
• Proposition 7.34: for open $D$ and upper semicontinuous $f$, $\mathrm{proj}_X(D)$ is open, $f^*=\inf_{D_x}f$ is upper semicontinuous, and for each $\varepsilon>0$ there is a Borel-measurable $\varphi_\varepsilon$ with graph in $D$ and

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

Significance

The results. Propositions 7.31–7.33 are the closure properties that make the dynamic programming recursion stay inside the class of lower semicontinuous functions bounded below: the expectation step preserves the class (7.31), the minimization step preserves it (7.32, 7.33), and the minimization admits a Borel-measurable exact minimizer (7.33). This is why, in semicontinuous models, the optimal cost functions are lower semicontinuous and optimal policies can be taken Borel-measurable and nonrandomized. Proposition 7.34 gives the weaker, $\varepsilon$-optimal counterpart for upper semicontinuous costs, where the infimum need not be attained.

Formalizing them. All of these results are proved in the book; none is open. As far as is known, none has a machine-checked proof: Mathlib has semicontinuity, the Hausdorff extended metric on closed and on nonempty compact sets, and the weak topology on probability measures, but no theorem combining them into a measurable selection result of this kind. A formal development would supply measurable selectors for semicontinuous minimization in Lean and the Borel-measurability of set-valued maps into the hyperspace of closed sets, both reusable well beyond dynamic programming.

Difficulty

The obvious attempt at the goal is to pick, for each $x$, some minimizer $y$ of $f(x,\cdot)$ over the compact section $D_x$. The minimizer exists by compactness and lower semicontinuity, but the choice is made pointwise and gives no control on measurability: a minimizer chosen by the axiom of choice need not be Borel-measurable. The argmin sets $F^*(x)$ vary with $x$ only semicontinuously: they can jump from a single point to a large set, so a continuous selection generally does not exist, and continuity arguments cannot replace measurability. Lemma 7.18 isolates the hardest part: a choice of a point of each nonempty closed set that is measurable as a function of the set itself.

A second difficulty is bookkeeping at infinity. Values $\pm\infty$ are allowed throughout, so sublevel sets, minima, integrals and $\varepsilon$-bounds must all be handled in $R^*$; the integral in Proposition 7.31 uses the convention $\infty-\infty=+\infty$, which is not Mathlib's.

Formalization scope

• Extended reals. Values are in EReal. The only place where values of opposite infinite sign are combined is the integral, which is the published definition DupacovaWets.Consistency.expect (reused, not restated): $\int f^+-\int f^-$ with an explicit case returning $+\infty$ when $\int f^+=\infty$, exactly the book's convention (42). The $\varepsilon$-bound of Proposition 7.34 adds a real $\varepsilon$ to a value different from $-\infty$, which is safe in EReal.
• Semicontinuity is Mathlib's LowerSemicontinuous/UpperSemicontinuous, equivalent to Definition 7.13 for EReal-valued functions. Lemma 7.13 of the book (the sequential characterization) is Mathlib's lowerSemicontinuous_iff_le_liminf together with first countability of metrizable spaces, and is not restated here.
• Functions on $D$. Functions "on $D$" are functions on $X\times Y$ with LowerSemicontinuousOn f D (resp. UpperSemicontinuousOn); values off $D$ play no role. $\mathrm{proj}_X(D)$ is Prod.fst '' D, selectors are functions on that subtype, and its σ-algebra is the Borel σ-algebra of the subspace topology.
• Hyperspace. $2^Y$ is Closeds Y, and $2^Y-\{\emptyset\}$ for compact $Y$ is NonemptyCompacts Y, each with the Hausdorff extended metric and the Borel σ-algebra of its topology. This topology agrees with the book's (the exponential topology of Appendix C, independent of the metric).
• Boundedness. "Bounded below/above" is by a real constant. BddBelow in EReal would be vacuous and is not used.
• Edge cases. Proposition 7.32(a)'s attainment clause is stated for nonempty $Y$, since for $Y=\emptyset$ the infimum is $+\infty$ and nothing attains it.
• Argmin minimum. Lemma 7.20 assumes nonempty $Y$ because its defining formula uses a minimum; for empty $Y$ there is no minimizer.
• Ruling out trivial readings. The graph condition $(x,\varphi(x))\in D$ is part of every selection statement; without it the goal would follow from the unconstrained case. The selector must be Borel-measurable on $\mathrm{proj}_X(D)$ and must attain the minimum exactly, not up to $\varepsilon$.

A complete development needs the Borel structure of the hyperspace (measurability of maps into Closeds Y from upper semicontinuity in the sense of Kuratowski, Proposition C.4 of the book), the construction of a measurable choice function on NonemptyCompacts Y, and approximation of semicontinuous functions by monotone sequences in $C(X)$. Each of these is reusable on its own; proofs of individual milestones by any route 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, Section 7.5 and Appendix C. https://web.mit.edu/dimitrib/www/soc.html
• L. E. Dubins and L. J. Savage, How to Gamble If You Must: Inequalities for Stochastic Processes, McGraw-Hill, 1965.
• K. Kuratowski and C. Ryll-Nardzewski, "A general theorem on selectors," Bull. Acad. Polon. Sci. 13 (1965), 397–403.
• F. Hausdorff, Set Theory, Chelsea, New York, 1957.

Motivation

Many networks are built and paid for by the users they serve: multicast trees, virtual overlays, shared subnetworks of the Internet. A protocol proposes a design and a rule for splitting its cost, and each participant is free to accept the proposal or defect to a cheaper alternative. The designer therefore cannot impose the global optimum; the best it can do is propose the cheapest outcome that no participant wants to leave, a Nash equilibrium. The ratio between the cost of the best equilibrium and the optimal cost, the price of stability, measures the loss caused by requiring stability. It contrasts with the price of anarchy, which compares the worst equilibrium with the optimum and suits settings with no coordinating protocol at all.

Anshelevich, Dasgupta, Kleinberg, Tardos, Wexler and Roughgarden (SIAM J. Comput. 2008; preliminary version FOCS 2004) studied this question for the most common cost-sharing rule, the Shapley (equal-split) rule, under which every user of an edge pays the same share of its cost. Their first result, the subject of this mission, is that the price of stability is at most the harmonic number $H(k)$, where $k$ is the number of players, and that this bound is attained in the limit.

Setting

There are $k$ players and a finite set $E$ of edges. Each player $i$ has a family $\Sigma_i$ of feasible strategies, each a set of edges; in the network setting $\Sigma_i$ consists of the edge sets connecting player $i$'s terminals in a directed graph. Each edge $e$ has a nonnegative cost $c_e$. In a strategy vector $S=(S_1,\dots,S_k)$, $S_i\in\Sigma_i$, let $x_e$ be the number of players whose strategy contains $e$. Under Shapley cost sharing player $i$ pays

$$C_i(S)=\sum_{e\in S_i}\frac{c_e}{x_e}.$$

The cost of the designed network is

$$\operatorname{cost}(S)=\sum_{e\in\bigcup_i S_i}c_e ,$$

and the payments add up to exactly this amount. The profile $S$ is a (pure) Nash equilibrium if no player $i$ has a strategy $S_i'\in\Sigma_i$ with $C_i(S_{-i},S_i')<C_i(S)$. Finally,

$$H(k)=1+\tfrac12+\dots+\tfrac1k .$$

The game is a congestion game: the per-user cost of an edge, $f_e(x)=c_e/x$, depends only on the edge and its number of users. Rosenthal's potential

$$\Phi(S)=\sum_{e\in E}\sum_{x=1}^{x_e}f_e(x)$$

changes by exactly the deviating player's change in cost when a single player changes strategy. The same objects are used with load-dependent edge costs $c_e(x)$, in which case $f_e(x)=c_e(x)/x$.

Formalization targets

Goal: Theorem 2.1 and its tightness

For every game with $c_e\ge0$ in which each player has a feasible strategy there is a Nash equilibrium $S$ with

$$\operatorname{cost}(S)\le H(k)\cdot\operatorname{cost}(P)\quad\text{for every profile }P,$$

and for every $k\ge1$, $\varepsilon>0$ the instance of Fig. 1.1 (player $i$ has its own path of cost $1/i$, and all players can share a path of cost $1+\varepsilon$) has a Nash equilibrium, every Nash equilibrium of it costs $H(k)$, and some profile costs $1+\varepsilon$. The ratio $H(k)/(1+\varepsilon)$ tends to $H(k)$ as $\varepsilon\to0$.

Milestones

1. Budget balance: $\sum_iC_i(S)=\operatorname{cost}(S)$ for every $S$ (Sect. 1).
2. Rosenthal's potential is exact (Theorem 2.1, proof, (2.1)).
3. From every profile some Nash equilibrium of no larger potential is reached (Theorem 2.1, proof).
4. Theorem 3.1: if $\operatorname{cost}(S)\le A\,\Phi(S)$ and $\Phi(S)\le B\operatorname{cost}(S)$ for all $S$, the price of stability is at most $AB$.
5. For nondecreasing concave edge costs $c_e(x)$: $\operatorname{cost}(S)\le\Phi(S)\le H(k)\operatorname{cost}(S)$ (Theorem 2.3, proof).
6. Theorem 2.3: the $H(k)$ bound for nondecreasing concave edge costs.
7. The Fig. 1.1 instance: its Nash equilibrium is unique and costs $H(k)$; a profile costs $1+\varepsilon$.

Significance

The bound shows that requiring stability under the Shapley rule costs at most a logarithmic factor, $H(k)=\Theta(\log k)$, whereas the price of anarchy of the same game is $k$ (two parallel edges of costs $1$ and $k$ already show this). It was among the first price-of-stability results and is the starting point for a line of work on network design games: the undirected case, where the $H(k)$ bound is not tight and the correct value remained open for years, weighted players, and other cost-sharing rules. The argument (an exact potential that over- and under-estimates the social cost by bounded factors) is the standard tool for price-of-stability bounds, and Theorem 3.1 isolates it in a reusable form.

The theorem is proved in the paper; to our knowledge no machine-checked proof exists. This mission produces a formal account of Shapley cost-sharing games as congestion games, of Rosenthal's potential and the finite improvement property, of the potential-sandwich argument of Theorem 3.1, and of the matching lower-bound instance, for constant and for nondecreasing concave edge costs.

Difficulty

The obvious approach, bounding the cost of an arbitrary equilibrium, fails: some equilibria cost $k$ times the optimum, so any proof must select a particular equilibrium. The selection uses the finiteness of the strategy space together with the exact potential, and the bound needs the inequality $\Phi\le H(k)\cdot\operatorname{cost}$, which for concave costs requires the per-user cost $c_e(x)/x$ to be nonincreasing. On the lower-bound side, the claim that every equilibrium of Fig. 1.1 costs $H(k)$ requires excluding all equilibria in which some players share the common path, for every $k$ at once, not only checking that the all-own profile is stable.

Formalization scope

Games are encoded as congestion games over arbitrary finite families of edge sets, reusing the published CongestionPoA.AsymSum.Model (congestion game, loads, player costs, cost-form pure Nash equilibrium, total cost). The paper notes that its proofs do not use the graph structure; the directed-graph game is the instance in which $\Sigma_i$ is the family of edge sets connecting player $i$'s terminals. Players and edges form finite types; $k$ is the number of players and $H(k)$ is Mathlib's harmonic k cast to $\mathbb R$. The price of stability is stated as the existence of a Nash equilibrium whose cost is at most the constant times the cost of every profile, with no division by the optimum, and with the hypothesis that some profile exists. Concave costs are functions on $\mathbb N$ with nonincreasing increments, nondecreasing, with $c_e(0)\ge0$; this last condition is implicit in the paper and needed for $c_e(x)/x$ to be nonincreasing. Theorem 3.1 carries the implicit hypothesis $A\ge0$.

A statement that bounds every equilibrium is false, and one that asserts a cheap profile without the Nash condition is trivial; both are excluded, and the tightness part quantifies over every Nash equilibrium of the instance and asserts that one exists.

Needed infrastructure: finite improvement paths in potential games, sum manipulations over loads, and bounds on harmonic sums. The potential lemmas apply to every finite congestion game and are reusable beyond this mission. Proofs of any milestone are welcome independently.

Selected references

• E. Anshelevich, A. Dasgupta, J. Kleinberg, É. Tardos, T. Wexler, T. Roughgarden, The Price of Stability for Network Design with Fair Cost Allocation, SIAM J. Comput. 38(4):1602–1623, 2008. https://doi.org/10.1137/070680096
• R. W. Rosenthal, A class of games possessing pure-strategy Nash equilibria, Int. J. Game Theory 2:65–67, 1973. https://doi.org/10.1007/BF01737559
• D. Monderer, L. S. Shapley, Potential games, Games Econ. Behav. 14:124–143, 1996. https://doi.org/10.1006/game.1996.0044