Motivation

A Markovian decision process (Howard, 1960) models a controller who, in each of finitely many states, picks a decision, earns a reward and moves to a random next state according to known transition probabilities. In applications (inventory control, equipment replacement, quality control) those probabilities are estimated, not known. Satia and Lave (Operations Research 21(3), 1973) treat the uncertainty in two ways: a game-theoretic formulation, in which each unknown row only lies in a given set, and a Bayesian formulation, going back to Silver (1963) and Martin (1967), in which the controller holds a prior on the unknown matrix and learns from observed transitions.

The Bayesian problem is the natural one but its state includes the whole prior, so it cannot be solved exactly beyond small cases. The paper's contribution in the Bayesian part is a pair of computable bounds on the Bayesian optimal return in terms of the two game-theoretic values (max-max and max-min). This mission formalizes those bounds and the chain of facts they rest on.

Setting

There are $N$ states $i$ and, in state $i$, a finite nonempty set $K_i$ of decisions. A transition $i \to j$ under decision $k$ earns $r^k_{ij}$ and rewards are discounted by $\beta$, $0 \le \beta < 1$. The row $p_i^k = (p^k_{ij})_j$ of transition probabilities is unknown; it is known to lie in a closed convex nonempty set $S_i^k$ of probability vectors, and $S = \{P : p_i^k \in S_i^k \text{ for all } i, k\}$.

A prior $g$ is a probability distribution on matrices $P = (p_i^k)$ whose rows are all probability vectors. Its means are $\bar p^k_{ij} = E(p^k_{ij})$. After a transition $l \to j$ under decision $m$ the prior is replaced by the Bayes transformation $T^m_{lj} g(P) = C\,p^m_{lj}\,g(P)$ (Eq. (8)), with $C$ the normalizing constant. The Bayesian optimal return $f(i,g)$ solves the recursion

$$f(i, g) = \max_{k \in K_i} \Big\{ \sum_j \bar p^k_{ij} r^k_{ij} + \beta \sum_j \bar p^k_{ij} f(j, T^k_{ij} g) \Big\}. \qquad (10)$$

The max-max and max-min values $V^+$, $V^-$ solve

$$V_i^\pm = \max_{k \in K_i} \operatorname*{max/min}_{p_i^k \in S_i^k} \Big\{ \sum_j p^k_{ij} r^k_{ij} + \beta \sum_j p^k_{ij} V_j^\pm \Big\},$$

with max for $V^+$ and min for $V^-$. Finally $\alpha = \operatorname{prob}(P \in S \mid g)$, the prior probability that the true matrix lies in $S$.

The Lean development lives in the namespace SatiaLave.Bayes: UncertainMDP, IsPrior, pbar, bayes, SolvesEq10, SolvesVplus, SolvesVminus, alpha, rmax, rmin, policyValue.

Formalization targets

Goal: Propositions 9 and 10

For every bounded solution $f$ of (10), all solutions $V^+$, $V^-$, every prior $g$ and every state $i$,

$$\alpha V_i^- + (1-\alpha)\min_{i,j,k}\frac{r^k_{ij}}{1-\beta} \;\le\; f(i,g) \;\le\; \alpha V_i^+ + (1-\alpha)\max_{i,j,k}\frac{r^k_{ij}}{1-\beta},$$

together with the existence of $f$, $V^+$ and $V^-$. Both halves are the paper's printed statements.

Milestones

1. Proposition 6 (Martin): (9)/(10) has a unique bounded solution (unique at priors).
2. No learning (p. 733): at a point-mass prior $\delta_P$, $f(\cdot,\delta_P)$ solves the optimality equations of the process with known $P$.
3. Proposition 8: $f(i,g)$ is convex in $g$.
4. Jensen step (proof of Proposition 9): $f(i,g) \le \int f(i,\delta_P)\,dg(P)$.
5. Policy step (proof of Proposition 10): $f(i,g) \ge \int [q + \beta P^A q + \beta^2 [P^A]^2 q + \cdots]_i\,dg(P)$ for every pure stationary policy $A$.

Significance

The result. The bounds sandwich an intractable quantity between two quantities computable by finite algorithms (the max-max and max-min policy-iteration procedures of the same paper), weighted by a single prior probability $\alpha$. When the prior concentrates on $S$ ($\alpha \to 1$) the bounds become $V_i^- \le f(i,g) \le V_i^+$: the Bayesian return lies between the pessimistic and optimistic robust values. They are the upper and lower bounds on the return that the paper's implicit-enumeration method (the decision tree of its Fig. 2 and Proposition 12) uses to compare decisions. The Jensen step is a value-of-information inequality (Bayesian optimal return is at most the expected full-information optimal return), which recurs throughout Bayesian control and bandit theory.

Formalizing it. The results are proved on paper (Propositions 6 and 8 by reference to Martin's book and Satia's thesis, Propositions 9 and 10 in the text); none is machine-checked. The mission produces a Lean model of Bayes-adaptive Markov decision processes with priors as measures, the Bayes transformation and its fixed-point recursion, and the link between the Bayesian and the robust (rectangular) formulations. Martin's existence-uniqueness theorem and the convexity of the Bayesian value are reusable for any Bayes-adaptive model.

Difficulty

The prior space is infinite-dimensional and not a vector space, so the recursion (10) lives on a space of measures, and the usual finite-state arguments do not apply verbatim. Proposition 8 gives convexity only along finite mixtures, while the proof of Proposition 9 applies Jensen's inequality to the integral mixture $g = \int \delta_P\,dg(P)$ of point masses; bridging the two, or proving the value-of-information inequality directly, is the central step. The paper also restricts the point masses to $x_i^k \in S_i^k$, which cannot represent a prior with mass outside $S$; the formal statement integrates over every transition matrix, as the next line of the paper's display requires. Measurability of $P \mapsto f(i,\delta_P)$ is not automatic, since $f$ is only characterized by a functional equation.

Formalization scope

• States are a nonempty Fintype S; decisions a dependent family D i of nonempty finite types. A matrix is P : (i : S) → D i → S → ℝ with the product Borel $\sigma$-algebra.
• Priors are measures: a probability measure giving full mass to matrices whose rows are probability vectors. This generalizes the paper's densities $g(P)$ and includes the point masses $a_x$ its proof uses.
• Bayes transformation at $\bar p = 0$: the normalizing constant does not exist; bayes then returns $g$. That posterior is always multiplied by $\bar p = 0$ in (10), so the choice is immaterial.
• Readings of informal words. "The problem reduces to a Markovian decision process" = at a point-mass prior, fixed by every Bayes transformation, $f$ solves the known-$P$ optimality equations. "Convex in $g$" = convex along mixtures of priors. "Unique set of bounded functions" = two bounded solutions agree at every prior (values at non-priors are unconstrained). "Satisfy (9)" is formalized as (10), which the paper derives from (9) by linearity of $E$. $\max_{P\in S}$/$\min_{P\in S}$ in $V^\pm$ is taken over the row $p_i^k \in S_i^k$ (the only row that enters; $S$ is a product), as ⨆/⨅ over a nonempty bounded set. "Obviously $f(i,g)\ge V_i^A$" is stated for every pure stationary policy $A$, not only a max-min optimal one. The policy return is the componentwise series $\sum_n \beta^n (P^A)^n q$.
• Added hypotheses, not printed: $0 \le \beta < 1$; $S_i^k \ne \emptyset$; $N \ge 1$. Printed and kept: $S_i^k$ closed and convex.
• $f$, $V^+$, $V^-$ are quantified as solutions of their equations; $\alpha$ is computed from $g$, never a free parameter; $\max_{i,j,k}[r^k_{ij}/(1-\beta)]$ ranges over all states $i,j$ and $k \in K_i$. Integrability of the integrands in milestones 4 and 5 is part of their conclusions.
• Trivializations ruled out. A free $\alpha \in [0,1]$, or $f$ defined off priors, would make the goal false or vacuous; the goal also asserts that bounded $f$ and $V^\pm$ exist, so its universal part is not vacuous.
• Not in scope: Proposition 7 (matrix-beta conjugacy, which needs a Dirichlet distribution), Propositions 11–13 and the numerical example.

Welcome contributions: the Banach fixed-point argument for (10) on bounded functions of priors; lemmas that bayes maps priors to priors and that point masses are fixed; continuity of the known-$P$ optimal value in $P$; a general Jensen inequality for functions convex along mixtures of probability measures.

Selected references

• J. K. Satia and R. E. Lave, Jr., Markovian Decision Processes with Uncertain Transition Probabilities, Operations Research 21(3), 728–740, 1973. https://doi.org/10.1287/opre.21.3.728
• J. J. Martin, Bayesian Decision Problems and Markov Chains, Wiley, New York, 1967.
• E. A. Silver, Markovian Decision Processes with Uncertain Transition Probabilities or Rewards, Interim Technical Report No. 1, Operations Research Center, Massachusetts Institute of Technology, August 1963.
• R. A. Howard, Dynamic Programming and Markov Processes, MIT Press, 1960.
• J. K. Satia, Markovian Decision Process with Uncertain Transition Matrices or/and Probabilistic Observation of States, Ph.D. dissertation, Stanford University, 1968.

Motivation

A maximal independent set (MIS) of a graph is a set of pairwise non-adjacent vertices to which no further vertex can be added. Sequentially an MIS is found greedily in linear time, but the greedy scan is inherently serial. Whether an MIS can be computed by a fast parallel algorithm was a central question of parallel complexity in the early 1980s: Karp and Wigderson gave the first NC algorithm (STOC 1984), and Luby's paper, SIAM J. Comput. 15(4):1036–1053, 1986, gave a much simpler one. MIS is a subroutine of many parallel and distributed graph algorithms (colouring, matching, symmetry breaking), and Luby's randomized algorithm remains the standard one in distributed computing.

The paper's second contribution, the subject of this mission, is a general method for removing randomness: analyse the randomized algorithm under pairwise independence only, then realize pairwise independent random variables on a sample space of polynomial size and try every sample point in parallel. The same method, often attributed jointly to Luby (1986) and to Alon, Babai and Itai (J. Algorithms 7, 1986), became a standard tool of derandomization.

Setting

Let $G = (V, E)$ be a finite simple graph with $n = |V|$ vertices labelled $0, \dots, n-1$. The algorithm keeps a set $I$ (initially empty) and the current graph $G' = (V', E')$, the subgraph of $G$ induced on $V'$ (initially $V' = V$). For $W \subseteq V'$ the neighbourhood is $N(W) = \{ i \in V' : \exists j \in W, (i,j) \in E' \}$. Each execution of the loop body selects an independent set $I' \subseteq V'$, adds it to $I$, and deletes $I' \cup N(I')$ from $V'$; the loop runs while $V' \ne \emptyset$. Write $d(i)$ for the degree of $i$ in $G'$, $Y_k$ for the number of edges of $G'$ before the $k$-th execution, and $\mathrm{sum}(i) = \sum_{j \in \mathrm{adj}(i)} 1/d(j)$.

Algorithm B's select step draws a coin $\mathrm{coin}(i) \in \{0,1\}$ for each vertex, with $\Pr[\mathrm{coin}(i) = 1] = 1/2d(i)$, puts $X = \{ i : \mathrm{coin}(i) = 1 \}$, and removes from $X$ the endpoint of smaller degree of every edge inside $X$ (both endpoints on a tie).

The sample space. Fix a prime $q$ with $n \le q \le 2n$. The sample points are the pairs $(x, y)$ with $0 \le x, y \le q-1$, each of probability $1/q^2$. With $n(i) = \lfloor q/2d(i) \rfloor$, the coin of vertex $i$ at $(x,y)$ is $1$ iff $(x + y \cdot i) \bmod q < n(i)$, so $\Pr[\mathrm{coin}(i) = 1] = p'_i = \lfloor q/2d(i) \rfloor / q$, and distinct coins are pairwise independent.

Algorithm D. Each execution of the loop body first moves the isolated vertices of $G'$ into $I$. Then:

• Case 1. If a vertex $i$ of maximum degree has $d(i) \ge n/16$, it joins $I$, and $\{i\} \cup N(\{i\})$ is deleted.
• Case 2. Otherwise all $q^2$ sample points are tried, the one whose coins make Algorithm B's select step eliminate the most edges is kept, and its $I'$ is used.

No random bits are used.

Formalization targets

Goal: the round bound and correctness of Algorithm D

For every graph $G$ on $n$ vertices, every prime $q$ with $n \le q \le 2n$, and every run of Algorithm D (every tie-break among maximum-degree vertices and every maximizing sample point), the loop body is executed exactly $k$ times, with

$$k \ \le\ \frac{\log(n^2)}{\log(18/17)} + 16 \ \le\ 25 \cdot \log_2 n + 16,$$

and the output $I$ is a maximal independent set of $G$.

Milestones

1. The sample space: Lemma 1, $\Pr[X_i = R_j] = n_{ij}/q$, and Lemma 2, $\Pr[X_i = R_j, X_{i'} = R_{j'}] = n_{ij} n_{i'j'}/q^2$ for $i \ne i'$.
2. The Technical Lemma: for $p_1 \ge \dots \ge p_n \ge 0$ and $c > 0$, $\max_l (\alpha_l - c\beta_l) \ge \tfrac12 \min\{\alpha_n, 1/c\}$.
3. The two steps of the proof of Theorem 1: $E[Y_k - Y_{k+1}] \ge \tfrac12 \sum_i d(i) \Pr[i \in N(I')]$, and $\tfrac12 \sum_{\mathrm{sum}(i) \le 2} d(i)\,\mathrm{sum}(i) + \sum_{\mathrm{sum}(i) > 2} d(i) \ge |E'|$.
4. Lemma C and Theorem 2: with pairwise independent coins of law $1/2d(i)$,

$$\Pr[i \in N(I')] \ge \tfrac18 \min\{\mathrm{sum}(i), 1\}, \qquad E[Y_k - Y_{k+1}] \ge \tfrac{1}{16} Y_k .$$

5. The rounding bound $\tfrac89 p_i \le p'_i \le p_i$ when $d(i) < n/16$.
6. Lemma D and Theorem 3: with pairwise independent coins of law $p'_i$ and all $d(i) < n/16$,

$$\Pr[i \in N(I')] \ge \tfrac19 \min\{\mathrm{sum}(i), 1\}, \qquad E[Y_k - Y_{k+1}] \ge \tfrac{1}{18} Y_k .$$

7. In Case 2 some sample point eliminates at least $1/18$ of the edges; Case 1 occurs at most 16 times in any run before it terminates.

Significance

The goal is the deterministic half of Luby's result: an MIS is computed in $O(\log n)$ parallel rounds with no randomness, which places MIS in deterministic NC. The pairwise-independent analysis (Lemmas C, D, Theorems 2, 3) is the reusable part: it shows that the Monte Carlo algorithm's progress guarantee survives when mutual independence is weakened to pairwise independence, which is what makes a sample space of size $q^2 = O(n^2)$ sufficient. Lemmas 1 and 2 are the standard construction of pairwise independent variables with prescribed rational marginals.

All of these results are proved in the paper. None is formalized on the platform. A related but different object is the platform's dot-product hash family (AlmostLossless.pairwiseIndependent_dotHash), which has uniform marginals over a field and is not the $q^2$-point matrix space with prescribed marginals $n_{ij}/q$. The companion mission A Simple Parallel Algorithm for the Maximal Independent Set Problem I formalizes Theorem 1, the mutually independent analysis of Algorithms A and B.

Difficulty

The obvious route to Theorem 2 repeats the proof of Lemma B, which lower-bounds $\Pr[i \in N(I')]$ by a product over independent events. Under pairwise independence the probability of an intersection of three or more coin events is not determined by the marginals, so that product argument fails, and the constant degrades from $\tfrac18$ to $\tfrac1{16}$.

The round bound needs a separate argument for high-degree vertices. The rounded probabilities $p'_i$ are close to $p_i$ only when $q/2d(i)$ is large, which is why vertices of degree at least $n/16$ are handled by Case 1. Counting the Case 1 rounds uses the vertex count $n$ of the original graph, not of the current one. Correctness at termination requires an invariant linking $I$, $V'$ and $G$ across both kinds of rounds and the deletion of isolated vertices.

Formalization scope

Vertices are Fin n with labels $0, \dots, n-1$, which is §4.2's indexing of $X_0, \dots, X_{n-1}$; the label enters $\mathbb{Z}/q\mathbb{Z}$ as a residue, and labels are distinct mod $q$ because $n \le q$. The current graph is the induced subgraph kept on the full vertex type, with deleted vertices isolated. One execution of the loop body is a relation between states $(I, V')$ that leaves the maximizing vertex (Case 1) and the maximizing sample point (Case 2) free, as the page does, and a run is any sequence of states starting at $(\emptyset, V)$ that follows the relation while $V' \ne \emptyset$. The goal asks for the first index $k$ with $V' = \emptyset$, so a statement about a later state or a bound on $k$ without termination does not meet it.

The conditions $d(i) \ge n/16$ and $d(i) < n/16$ are encoded exactly as $n \le 16\,d(i)$ and $16\,d(i) < n$ in $\mathbb{N}$. $\lfloor q/2d(i) \rfloor$ is natural-number division. The printed code tests $(x + y\cdot i) \bmod q \le n(i)$, which puts $n(i) + 1$ residues in $X$ and contradicts $p'_i = \lfloor p_i q \rfloor / q$ stated on the same page; the formalization uses the strict test.

Lemmas C, D and Theorems 2, 3 quantify over every probability space carrying measurable, pairwise independent (IndepFun for each pair of distinct vertices) coins with the stated marginals at vertices of positive degree. Replacing pairwise by mutual independence, or fixing the probability space, would weaken them. They are stated for a fixed current graph, that is, as the expectation conditional on the state before the round, which is what their proofs establish. Expectations are Bochner integrals of a function with finitely many values and are therefore genuine. Lemma 2 carries the hypothesis $i \ne i'$, implicit on the page.

The development needs the induced subgraph and degree bookkeeping from Mathlib's SimpleGraph, pairwise independence from ProbabilityTheory.IndepFun, finite counting in ZMod q, and real logarithms. The pairwise-independent analysis (Lemma C to Theorem 3) and the sample-space lemmas are reusable beyond this mission. Contributions to any milestone are welcome.

Selected references

• M. Luby, A Simple Parallel Algorithm for the Maximal Independent Set Problem, SIAM J. Comput. 15(4):1036–1053, 1986. https://doi.org/10.1137/0215074
• R. M. Karp and A. Wigderson, A Fast Parallel Algorithm for the Maximal Independent Set Problem, J. ACM 32(4):762–773, 1985. https://doi.org/10.1145/4221.4226
• N. Alon, L. Babai and A. Itai, A Fast and Simple Randomized Parallel Algorithm for the Maximal Independent Set Problem, J. Algorithms 7(4):567–583, 1986. https://doi.org/10.1016/0196-6774(86)90019-2

Motivation

A maximal independent set (MIS) of a graph is a set of vertices, no two adjacent, to which no further vertex can be added. Sequentially an MIS is found greedily in linear time, but the greedy scan is inherently serial. Whether an MIS can be found fast in parallel was a central question of parallel complexity in the early 1980s: an MIS algorithm is a subroutine for maximal matching, vertex colouring with $\Delta + 1$ colours, and many other symmetry-breaking tasks.

• Karp and Wigderson (STOC 1984; J. ACM 32, 1985) gave the first fast parallel algorithms for MIS: a randomized one and a deterministic one, both with running time $O((\log n)^4)$, placing MIS in NC$^4$.
• Luby (SIAM J. Comput. 15(4), 1986) gave the Monte Carlo algorithms analysed in this mission, together with a derandomization that yields a deterministic EREW P-RAM algorithm with $O((\log n)^2)$ running time, placing MIS in NC$^2$. Alon, Babai and Itai (J. Algorithms 7, 1986) independently found a Monte Carlo algorithm similar to Algorithm B.

Luby's algorithm is the standard textbook example of a randomized parallel algorithm and remains the basis of distributed MIS algorithms in the LOCAL model. Its analysis rests on one statement, Theorem 1 of the paper, which this mission formalizes.

Setting

All algorithms in the paper run the same loop on a finite simple undirected input graph $G = (V, E)$ with $n = |V|$ vertices. The current graph is $G' = (V', E')$, initially $G$. For $W \subseteq V'$ the neighbourhood is $N(W) = \{ i \in V' : \exists j \in W,\ (i,j) \in E' \}$. One execution of the loop body selects a set $I' \subseteq V'$ independent in $G'$, adds it to the output, and replaces $G'$ by the subgraph induced on $V' - (I' \cup N(I'))$. The loop stops when $G'$ is empty.

For $i \in V'$ write $\mathrm{adj}(i)$ for its neighbours and $d(i) = |\mathrm{adj}(i)|$ for its degree. The two Monte Carlo select steps are:

• Algorithm A. Every vertex draws a priority $\pi(i)$ uniformly from $\{1, \dots, n^4\}$, independently. A vertex enters $I'$ when its priority is strictly smaller than the priority of each of its neighbours.
• Algorithm B. Every vertex independently sets $\mathrm{coin}(i) = 1$ with probability $1/(2d(i))$, or always if $d(i) = 0$. Let $X$ be the set of vertices with coin $1$. A vertex of $X$ enters $I'$ when each of its neighbours in $X$ has strictly smaller degree.

Let $Y_k$ be the number of edges of $E'$ before the $k$-th execution of the loop body. The number of edges eliminated by that execution is $Y_k - Y_{k+1}$: exactly the edges of $G'$ with at least one endpoint in $I' \cup N(I')$. For $d(i) \ge 1$ the paper uses the weight $\mathrm{sum}(i) = \sum_{j \in \mathrm{adj}(i)} 1/d(j)$.

Formalization targets

Goal: Theorem 1

For the current graph $G'$ and $n \ge \max(1, |V'|)$,

$$E\big[Y_k^A - Y_{k+1}^A\big] \ge \tfrac18\, Y_k^A - \tfrac1{16}, \qquad E\big[Y_k^B - Y_{k+1}^B\big] \ge \tfrac18\, Y_k^B .$$

The constants are those printed in the paper. No connectivity, degree or size condition on $G'$ is assumed.

Milestones

1. §3.2, p. 1040. The priorities of Algorithm A are pairwise distinct with probability at least $1 - 1/(2n^2)$.
2. TECHNICAL LEMMA, p. 1043. For $p_1 \ge \dots \ge p_n \ge 0$ and $c > 0$, with $\alpha_l = \sum_{j \le l} p_j$, $\beta_l = \sum_{j < k \le l} p_j p_k$ and $\gamma_l = \alpha_l - c\beta_l$,

$$\max_{1 \le l \le n} \gamma_l \ge \tfrac12 \min\{\alpha_n, 1/c\}.$$

3. LEMMA A (Beame), p. 1041. For Algorithm A and $d(i) \ge 1$,

$$\Pr[i \in N(I')] \ge \big[\tfrac14\min\{\mathrm{sum}(i), 1\}\big]\big(1 - \tfrac{1}{2n^2}\big).$$

4. LEMMA B, p. 1042. For Algorithm B and $d(i) \ge 1$,

$$\Pr[i \in N(I')] \ge \tfrac14 \min\{\mathrm{sum}(i)/2, 1\}.$$

5. Proof of Theorem 1, first display, p. 1041. For any random choice of $I'$,

$$E[Y_k - Y_{k+1}] \ge \tfrac12 \sum_i d(i)\Pr[i \in I' \cup N(I')] \ge \tfrac12 \sum_i d(i) \Pr[i \in N(I')].$$

6. Proof of Theorem 1, closing chain, p. 1041.

$$\tfrac12 \sum_{\mathrm{sum}(i) \le 2} d(i)\,\mathrm{sum}(i) + \sum_{\mathrm{sum}(i) > 2} d(i) \ge |E'|.$$

Significance

Theorem 1 says that each round removes, in expectation, a constant fraction of the remaining edges. From it the paper derives that the expected number of rounds of either algorithm is $O(\log n)$, and hence that MIS has a Monte Carlo algorithm running in $O(\log n)$ expected time on a CRCW P-RAM and $O((\log n)^2)$ on an EREW P-RAM with $O(m)$ processors. Algorithm B and the proof of part (2) are also the basis of the paper's deterministic algorithm: the analysis of Lemma B uses only pairwise independence of the coins. The companion mission (A Simple Parallel Algorithm for the Maximal Independent Set Problem II) formalizes that derandomization and reuses the statements of milestones 2, 5 and 6.

The results are proved in the paper and reproduced in textbooks (e.g. Motwani and Raghavan, Randomized Algorithms), but not formalized: no statement of Theorem 1, Lemma A or Lemma B was found on the platform. A formal proof would make the per-round analysis of a standard parallel randomized algorithm reusable. That includes the degree-weighted counting of milestone 6 and the Bonferroni-type bound of the Technical Lemma, both of which recur in later analyses of distributed symmetry breaking.

Difficulty

The obvious argument tries to show that a fixed vertex enters $I'$ with good probability. That fails, because a high-degree vertex rarely wins against all its neighbours. The analysis instead bounds the probability that a vertex is removed, i.e. lands in $N(I')$. This event is a union over neighbours of dependent events, so the first Bonferroni inequality alone does not give a lower bound: the pairwise-intersection terms must be controlled. The union bound can also be very lossy when $\mathrm{sum}(i)$ is large, which is why the conclusion involves a minimum with a constant.

A second obstacle is the passage from vertices to edges: vertices of small $\mathrm{sum}(i)$ can have high degree while contributing little probability. The per-vertex bounds therefore have to be summed with degree weights and redistributed over edges. For Algorithm A there is an additional complication: priorities from $\{1, \dots, n^4\}$ can collide, so the argument about a uniformly random order holds only on the event that $\pi$ is injective. That event appears as the factor $1 - 1/(2n^2)$.

Formalization scope

• Graph. The current graph $G'$ is a SimpleGraph V on a finite type with decidable adjacency, and $V' = V$. The degree is SimpleGraph.degree, $\mathrm{adj}(i)$ is neighborFinset, and $Y_k = |E'|$ is edgeFinset.card.
• Conditional form. Theorem 1 is stated for a fixed current graph $G'$, i.e. conditionally on the first $k - 1$ rounds, as in the paper's proof. The unconditional statement follows by averaging.
• Input size. $n$ is a parameter with $1 \le n$ and $|V'| \le n$. It is not fixed to $|V'|$, which would cover only the first round.
• Select steps. Both endpoints' ALGEDGE runs are applied to every edge, since $E'$ contains each edge in both orientations. Hence Algorithm A keeps $i$ iff $\pi(i) < \pi(j)$ for all neighbours $j$. Algorithm B keeps $i \in X$ iff $d(j) < d(i)$ for all neighbours $j \in X$. Algorithm B's $I'$ starts at $X$; the page leaves $I'$ uninitialized in §3.3, and Algorithm D's code (p. 1047) has $I' \leftarrow X$.
• Laws. Probabilities and expectations are explicit finite sums: uniform over the $(n^4)^{|V|}$ priority vectors, and the product law over the $2^{|V|}$ coin vectors. A coin of an isolated vertex is $1$ with probability $1$, as on the page.
• Milestones. Milestone 5 is stated for an arbitrary finite distribution of $I'$, which contains both algorithms' laws. Milestone 6 divides out the common factor $\tfrac18$ of the printed chain.

Theorem 1 is false for arbitrary distributions of priorities or coins. A formalization that takes "Pr" as an unconstrained parameter, conditions on the event of interest, or replaces $n$ by $|V'|$ does not state the paper's theorem.

A complete development needs finite product probability spaces, inclusion–exclusion (Bonferroni) inequalities for finite unions, the symmetry of uniform priorities conditioned on injectivity, and degree-sum identities (SimpleGraph.sum_degrees_eq_twice_card_edges). The Technical Lemma and milestones 5 and 6 are reusable beyond this mission. Proofs of any milestone, and alternative proofs of Lemmas A and B, are welcome.

Selected references

• M. Luby, A Simple Parallel Algorithm for the Maximal Independent Set Problem, SIAM J. Comput. 15(4):1036–1053, 1986. https://doi.org/10.1137/0215074
• R. M. Karp and A. Wigderson, A Fast Parallel Algorithm for the Maximal Independent Set Problem, J. ACM 32(4):762–773, 1985. https://doi.org/10.1145/4221.4226
• N. Alon, L. Babai and A. Itai, A Fast and Simple Randomized Parallel Algorithm for the Maximal Independent Set Problem, J. Algorithms 7(4):567–583, 1986. https://doi.org/10.1016/0196-6774(86)90019-2
• R. Motwani and P. Raghavan, Randomized Algorithms, Cambridge University Press, 1995. https://doi.org/10.1017/CBO9780511814075

Motivation

Where to hold safety stock in a multi-stage supply chain is a basic question of inventory planning. Graves and Willems (MSOM 2(1), 2000) optimize safety-stock placement under the guaranteed-service assumption: each stage quotes a service time to its customers and always meets it. That assumption makes the placement problem tractable, and it is the basis of the dynamic program in the body of the paper and of later work built on it. It also has a price. A stage that promises a service time must hold enough stock to keep the promise even when it would be cheaper to let a downstream stage absorb an occasional delay.

The paper's Appendix measures that price in the simplest setting where it can be computed exactly. The setting is a serial chain in which internal stages promise nothing and only the external customer is guaranteed 100% service. Its one theorem, called the Result, characterizes the optimal base stocks of this relaxed model in closed form. The paper then compares that policy with the guaranteed-service optimum on 36 test instances. The guaranteed-service counterpart of this serial model, Simpson's all-or-nothing property of optimal service times, is on Prove2Me as a separate statement (SupplyChainTheory.gs_all_or_nothing, from Snyder and Shen's textbook). This mission formalizes the other side of the comparison.

Setting

A serial supply chain has $N$ stages. Stage $1$ is the demand node and stage $i$ supplies stage $i-1$ for $i = 2, \dots, N$. Time is discrete, with periods $t \in \mathbb{Z}$. Stage $i$ has a deterministic lead time $T_i \in \mathbb{N}$ and a base stock $B_i \in \mathbb{R}$. It follows a base-stock policy: in each period it observes end-item demand and orders that amount from its supplier.

The end-item demand in period $t$ is $d(t)$. The window demand is $d(a, b] = d(a+1) + \dots + d(b)$, which is $0$ when $a \ge b$. The demand bound $D : \mathbb{N} \to \mathbb{R}$ gives $D(\tau)$, the maximum possible end-item demand over $\tau$ periods, with $D(0) = 0$.

The backlog $Q_i(t)$ is the amount the customer of stage $i$ has ordered but not yet received. It satisfies the recursion (A1):

$$Q_i(t) = \bigl[d(t - T_i, t] + Q_{i+1}(t - T_i) - B_i\bigr]^+, \qquad Q_{N+1} \equiv 0 .$$

Unrolling it gives the closed max-form (A2). The external customer receives 100% service when $Q_1(t) = 0$ for all $t$. When demand never exceeds its bound, this is ensured by the service constraints

$$B_1 + \dots + B_i \ge D(T_1 + \dots + T_i), \qquad i = 1, \dots, N. \tag{A3}$$

Let $h_i$ be the holding cost at stage $i$ and $e_i = h_i - h_{i+1}$ the echelon holding cost. After constant terms are dropped, the expected holding cost gives program $\mathbf P^*$:

$$\min_B\ \sum_{i=1}^N h_i B_i - \sum_{i=2}^N e_{i-1} E[Q_i] \quad\text{s.t. (A3) and } B_i \ge 0 .$$

Demand is random, and $E[Q_i]$ is the expected backlog at stage $i$ in a period $t$.

Formalization targets

Goal: the Result, Eq. (A6)

If the echelon holding costs are nonnegative and $D$ is nondecreasing, then an optimal solution of $\mathbf P^*$ is

$$B_1 = D(T_1), \qquad B_i = D(T_1 + \dots + T_i) - D(T_1 + \dots + T_{i-1}), \quad i = 2, \dots, N. \tag{A6}$$

Formally, (A6) is feasible, and for every period $t$ its objective value is at most that of every feasible vector. The goal names this vector and compares it with every feasible $B$. The weaker claim that "some optimal solution binds all of (A3)" would not be enough.

Milestones

1. Eq. (A2). The closed max-form of $Q_i(t)$, derived from the recursion (A1).
2. Eq. (A3). Under the demand bound $d(a, a+s] \le D(s)$, the constraints (A3) force $Q_1 \equiv 0$ (sufficiency).
3. (A6) is feasible and is the unique binding solution of (A3).
4. Backlog bounds under a transfer. Moving $\Delta \ge 0$ units of base stock from stage $k$ to stage $k+1$ leaves $E[Q_i]$ unchanged for $i > k+1$ and raises it by at most $\Delta$ for $i \le k$. It lowers $E[Q_{k+1}]$ by at most $\Delta$.
5. Eqs. (A7)–(A8). For $k < N$, the transfer that makes the $k$-th constraint binding keeps the vector feasible and does not raise the objective.
6. The case $k = N$. Lowering $B_N$ until the $N$-th constraint binds does not raise the objective.

Significance

The Result shows that, without guaranteed internal service, the optimal base stocks do not depend on the holding costs, provided the echelon costs are nonnegative. Each stage then covers exactly the increment of maximal demand that its own lead time adds. This closed form is the benchmark against which the paper measures the cost of guaranteed service: 26% more safety-stock holding cost on average over its test problems. The paper also remarks, without proof, that Rosling's transformation extends the Result to assembly systems.

The Result is proved in the paper. As far as is known, neither it nor the backlog identity (A2) has been machine-checked. A complete development would yield a verified model of serial base-stock backlogs under bounded demand. It would also verify an exchange argument that recurs in multi-echelon inventory theory: moving stock toward the customer, with echelon costs controlling the sign of the change.

Difficulty

The objective is not linear in $B$. Each $E[Q_i]$ is a convex, nonsmooth function of $B_i, \dots, B_N$ through the maximum in (A2), and the objective subtracts these terms, so $\mathbf P^*$ minimizes a concave function over a polyhedron. The obvious approaches are linear-programming duality and convex first-order optimality conditions on $\mathbf P^*$, and neither applies. The result is a comparison of objective values between arbitrary feasible vectors and (A6). It has to hold pathwise under every demand distribution, and it then has to be carried through expectations. The hypotheses the Result leaves implicit must be recovered from the rest of the paper. Two of them, stated below, are necessary.

Formalization scope

Stages are natural numbers read on the range $\{1, \dots, N\}$. Lead times are natural numbers cast to $\mathbb{Z}$. Base stocks, holding costs and the demand bound are real-valued. A base-stock vector is a function $\mathbb{N} \to \mathbb{R}$, and only indices $1, \dots, N$ are read. The backlog is defined by the recursion (A1), computed in $N + 1 - i$ steps, with $Q_i \equiv 0$ for $i > N$. The closed form (A2) is a theorem. Randomness is a probability space $(\Omega, \mu)$ with a demand path $d(\omega, \cdot)$ whose value in each period is integrable. The integrability of the backlog is not assumed; it follows from the integrability of demand.

The page's informal words are read as follows:

• "The echelon holding costs are nonnegative" means $h_i - h_{i+1} \ge 0$ for $1 \le i < N$, and $h_N \ge 0$, i.e. $e_N \ge 0$ with $h_{N+1} := 0$. The case $k = N$ of the proof uses $h_N \ge 0$. Without it the Result is false ($N = 1$, $h_1 < 0$).
• $D(0) = 0$ is the paper's convention (§2, p. 70) and is added as a hypothesis. Without it (A6) can be infeasible ($D \equiv -1$ is nondecreasing).
• "$D(\,)$ is a nondecreasing function" means Monotone D on $\mathbb{N}$.
• "An optimal solution to $\mathbf P^*$" means feasible, with objective at most that of every feasible vector.
• "$E[Q_i]$" means the expectation of $Q_i(t)$ at a fixed period $t$. Every statement holds for all $t$, and stationarity is not assumed. The paper writes $E[Q_i]$ without $t$ because its demand is stationary, and this reading is at least as strong.
• The demand bound $d(a, a+s] \le D(s)$ appears only in milestone 2. The Result does not use it, so it is not a hypothesis of the goal.
• Eq. (A3) is formalized in the sufficiency direction only. The page's necessity remark ("as we assume that the demand bounds can be realized") is not stated.

A non-integrable backlog would make its Bochner integral $0$ and erase the backlog terms of the objective. The formalization rules this out by assuming integrable demand, which makes the backlogs integrable; it does not assume the backlogs themselves integrable. Out of scope: the spanning-tree dynamic program of §5, the unproved remarks of §§3–4, the Rosling extension, the Kodak application and the computational study.

Useful contributions include a proof of (A2) by downward induction on stages, the integrability of $Q_i(t)$, the pathwise version of milestone 4, and the iteration argument that assembles milestones 3, 5 and 6 into the goal.

Selected references

• S. C. Graves and S. P. Willems, Optimizing Strategic Safety Stock Placement in Supply Chains, Manufacturing & Service Operations Management 2(1):68–83, 2000. https://doi.org/10.1287/msom.2.1.68.23267
• K. F. Simpson, In-Process Inventories, Operations Research 6(6):863–873, 1958. https://doi.org/10.1287/opre.6.6.863
• K. Rosling, Optimal Inventory Policies for Assembly Systems under Random Demands, Operations Research 37(4):565–579, 1989. https://doi.org/10.1287/opre.37.4.565
• L. V. Snyder and Z.-J. M. Shen, Fundamentals of Supply Chain Theory, Wiley, 2nd ed., 2019. https://doi.org/10.1002/9781119584445

Motivation

Many combinatorial optimization problems ask for a subset of a finite ground set that maximizes a set function with diminishing returns: Max Cut and Max Directed Cut in graphs, facility location, maximum entropy sampling, and welfare problems in combinatorial auctions all fit this pattern. The common abstraction is the maximization of a submodular function, the discrete analogue of a concave function. Unlike the monotone case, where the objective only grows as elements are added, the non-monotone problem has no constraint at all and is still NP-hard, since Max Cut is a special case.

For Max Cut and Max Directed Cut, the simplest algorithm there is, putting every vertex on a side by an independent fair coin, already cuts half, respectively a quarter, of the optimum in expectation. Feige, Mirrokni and Vondrák (SIAM J. Comput. 40(4), 2011; extended abstract at FOCS 2007) showed that this is not a feature of cut functions: the same random choice achieves the same factors for every nonnegative submodular function, and for every symmetric one. This mission formalizes that result, Theorem 2.1 of the paper, together with the two sampling lemmas on which it rests. The paper's other results (a nonadaptive 1/3-approximation, deterministic and smoothed local search, and query lower bounds) are the subjects of companion missions in the same series.

Setting

Let $X$ be a finite set with $n = |X|$ elements. A set function assigns a real number $f(S)$ to every subset $S \subseteq X$. It is submodular if

$$f(S \cup T) + f(S \cap T) \le f(S) + f(T) \qquad \text{for all } S, T \subseteq X,$$

equivalently if the marginal value $f(B \cup \{x\}) - f(B)$ of an element $x$ does not increase as the set $B$ grows. It is symmetric if $f(X \setminus S) = f(S)$ for every $S \subseteq X$; the cut function of an undirected graph is the standard example. The optimum is

$$OPT = \max_{S \subseteq X} f(S).$$

For $p \in [0,1]$, $X(p)$ denotes the random subset of $X$ containing each element independently with probability $p$; similarly $A(p)$ is the random subset of a fixed $A \subseteq X$. The Random Set Algorithm (RS) returns $R = X(1/2)$, a uniformly random subset of $X$, without querying $f$. Its expected value is the average of $f$ over all subsets,

$$\mathbf{E}[f(R)] = F(\tfrac12, \dots, \tfrac12) = \frac{1}{2^n} \sum_{S \subseteq X} f(S),$$

where $F(x) = \sum_{S \subseteq X} f(S) \prod_{i \in S} x_i \prod_{i \notin S} (1 - x_i)$ is the multilinear extension of $f$, the expectation of $f$ on a random set that includes element $i$ independently with probability $x_i$.

Formalization targets

Goal: Theorem 2.1

For every nonnegative submodular $f : 2^X \to \mathbb{R}_+$,

$$\mathbf{E}[f(X(1/2))] \ge \tfrac14\, OPT,$$

and if $f$ is in addition symmetric,

$$\mathbf{E}[f(X(1/2))] \ge \tfrac12\, OPT.$$

Both parts form the goal, stated as one theorem. The constants $\tfrac14$ and $\tfrac12$ are exact, not asymptotic, and they are tight: the directed cut of a single arc attains $\tfrac14$, and the cut of a single edge attains $\tfrac12$.

Milestones

1. Lemma 2.2. For submodular $g : 2^X \to \mathbb{R}$, $A \subseteq X$ and $p \in [0,1]$,

$$\mathbf{E}[g(A(p))] \ge (1-p)\, g(\emptyset) + p\, g(A).$$

2. Lemma 2.3. For submodular $f : 2^X \to \mathbb{R}$, sets $A, B \subseteq X$ that need not be disjoint, independent samples $A(p)$, $B(q)$, and $p, q \in [0,1]$,

$$\mathbf{E}[f(A(p) \cup B(q))] \ge (1-p)(1-q) f(\emptyset) + p(1-q) f(A) + (1-p)q f(B) + pq f(A \cup B).$$

3. The display in the proof of Theorem 2.1. For submodular $f : 2^X \to \mathbb{R}$ and every $S \subseteq X$, with $\bar S = X \setminus S$,

$$\mathbf{E}[f(X(1/2))] \ge \tfrac14 f(\emptyset) + \tfrac14 f(S) + \tfrac14 f(\bar S) + \tfrac14 f(X).$$

The milestones need no sign on the function; nonnegativity enters only in the goal.

Significance

The result. Theorem 2.1 gives an algorithm that makes no query at all and is still a constant-factor approximation for unconstrained non-monotone submodular maximization. It sets the baseline that every later algorithm for the problem is measured against: the paper's own nonadaptive $\tfrac13$-algorithm and its local search algorithms with factors $\tfrac13$ and $\tfrac25$, followed by later work culminating in the tight $\tfrac12$-approximation of Buchbinder, Feldman, Naor and Schwartz (FOCS 2012). The paper also shows that $\tfrac14$ is optimal among nonadaptive algorithms required to return one of the queried sets, and that $\tfrac12$ is optimal for symmetric functions among all algorithms using polynomially many value queries, so both factors of Theorem 2.1 have a precise place in the complexity landscape. Lemma 2.3, the probabilistic inequality behind it, is reused in the analyses of the nonadaptive algorithm and of smooth local search.

Formalizing it. The result is proved, with a short proof. What this mission adds is a machine-checked version of the random-set guarantee and of the two sampling lemmas, stated for arbitrary finite ground sets and, for the lemmas, for real-valued submodular functions without a sign. To our knowledge none of these statements has a machine-checked proof; Mathlib has no theory of submodular set functions or of their multilinear extension.

Difficulty

The goal itself is a two-line consequence of the third milestone. The work sits in the lemmas and in one change of viewpoint.

Lemma 2.2 is not a pointwise statement: the random set $A(p)$ can be any subset of $A$, and $g$ can be smaller on it than both $g(\emptyset)$ and $g(A)$. The inequality holds only in expectation, and only because submodularity controls the marginal value of each element uniformly across the sets it can be added to. Lemma 2.3 needs a conditioning argument over two independent samples; the sets $A$ and $B$ may overlap, and on $A \cap B$ the union $A(p) \cup B(q)$ contains an element with probability $1 - (1-p)(1-q)$, so it is not the product distribution with probability $p$ on $A$ and $q$ on $B$. Finally, the third milestone requires identifying the uniform random subset $X(1/2)$ with the union of independent half-samples of $S$ and of its complement, as a statement about finite sums.

The obvious attempt at the goal, comparing $f(R)$ with $f(S^*)$ for an optimal $S^*$ set by set, fails: $f$ is not monotone, so a random set that contains most of $S^*$ may still have small value, and a random set can pick up elements that hurt.

Formalization scope

The ground set is a Lean type X with [Fintype X] [DecidableEq X]; subsets are Finset X and set functions are f : Finset X → ℝ. Submodularity is the lattice inequality of Definition 1.1, not the decreasing-marginals property. Nonnegativity, the paper's standing assumption $f : 2^X \to \mathbb{R}_+$, is the hypothesis ∀ S, 0 ≤ f S; it appears only in the goal. Symmetry is ∀ S, f Sᶜ = f S for all subsets, not only for an optimal one. $OPT$ is Finset.univ.sup' Finset.univ_nonempty f, a maximum over the always nonempty family of all subsets, so it is attained. The ground set may be empty; the goal holds there too and no nonemptiness is assumed.

Expectations are written as exact finite sums, not as integrals. $\mathbf{E}[f(X(1/2))]$ is the multilinear extension F f (fun _ => 1/2). $\mathbf{E}[g(A(p))]$ is $\sum_{T \subseteq A} p^{|T|}(1-p)^{|A \setminus T|} g(T)$, and $\mathbf{E}[f(A(p) \cup B(q))]$ is the double sum over independent samples $S \subseteq A$, $T \subseteq B$ with the product of the two weights. The ranges $0 \le p \le 1$ and $0 \le q \le 1$, implied in the paper by the word "probability", are explicit hypotheses; Lemma 2.2 is false without them.

Trivializing formalizations are excluded: the weights are exactly those of the uniform distribution on all $2^n$ subsets, $OPT$ is the true maximum rather than the value at one fixed set, and $f$ is required to be both nonnegative and submodular.

Reusable infrastructure produced by a complete development: the multilinear extension of a set function and its expression as an expectation, product-weight identities for independent sampling of subsets (including the decomposition of $X(1/2)$ along a set and its complement), and Lemmas 2.2 and 2.3, which the companion missions on the nonadaptive algorithm and on smooth local search also need. Proofs of any milestone are welcome independently.

Selected references

• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing Non-Monotone Submodular Functions, SIAM Journal on Computing 40(4):1133–1153, 2011. https://doi.org/10.1137/090779346
• U. Feige, V. S. Mirrokni, J. Vondrák, Maximizing non-monotone submodular functions, Proceedings of the 48th IEEE Symposium on Foundations of Computer Science (FOCS), 2007, pp. 461–471. https://doi.org/10.1109/FOCS.2007.29
• N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, A Tight Linear Time (1/2)-Approximation for Unconstrained Submodular Maximization, SIAM Journal on Computing 44(5):1384–1402, 2015 (FOCS 2012). https://doi.org/10.1137/130929205
• G. L. Nemhauser, L. A. Wolsey, M. L. Fisher, An analysis of approximations for maximizing submodular set functions — I, Mathematical Programming 14:265–294, 1978. https://doi.org/10.1007/BF01588971

Motivation

A supplier and a retailer who trade a seasonal product must decide who carries the inventory risk: the stock left unsold, or the demand left unserved, when the season ends. With a push contract the retailer orders everything before the season and bears the risk; with a pull contract he orders during the season from the supplier's stock at a single wholesale price, and the supplier bears it. Cachon (Management Science 50(2), 2004) studies the two and the contract between them, the advance-purchase discount, in which units ordered before the season are cheaper than units ordered during it.

In the base model of that paper, shipping a unit during the season costs the same as shipping it before. In practice orders placed during the season are often smaller and more urgent, and shipping and handling them costs more. §5.1 of the paper adds such a cost and asks whether pull contracts remain attractive. Theorem 8 answers that they are then never Pareto efficient: some advance-purchase discount is better for both firms.

Setting

Demand $D$ for the season has law $\mu$ on $\mathbb R$, distribution function $F$ and density $f$. As in §3 of the paper, $F(0) = 0$, $F$ is strictly increasing on $[0,\infty)$, $F' = f$ on $(0,\infty)$, and the generalized failure rate $g(x) = x f(x)/(1 - F(x))$ is strictly increasing (IGFR). The expected sales from $q$ available units are

$$S(q) = q - \int_0^q F(x)\,dx .$$

The retail price is $p$, the unit production cost $c$, the salvage value $v$, with $v < c < p$.

A contract is a pair of wholesale prices $\{w_1, w_2\}$. Before production the retailer submits a prebook order of $y \ge 0$ units at $w_1$. The supplier then produces $q \ge y$. During the season, after running out of prebooked stock, the retailer places at-once orders at $w_2$, filled from the supplier's remaining stock. Pull is $w_1 = w_2 < p$; an advance-purchase discount is $w_1 < w_2$. In §5.1 the supplier pays an extra shipping and handling cost $\tau > 0$ per at-once unit. The profits are

$$\pi_r(y,q) = -(w_1 - v)y + (p - v)S(y) + (p - w_2)\bigl(S(q) - S(y)\bigr),$$ $$\pi_s(y,q) = (w_1 - v)y + (w_2 - \tau - v)\bigl(S(q) - S(y)\bigr) - (c - v)q .$$

A supplier best response to $y$ maximizes $\pi_s(y,\cdot)$ over $q \ge y$. An outcome of $\{w_1, w_2\}$ is a pair $(y, q)$ with $q$ a best response to $y$ and $y \ge 0$ maximizing $\pi_r$ when every alternative prebook is followed by a best response to it.

Formalization targets

Goal: Theorem 8

Fix $w_2 < p$ and $\tau > 0$, and suppose the retailer does not prebook under the pull contract $\{w_2, w_2\}$: $y = 0$ is his unique best reply, followed by the supplier's best response $q_0$. Then there is $w_1$ with

$$c < w_1 < w_2$$

such that $\{w_1, w_2\}$ has an outcome, and every outcome $(y, q)$ of it satisfies

$$\pi_r^{\{w_1,w_2\}}(y,q) > \pi_r^{\{w_2,w_2\}}(0,q_0), \qquad \pi_s^{\{w_1,w_2\}}(y,q) > \pi_s^{\{w_2,w_2\}}(0,q_0).$$

Milestones

1. Eq. (22): for $v < w_1 \le w_2 \le p$ the retailer's profit is concave in $y$ and uniquely maximized at $y_r$ with $F(y_r) = (w_2 - w_1)/(w_2 - v)$, whatever $q$.
2. Eqs. (20)–(21) with $w_2 - \tau$: the supplier's best response to $y$ is $\max\{y, q_s\}$ with $F(q_s) = (w_2 - \tau - c)/(w_2 - \tau - v)$, independent of $w_1$, and $q_s$ is smaller than without the shipping cost.
3. §5.1: for fixed $w_2$ the retailer is never worse off with $w_1 \le w_2$ than with $w_1 = w_2$.
4. $y_r(w_1) > 0$ for every $w_1 < w_2$.
5. The derivative of $w_1 \mapsto \pi_s(y_r(w_1), q)$, where the density at $y_r(w_1)$ is positive:

$$\frac{d\pi_s(y_r(w_1), q)}{dw_1} = y_r(w_1) - \frac{(w_1 - v) - (w_2 - \tau - v)(1 - F(y_r(w_1)))}{(w_2 - v) f(y_r(w_1))}.$$

6. $y_r(w_1) \to 0$ as $w_1 \to w_2$, and, when $f$ has a positive right limit $f(0)$ at $0$, the derivative in 5 tends to $-\tau/((w_2 - v) f(0)) < 0$.

Significance

Without shipping costs, advance-purchase discounts with $w_2 = p$ coordinate the supply chain (Theorem 7 of the paper, the subject of mission 2 of this series), and a pull contract can lie in the Pareto set among push and pull contracts (Theorem 6, mission 1). Theorem 8 shows that the second fact does not survive an at-once shipping cost of any size: pulling inventory during the season incurs a cost the integrated chain would avoid, and a small discount for early commitment shifts part of the stock to the prebook, where it is cheaper to ship. The Pareto set then no longer consists of a single contract type. The result supports the paper's conclusion that each of its three extensions makes push relatively more attractive than pull.

The theorem is proved in the paper, not formalized anywhere. A formal proof requires making precise two points the paper passes over: what "the retailer does not prebook" means when the retailer could switch to a large prebook once a discount is offered, and why no positive density at $0$ is needed. Formalized, the statement also gives a checked account of the prebook game under a two-price contract, reusable for the other extensions of §5.

Difficulty

The paper's argument differentiates the supplier's profit along the retailer's optimal prebook and takes the limit as $w_1 \to w_2$. That limit involves $f(0)$, which the model does not provide: $F$ is differentiable only on $(0, \infty)$, and for gamma demand with shape above $1$ the density vanishes at $0$, so the paper's limit is $-\infty$. A proof of the goal must therefore not rest on the limit display alone.

The second obstacle is the retailer's global choice. The calculus concerns prebooks $y_r(w_1)$ below the supplier's production $q_s$. Once $w_1 < w_2$, the retailer might instead prefer a prebook at least $q_s$, turning the chain into push mode, and the outcome would then not be the one the derivative describes. Ruling this out for $w_1$ close to $w_2$ requires the strict form of the premise and a uniform comparison of the two regimes; it is not a local argument at $y_r$.

Formalization scope

Demand is a probability measure μ on ℝ with F := ProbabilityTheory.cdf μ, and the standing assumptions of §3 form the predicate DemandModel μ f; differentiability of F is required on $(0,\infty)$ only, so the exponential law is admitted. Quantities range over $[0, \infty)$. Best responses and outcomes are defined as maximizers, not by the closed forms of milestones 1 and 2. All profit formulas are those of §4.5 for $w_2 \le p$, and every statement assumes it. The shipping cost enters only the supplier's at-once net revenue $w_2 - \tau$. The prebook function $y_r$ in milestones 5 and 6 is a function pinned on $(v, w_2)$ by Eq. (22), which determines it uniquely.

Readings of the paper's words:

• "the retailer does not prebook when $w_1 = w_2$" is read as "$y = 0$ is the retailer's unique best reply" (every $y > 0$ gives strictly less); with a tie the conclusion can fail;
• "profit increases for both" is read as a strict increase for both firms, in every outcome of the discounted contract;
• the conclusion $c < w_1$ strengthens "advance-purchase discount" ($w_1 < w_2$);
• "reduces the supplier's optimal production" (milestone 2) is a strict decrease; its formula is stated for $c \le w_2 - \tau$;
• "$f(0)$" in milestone 6 is the right limit of $f$ at $0$, assumed positive there only; the positivity of $f(y_r(w_1))$ in milestone 5 is the hypothesis of the implicit-function step;
• "never worse off" (milestone 3) compares every outcome of $\{w_1, w_2\}$ with every outcome of $\{w_2, w_2\}$.

A version of the goal that assumed $f(0) > 0$, assumed $y_r(w_1) < q_s$, compared only one favourably chosen outcome of the discounted contract, or stated either firm's gain with $\ge$, would be weaker than Theorem 8 and is not the target.

A complete development needs the concavity and first-order conditions for $S$, the inverse-function derivative for $F$, and the regime comparison between prebooks below and above $q_s$. The first two are reusable across all newsvendor-type models; contributions proving the milestones in any order are welcome.

Selected references

• G. P. Cachon, The Allocation of Inventory Risk in a Supply Chain: Push, Pull, and Advance-Purchase Discount Contracts, Management Science 50(2):222–238, 2004. https://doi.org/10.1287/mnsc.1030.0190
• M. A. Lariviere, E. L. Porteus, Selling to the Newsvendor: An Analysis of Price-Only Contracts, Manufacturing & Service Operations Management 3(4):293–305, 2001. https://doi.org/10.1287/msom.3.4.293.9971