All missions

Motivation

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

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

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

Setting

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

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

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

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

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

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

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

Formalization targets

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

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

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

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

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

Revenue sharing (Sec. 3.2, p. 14)

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

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

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

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

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

Selected references

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

Motivation

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

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

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

Setting

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

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

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

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

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

Formalization targets

Goal: Theorem 2 (p. 203)

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

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

Milestones

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

Significance

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

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

Difficulty

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

Formalization scope

Conventions committed to in Lean:

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

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

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

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

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

Formalization targets

Goal: Proposition 4.2

Under Assumption C,

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

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

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

The statement carries no constants beyond those of Assumption C.

Milestones

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

Further result

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

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

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

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

Selected references

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

Why staffing large call centers is a mathematical question

A call center must choose enough servers to limit waiting while paying for every server it staffs. When arrivals are heavy, small changes in the number of servers can change the probability of delay substantially. Borst, Mandelbaum, and Reiman study how to make this choice when the arrival rate grows and the costs of staffing and waiting need not grow at the same rate. Their CWI report treats several regimes within one queueing model. This mission concerns the efficiency-driven regime, where the incremental staffing cost eventually dominates the conditional waiting cost at every fixed positive square-root staffing offset. The resulting rule chooses an offset by optimizing a simpler cost that treats the probability of waiting as one.

The result is useful when the staffing-cost and waiting-cost primitives change with system scale. It says that the simplified choice still attains the optimal total cost asymptotically, even though the actual staffing decision is an integer and the simplified problem uses a real variable. The report states this as Theorem 6.1 on printed page 19, with its interpretation of asymptotic optimality supplied by Corollary 3.3 on printed page 14.

The Erlang-C cost model

Customers arrive at rate $\lambda>0$ and receive exponential service at rate $\mu>0$ per server. The service rate $\mu$ is fixed as $\lambda$ grows. For an integer number of servers $N>\lambda/\mu$, the Erlang-C delay probability $\pi(N,\lambda/\mu)$ is the explicit finite-sum expression in Section 2 of the report. A customer who waits has an exponential waiting time with rate $N\mu-\lambda$. Let $D_\lambda(t)$ be the cost of a wait of length $t$. It is strictly increasing on $t\ge0$, satisfies $D_\lambda(0)=0$, and has finite exponential expectation at every positive rate. The resulting conditional waiting cost is

$$G(N,\lambda)=(N\mu-\lambda)\int_0^\infty D_\lambda(t)e^{-(N\mu-\lambda)t}\,dt.$$

The staffing cost $F(N)$ is one fixed, convex, strictly increasing function of the server count. Its continuous extension is evaluated at real $N>0$. Total cost per unit of time at a stable integer level is

$$C(N,\lambda)=F(N)+\lambda\pi(N,\lambda/\mu)G(N,\lambda).$$

Write $N^*_\lambda$ for any minimizing stable integer level. Ties are permitted. For a positive real offset $x$, define $N_\lambda(x)=\lambda/\mu+x\sqrt{\lambda/\mu}$, $F_\lambda(x)=F(N_\lambda(x))-F(\lambda/\mu)$, and $G_\lambda(x)=\lambda G(N_\lambda(x),\lambda)$. The report extends Erlang-C continuously to $\pi_\lambda(x)$ and writes the incremental continuous objective as $C_\lambda(x)=F_\lambda(x)+\pi_\lambda(x)G_\lambda(x)$. These definitions and the integer-extension identity are from Section 3, printed pages 11–12.

Formalization targets

The report defines the efficiency-driven regime by

$$\text{for every }\kappa>0,\qquad \lim_{\lambda\to\infty}\frac{F_\lambda(\kappa)}{G_\lambda(\kappa)}=+\infty.$$

For each $\lambda>0$, choose $y^*_\lambda>0$ to minimize $F_\lambda(y)+G_\lambda(y)$ over $y>0$. Let $S_\lambda(y)$ be the smaller cost of the stable integer levels immediately below and above $N_\lambda(y)$; if the lower one is unstable, use the upper one. The goal, Theorem 6.1 together with Corollary 3.3, is

$$\lim_{\lambda\to\infty} \frac{S_\lambda(y^*_\lambda)-F(\lambda/\mu)} {C(N^*_\lambda,\lambda)-F(\lambda/\mu)}=1.$$

The milestone path includes the convexity of the conditional waiting cost (Lemma C.1), the agreement of the continuous Erlang-C extension with its integer formula, the two approximation lemmas and their corollary (Lemmas 3.1–3.2 and Corollary 3.3), the convex staffing-cost comparison of equation (13), and all three clauses of the Halfin–Whitt limit in Lemma 4.1. This ordering follows the objects each later statement uses.

What the result gives

The theorem certifies a staffing rule defined by a one-variable surrogate rather than the exact Erlang-C probability in the objective. Its guarantee concerns the incremental total cost above the unavoidable baseline $F(\lambda/\mu)$, which is the economically relevant quantity when comparing two near-minimal stable staffing levels. The ratio tends to one, so the theorem is stronger than a claim that the two costs merely have the same growth order. The source also presents other regimes with different surrogates; their conclusions are separate targets in this series.

The paper proves the mathematical theorem. This mission asks for a Lean proof of its closed-form model and the surrounding lemmas. The complete development would make the report's approximation framework reusable for later results that combine a continuous queueing approximation, a surrogate minimizer, and integer rounding. It would also expose the exact assumptions needed to pass between real and integer staffing levels. No machine-checked proof of this report's Theorem 6.1 is claimed here.

Where the difficulty lies

The simple objective replaces the delay probability $\pi_\lambda(y)$ by one. That replacement is accurate near zero offset, but the minimizing offset itself changes with $\lambda$. Pointwise asymptotics at a fixed positive offset do not directly control the value of an objective at its moving minimizer. The proof therefore has to relate the regime assumption to the location of the relevant minimizers before using the Halfin–Whitt limit. Integer rounding introduces another boundary issue: when $N_\lambda(y)$ is just above $\lambda/\mu$, its floor need not be stable, so evaluating the ordinary Erlang-C formula there would compare the target against a meaningless cost. These difficulties are visible already in the statements of Theorem 6.1 and Lemma 3.2.

Formalization scope and conventions

Lean represents $\lambda$, $\mu$, offsets, and costs as real numbers; arrival-rate limits use the real filter at $+\infty$. Staffing counts are natural numbers. The service rate is positive and fixed. A WaitModel packages strict increase and normalization of $D_\lambda$ on nonnegative waits together with integrability against every positive exponential rate. This integrability expresses the report's finiteness assumption for $G$ and prevents a nonintegrable real integral from silently evaluating to zero. The hypotheses on $F$ are convexity and strict increase on positive real staffing levels; $F$ does not depend on $\lambda$.

The report asserts that $G(N,\lambda)$ diverges as $N$ decreases to $\lambda/\mu$, although the stated assumptions permit bounded increasing waiting penalties for which that assertion fails. The goal therefore includes this explicit divergence hypothesis, which also supports existence of the continuous minimizer used in the report's argument. The integer optimum and the surrogate optimum are functions constrained to be minimizers at every positive arrival rate. They cannot be arbitrary choices that make the conclusion vacuous. The continuous optimum appears only in the framework milestones; it is not a hypothesis of Theorem 6.1.

All formulas are total Lean functions. Their values at $\lambda\le0$, unstable integer counts, nonpositive offsets, or invalid parameters to the continuous Erlang-C integral have no queueing interpretation. Every theorem using them constrains its relevant inputs. The definition of $S_\lambda$ ignores an unstable floor and uses the stable ceiling. At a positive offset and arrival rate this ceiling is above offered load. The Gaussian density, its cumulative integral, the hazard rate, and the delay function use the explicit formulas of Section 4; the value of the delay function at zero is the continuous extension needed by Lemma 4.1.

The queue's stochastic construction is outside this mission. The formal objects are the report's cost formulas and asymptotic comparisons, not a continuous-time Markov chain. Useful contributions include proofs of the special-function limit, convexity of conditional waiting cost, the integer-extension identity, and the reusable approximation lemmas. The regime condition is the full limit in equation (23); weakening it to an unrelated boundedness condition would change the theorem.

Selected references

• Sem Borst, Avi Mandelbaum, and Martin I. Reiman, Dimensioning Large Call Centers, CWI Report PNA-R0015, 2000. Report PDF. Theorem 6.1, printed p. 19; Corollary 3.3, printed p. 14; Lemma 4.1, printed p. 15; Lemma C.1, printed p. 40.

Motivation

In stochastic optimization and statistical learning one chooses a parameter $\theta$ from a set $\Theta\subseteq\mathbb R^d$ to make the risk $R(\theta)=\mathbb E_P[\ell(\theta;X)]$ small, having seen only a sample $X_1,\dots,X_n$ from $P$. Generalization bounds suggest trading empirical risk against its standard deviation, but the variance-penalized objective is non-convex even for convex losses. Duchi and Namkoong (arXiv:1610.02581v3) replace it by the robustly regularized risk, the worst-case expected loss over a $\chi^2$-divergence ball around the empirical distribution. This objective is convex whenever $\ell$ is, and it agrees with the variance-penalized objective up to a small error.

When the risk has curvature near its minimizers, empirical risk minimization attains rates faster than $1/\sqrt n$ (Bartlett, Bousquet and Mendelson 2005; Shapiro, Dentcheva and Ruszczyński 2009). Section 4.1 of the paper asks whether minimizers of the robust risk, which carry an extra variance-dependent penalty of order $\sqrt{\rho/n}$, keep these fast rates. Its Theorem 5 answers yes, and does so for approximate minimizers, which is what iterative solvers return.

Setting

A loss $\ell:\mathbb R^d\times\mathcal X\to\mathbb R$ is fixed, with $\ell(\cdot;x)$ convex and $L$-Lipschitz on a convex set $\Theta$ for every $x$, and $\ell(\theta;\cdot)$ integrable. The risk is $R(\theta)=\mathbb E_P[\ell(\theta;X)]$.

For a radius $\rho\ge0$, the $\chi^2$ ball around the empirical distribution $\widehat P_n$ is the set of weight vectors

$$\mathcal P_n=\Big\{p\in\mathbb R^n_+:\tfrac12\|np-\mathbf 1\|_2^2\le\rho,\ \langle\mathbf 1,p\rangle=1\Big\},$$

and the robust risk is $R_n(\theta,\mathcal P_n)=\sup_{p\in\mathcal P_n}\sum_i p_i\,\ell(\theta;X_i)$.

For $\epsilon\ge0$ the $\epsilon$-suboptimal sets of the risk and of the robust risk are

$$S_\star^\epsilon=\{\theta\in\Theta:R(\theta)\le\inf_\Theta R+\epsilon\},\qquad\widehat S_\star^\epsilon=\{\theta\in\Theta:R_n(\theta,\mathcal P_n)\le\inf_\Theta R_n(\cdot,\mathcal P_n)+\epsilon\},$$

with $S_\star=S_\star^0$ the solution set and $\pi_{S_\star}$ the Euclidean projection onto it. The risk satisfies a growth condition of order $\gamma>1$ if, for some $\lambda>0$ and $r>0$,

$$R(\theta)-\inf_\Theta R\ \ge\ \lambda\,\mathrm{dist}(\theta,S_\star)^\gamma\quad\text{whenever }\mathrm{dist}(\theta,S_\star)\le r.\tag{26}$$

The complexity of the problem enters through the localized class $\{x\mapsto\ell(\theta;x)-\ell(\pi_{S_\star}(\theta);x):\theta\in A\}$ and its empirical Rademacher complexity $\mathfrak R_n(A)=\mathbb E_\varepsilon\big[\sup_{\theta\in A}\frac1n\sum_i\varepsilon_i(\ell(\theta;X_i)-\ell(\pi_{S_\star}(\theta);X_i))\big]$, with independent uniform signs $\varepsilon_i\in\{\pm1\}$.

Formalization targets

Goal: Theorem 5 (p. 19)

For $t>0$, $\rho\ge0$, and $0<\epsilon\le\frac12\lambda r^\gamma$ satisfying

$$\epsilon\ge\Big(2\frac{8^\gamma L^\gamma}{\lambda}\Big)^{\frac1{\gamma-1}}\Big(\frac\rho n\Big)^{\frac\gamma{2(\gamma-1)}}\quad\text{and}\quad\frac\epsilon2\ge2\,\mathbb E[\mathfrak R_n(S_\star^{2\epsilon})]+L\Big(\frac{2\epsilon}\lambda\Big)^{\frac1\gamma}\sqrt{\frac{2t}n},\tag{27}$$ $$\mathbb P\big(\widehat S_\star^\epsilon\subset S_\star^{2\epsilon}\big)\ \ge\ 1-e^{-t}.$$

Milestones, in attack order

1. Localization (p. 44). Under (26), $S_\star^{2\epsilon}$ lies in $\{\theta\in\Theta:\mathrm{dist}(\theta,S_\star)\le(2\epsilon/\lambda)^{1/\gamma}\}$.
2. Theorem 1, upper half of (10) (p. 7). $\sup_{p\in\mathcal P_n}\langle p,z\rangle-\bar z\le\sqrt{2\rho s_n^2/n}$ for every $z\in\mathbb R^n$.
3. Claim E.1 (p. 44). If $\widehat S_\star^\epsilon\not\subset S_\star^{2\epsilon}$, the localized deviation $\Delta_n$ plus a variance term reaches $\epsilon$ somewhere on $S_\star^{2\epsilon}$.
4. Display (43) (p. 45). $\mathbb P(\widehat S_\star^\epsilon\not\subset S_\star^{2\epsilon})\le\mathbb P(\sup_{S_\star^{2\epsilon}}\Delta_n\ge\epsilon/2)$.
5. Concentration (p. 45). $\mathbb P(\sup_{S_\star^{2\epsilon}}\Delta_n\ge2\mathbb E[\mathfrak R_n(S_\star^{2\epsilon})]+u)\le\exp(-\frac{nu^2}{2L^2}(\frac\lambda{2\epsilon})^{2/\gamma})$.

Significance

The theorem says that the variance penalty implicit in the robust objective does not cost the fast rates available under curvature. The $\rho$-dependent condition in (27) is of order $(\rho/n)^{\gamma/(2(\gamma-1))}$, which for quadratic growth ($\gamma=2$) is $\rho/n$, the same order as the localized complexity term in typical parametric problems. Corollary 4.1 of the paper derives explicit rates of order $\frac dn\log\frac nd+\frac tn+\frac\rho n$ from it for a unique minimizer. The result applies to $\epsilon$-approximate minimizers, so it covers the output of the stochastic-gradient methods used to solve the robust problem.

The result is proved in the paper (Appendix E). None of it is formalized: no statement about growth conditions, localized deviations of a robust objective, or fast rates for robust minimizers is on Prove2Me. A formal proof would check the printed constants, settle the boundary case $\epsilon=0$ (see below), and produce a localization lemma and a reduction from approximate robust minimizers to empirical processes that apply to other estimators.

Difficulty

The obvious argument fails at two points. First, a uniform deviation bound over all of $\Theta$ gives only the $1/\sqrt n$ rate: the speed-up comes from localizing to $S_\star^{2\epsilon}$, which requires transferring the growth condition, assumed only within distance $r$ of $S_\star$, to every $2\epsilon$-suboptimal point by convexity. Second, the robust risk is not an empirical average, so standard comparisons between empirical and population minimizers do not apply. Claim E.1 handles this by moving along the segment from a bad approximate minimizer to its projection, which needs the projection to be preserved along that segment (a normal-cone property of $\pi_{S_\star}$) and the risk to be continuous there. The robust–empirical gap is then controlled by the variance expansion of Theorem 1. The concentration step needs a bounded-differences inequality for a supremum over an uncountable class, together with symmetrization; neither is in Mathlib in this form.

Formalization scope

Parameters live in EuclideanSpace ℝ (Fin d), so norms, distances and projections are Euclidean. The sample is the coordinate process of the product measure $P^{\otimes n}$ on Fin n → X, $n\ge1$, and probabilities are measures of sample sets (the outer measure for a set that is not measurable). The $\chi^2$ ball is the weight-vector form (8). The suboptimal sets are written without infima ($R(\theta)\le R(\theta')+\epsilon$ for all $\theta'\in\Theta$). Each supremum "$\sup\ge c$" is written as "for every $\delta>0$ some $\theta$ reaches $c-\delta$", so no statement relies on the default value of a real supremum. The Rademacher complexity is the published UnderstandingML.rademacher, and its expectation over the sample is assumed integrable, so that it is the true expectation and not the default value $0$ of a Bochner integral. Lipschitz continuity is required on $\Theta$, as printed.

Corrections and presuppositions:

• $\epsilon>0$. The paper prints $0\le\epsilon$. At $\epsilon=0$, $\rho=0$, both conditions of (27) hold, yet for $\ell(\theta;x)=\frac12(\theta-x)^2$ on $\Theta=[-1,1]$ with $X$ uniform on $[-\frac12,\frac12]$ the robust minimizer is the sample mean, which is almost surely not in $S_\star=\{0\}$. The proof divides by $\epsilon$ (p. 45). The goal is stated for $\epsilon>0$.
• $S_\star$ nonempty and closed are assumed. The projection $\pi_{S_\star}$ presupposes them, and Appendix E calls $S_\star$ closed.
• Only the upper half of Theorem 1's (10) is stated; it needs no boundedness of the values.

The constant $\big(2\cdot8^\gamma L^\gamma/\lambda\big)^{1/(\gamma-1)}$ is the printed one; the proof uses a smaller one, which the printed condition implies. The hypotheses $\epsilon>0$, $\gamma>1$ and $\lambda>0$ make every power well defined. A formalization that assumed (26) vacuously, took $\epsilon=0$, or let the Rademacher term be a non-integrable Bochner integral would trivialize the goal; the statements rule these out.

Infrastructure: Euclidean projection onto closed convex sets and its normal-cone characterization (partly in Mathlib), convexity of integral functionals, McDiarmid's bounded-differences inequality, and symmetrization for suprema of empirical processes. The concentration tools and the localization lemma can be reused beyond this mission. Contributions toward McDiarmid's inequality and symmetrization are especially welcome.

Selected references

• J. C. Duchi and H. Namkoong, Variance-based regularization with convex objectives, arXiv:1610.02581v3, 2017. https://arxiv.org/abs/1610.02581
• P. L. Bartlett, O. Bousquet and S. Mendelson, Local Rademacher complexities, Annals of Statistics 33(4), 2005. https://doi.org/10.1214/009053605000000282
• S. Boucheron, G. Lugosi and P. Massart, Concentration Inequalities: A Nonasymptotic Theory of Independence, Oxford University Press, 2013. https://doi.org/10.1093/acprof:oso/9780199535255.001.0001
• A. Shapiro, D. Dentcheva and A. Ruszczyński, Lectures on Stochastic Programming: Modeling and Theory, SIAM, 2009. https://doi.org/10.1137/1.9780898718751
• A. Maurer and M. Pontil, Empirical Bernstein bounds and sample variance penalization, COLT, 2009. https://arxiv.org/abs/0907.3740

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