Optimization

Motivation

Most practical reinforcement-learning methods do not compute value functions exactly. They alternate between estimating a value function from data, usually with a parametric approximator, and acting greedily with respect to that estimate. Approximate value iteration and approximate policy iteration are the two classical schemes of this kind, and their error analysis decides how accuracy in the estimation step translates into quality of the policies produced. Chapter 3 of S. M. Kakade's thesis On the Sample Complexity of Reinforcement Learning (University College London, 2003) collects the basic guarantees, developed from Bertsekas (Dynamic Programming: Deterministic and Stochastic Models, 1987) for greedy policies, Singh and Yee (1994), and Bertsekas and Tsitsiklis, Neuro-Dynamic Programming (Athena Scientific, 1996). The bounds are stated in terms of the worst-case (max-norm) error of the evaluation step, and the thesis uses them to argue that max-norm error is the obstacle to state-space-independent sample complexity results for these methods, which motivates the later chapters of the thesis.

Setting

A finite discounted Markov decision process consists of a finite set of states $S$, a finite nonempty set of actions $A$, a transition kernel $P(s'\mid s,a)$ (for every $(s,a)$ a probability distribution over $S$), a deterministic reward $r(s,a)\in[0,1]$, and a discount factor $0\le\gamma<1$. A policy $\pi(a\mid s)$ is a probability distribution over actions for every state; a deterministic policy is a map $f:S\to A$, identified with the policy that plays $f(s)$ with probability one.

Values are normalized: the value of $\pi$ at $s$ is

$$V_\pi(s)=(1-\gamma)\,\mathbb E\Big[\sum_{t\ge0}\gamma^t r(s_t,a_t)\,\Big|\,\pi,\ s_0=s\Big],$$

and the state-action value is $Q_\pi(s,a)=(1-\gamma)r(s,a)+\gamma\,\mathbb E_{s'\sim P(\cdot\mid s,a)}[V_\pi(s')]$. With rewards in $[0,1]$, every value lies in $[0,1]$. An optimal policy $\pi^*$ has $V_{\pi^*}(s)\ge V_\pi(s)$ for every policy $\pi$ and state $s$; write $V^*=V_{\pi^*}$ and $Q^*=Q_{\pi^*}$. The max norm is $\|x\|_\infty=\max_s|x(s)|$ on state vectors and $\max_{s,a}|x(s,a)|$ on state-action arrays.

The backup operator is $[BJ](s)=\max_a\big((1-\gamma)r(s,a)+\gamma\,\mathbb E_{s'\sim P(\cdot\mid s,a)}[J(s')]\big)$. A deterministic policy $f$ is greedy with respect to $Q$ if $f(s)\in\arg\max_a Q(s,a)$ for every $s$.

• $\gamma$-approximate value iteration produces vectors $J_0=0,J_1,J_2,\dots$ with $\|J_t-BJ_{t-1}\|_\infty\le\varepsilon$, and greedy policies $\pi_t$ for the lookahead $(1-\gamma)r(s,a)+\gamma\,\mathbb E_{s'}[J_t(s')]$.
• $\gamma$-approximate policy iteration starts from any deterministic $\pi_0$, forms an estimate $\tilde Q_t$ of $Q_{\pi_t}$ with $\|\tilde Q_t-Q_{\pi_t}\|_\infty\le\varepsilon$, and takes $\pi_{t+1}$ greedy with respect to $\tilde Q_t$.

Formalization targets

Goal: Theorem 3.2.2 (approximate policy iteration)

$$\limsup_{t\to\infty}\|V^*-V_{\pi_t}\|_\infty\le\frac{2\varepsilon}{(1-\gamma)^2}.$$

The policies need not converge; the statement bounds where they end up.

Milestones

• Theorem 3.1.1: if $\|\tilde Q-Q^*\|_\infty\le\varepsilon$ and $\pi$ is greedy for $\tilde Q$, then $V_\pi(s)\ge V^*(s)-\frac{2\varepsilon}{1-\gamma}$ for all $s$.
• Lemma 3.2.3: $\|V^*-V_{\pi_{t+1}}\|_\infty\le\gamma\|V^*-V_{\pi_t}\|_\infty+\frac{2\varepsilon}{1-\gamma}$.
• Rate of approximate policy iteration (p. 41): $\|V^*-V_{\pi_t}\|_\infty\le\gamma^t+\frac{2\varepsilon}{(1-\gamma)^2}$.
• Contraction of the backup (p. 26): $\|BJ-BJ'\|_\infty\le\gamma\|J-J'\|_\infty$.
• Approximate value iteration (p. 40): $\|V^*-J_t\|_\infty\le\gamma^t+\frac{\varepsilon}{1-\gamma}$.
• Rate of approximate value iteration (p. 41): $\|V^*-V_{\pi_t}\|_\infty\le\frac{2\gamma^t}{1-\gamma}+\frac{2\varepsilon}{(1-\gamma)^2}$.
• Theorem 3.2.1: the same lim sup bound $\frac{2\varepsilon}{(1-\gamma)^2}$ for approximate value iteration.

Significance

The results give the standard performance guarantee for greedy approximate dynamic programming: an evaluation error of $\varepsilon$ in max norm costs at most $2\varepsilon/(1-\gamma)^2$ in max-norm suboptimality, uniformly over the asymptotic set of policies, with a geometric rate of approach. Example 3.1.2 of the thesis shows that the factor $2\varepsilon/(1-\gamma)$ of Theorem 3.1.1 is attained, so the greedy step itself cannot be improved; the two factors of the horizon $1/(1-\gamma)$ in the limit bound are the reason the thesis turns to other error measures in later chapters.

All the statements are classical and proved in the literature (Bertsekas–Tsitsiklis 1996, Chapter 6, in the unnormalized model and with a factor $\gamma$ to spare in the limit bounds); Lemma 3.2.3 and Theorem 3.2.2 are stated in the thesis without proof. To our knowledge none has a machine-checked proof. The mission produces formal proofs in the normalized model shared with the formalization of Kakade–Langford (2002) on this platform, so later chapters of the series (conservative policy iteration, policy search) can compare against them.

Difficulty

Approximate policy iteration is not monotone: with evaluation errors, $V_{\pi_{t+1}}$ can be worse than $V_{\pi_t}$ at some states, so the argument of exact policy iteration, which uses $V_{\pi_{t+1}}\ge V_{\pi_t}$ everywhere, does not apply. The difficulty of Lemma 3.2.3 is to control the distance to optimality without improvement at each step, combining the greedy step with the lack of monotonicity of the new policy's value; the thesis calls the proof of Theorem 3.2.2 "somewhat technical" and omits it. A second, mechanical difficulty is that the normalized value $V_\pi$ is defined as an infinite series, so its Bellman equation $V_\pi(s)=Q_\pi(s,\pi(s))$, the optimality equation $V^*=BV^*$ and the bound $0\le V_\pi\le1$ have to be derived from that definition before any of the recursions can be run.

Formalization scope

• The model is the published normalized model ApproxOptRL.Shared.Model: value P r γ π is $V_\pi$ (defined as $(1-\gamma)$ times a tsum), qValue is $Q_\pi$. $S$ and $A$ are finite types, $A$ nonempty; $P$ satisfies IsTransitionKernel; every statement assumes $0\le r\le1$ and $0\le\gamma<1$.
• The optimal policy is a binder $\pi^*$ with IsOptimalPolicy P r γ πstar (a stationary stochastic policy dominating every stationary stochastic policy at every state). Such a policy exists for every finite MDP (p. 26 of the thesis), and for finite MDPs it is optimal among all policies.
• Policies of the runs are deterministic, S → A, and are evaluated through the indicator policy detPolicy. "Greedy" is the relation ∀ s a, Q s a ≤ Q s (f s): every tie-breaking rule is covered.
• The runs are sequences indexed by ℕ, with the greedy and accuracy conditions as hypotheses at every index; the value-iteration condition is written for indices $t+1$ and $t$.
• $\|\cdot\|_\infty$ is Mathlib's sup norm on S → ℝ and S → A → ℝ.
• The lim sup statements are in $\varepsilon$–$N$ form: for every $\delta>0$ the bound plus $\delta$ holds eventually.
• Ruled out: the accuracy hypothesis is stated against $Q_{\pi_t}$, the value of the current policy, not against $Q^*$, and the greedy relation genuinely constrains $\pi_{t+1}$; with either changed, the hypotheses would be unsatisfiable or the policies unconstrained and the theorem empty.
• Infrastructure needed and reusable beyond this mission: the Bellman equation of the normalized value for indicator policies, $V^*=BV^*$, monotonicity and contraction of policy-evaluation and backup operators in the normalized model, and the bound $0\le V_\pi\le1$. Contributions of these lemmas are welcome.

Selected references

• S. M. Kakade, On the Sample Complexity of Reinforcement Learning, PhD thesis, Gatsby Computational Neuroscience Unit, University College London, 2003. https://discovery.ucl.ac.uk/id/eprint/10100726/
• D. P. Bertsekas and J. N. Tsitsiklis, Neuro-Dynamic Programming, Athena Scientific, 1996. ISBN 1-886529-10-8.
• S. P. Singh and R. C. Yee, An upper bound on the loss from approximate optimal-value functions, Machine Learning 16 (1994), 227–233. https://doi.org/10.1007/BF00993104
• S. M. Kakade and J. Langford, Approximately optimal approximate reinforcement learning, ICML 2002. https://dl.acm.org/doi/10.5555/645531.656005

Motivation

At a busy airport the runway is the bottleneck, and the order in which aircraft land or take off determines how much of its capacity is used. Wake turbulence forces a minimum time between consecutive operations that depends on the weight classes of the leading and trailing aircraft, so reordering a first-come-first-served (FCFS) queue can increase throughput or reduce delay. Controllers cannot reorder freely: constrained position shifting (CPS), introduced by Dear (1976, MIT Flight Transportation Laboratory Report R76-9), allows each aircraft to move at most $k$ positions from its FCFS position, which keeps the sequence fair and predictable.

Balakrishnan and Chandran (Oper. Res. 58(6), 2010) cast CPS scheduling as dynamic programming on a layered network whose paths are the admissible sequences. For makespan and total delay the separations are assumed to satisfy the triangle inequality, which holds for arrivals only or departures only. When arrivals and departures share a runway it fails: in the separation table of the paper, a heavy arrival followed by a departure and then a small arrival needs only $75+60=135$ seconds through the departure, while the direct requirement is $196$ seconds. Section 6.2 of the paper handles this case for arbitrary per-aircraft cost functions, by expanding the network state. This mission formalizes that construction and its correctness.

Setting

Time is discrete: all data are integer multiples of one period. There are $n$ aircraft labelled in FCFS order, a maximum shift $k$, a minimum separation $\delta_{ab}\in\mathbb N$ between a leading aircraft $a$ and a trailing aircraft $b$, a time window $[e_a,l_a]$ for each aircraft, a finite set of precedence pairs $(x,y)$ ($x$ lands before $y$), and a cost $c_a(t)$ of landing aircraft $a$ at period $t$.

A $k$-CPS sequence is a bijection $\sigma$ from positions to aircraft with $|\sigma(p)-p|\le k$. A feasible schedule is a $k$-CPS sequence with integer landing times $t_p$ such that precedence pairs are respected, $e_{\sigma(p)}\le t_p\le l_{\sigma(p)}$, and

$$t_q-t_p\ \ge\ \delta_{\sigma(p)\sigma(q)}\qquad\text{for all positions } p<q .$$

Its cost is $\sum_p c_{\sigma(p)}(t_p)$.

The CPS network has stages $1,\dots,n$. A node of stage $p$ is a list of $\min\{2k+1,p\}$ distinct aircraft that may occupy positions $p-\min\{2k+1,p\}+1,\dots,p$; its last aircraft is the final aircraft $\mathrm{fin}(i)$. An arc joins consecutive stages when the lists overlap. Removing the nodes that violate a precedence pair gives the network $G$. For a node $i$, $\Gamma(i)$ is the set of integer times in the window of $\mathrm{fin}(i)$.

The modified network of §6.2 has nodes $(i,t,d)$: a node $i$ of $G$, a time $t\in\Gamma(i)$, and a lower bound $d$ on the separation between $\mathrm{fin}(i)$ and its predecessor, with $d=0$ at stage $1$ and otherwise $d^{\min}_i\le d\le d^{\max}_i$, where, for the penultimate and final aircraft $a,b$ of $i$,

$$d^{\min}_i=\delta_{ab},\qquad d^{\max}_i=\max\Big\{\max_{j:\,i\in P(j)}\big(\delta_{a,\mathrm{fin}(j)}-\delta_{b,\mathrm{fin}(j)}\big),\ d^{\min}_i\Big\}.$$

An arc $(i,t',d')\to(j,t'',d'')$ requires an arc $(i,j)$ of $G$, $t''-t'\ge d^{\min}_j$, $d''=\min\{t''-t',d^{\max}_j\}$, and $d'+t''-t'$ at least the separation between the penultimate aircraft of $i$ and $\mathrm{fin}(j)$. Arcs entering $(i,t,d)$ cost $c_{\mathrm{fin}(i)}(t)$.

Formalization targets

Goal: minimum-cost paths are optimal schedules

Under $k\ge 1$, positive costs, and the polygon inequalities of three or more hops (below):

1. a feasible schedule exists if and only if the modified network has a source-sink path;

$$\min_{(\sigma,t)\ \text{feasible}}\ \sum_p c_{\sigma(p)}(t_p)\;=\;\min_{\text{paths}}\ \sum_{p=1}^n c_{\mathrm{fin}(i_p)}(t_p),$$

each minimum existing exactly when the other does; 3. every minimum-cost path represents a feasible, optimal schedule.

Milestones

• Theorem 1 (with §3.1): the $k$-CPS sequences respecting precedence are exactly the sequences of source-sink paths of $G$.
• Lemma 5: every source-sink path of the modified network represents a feasible schedule.
• Lemma 6: every feasible schedule (in particular an optimal one) is represented by a source-sink path.
• Remark 1: under the triangle inequality, $d^{\min}_i=d^{\max}_i=\delta_{ab}$.
• Lemma 4: under the triangle inequality, a feasible schedule exists if and only if the simpler discrete-time network of §6.1.2, with nodes $(i,t)$, has a source-sink path.

Significance

The result turns a scheduling problem with arbitrary separable costs, time windows, precedence and non-metric separations into a shortest-path problem whose size is polynomial in $n$ for fixed $k$ and in the number of periods. It covers mixed arrival–departure operations, where the triangle inequality genuinely fails, and it is the basis of the paper's §7.1 algorithm for coupled arrivals and departures.

The paper proves Lemmas 5 and 6 in a few paragraphs and omits the proof of Lemma 4. No machine-checked version of the CPS network or of these lemmas exists. A formal development pins down the boundary cases the prose passes over (the first two stages, the last stage where $d^{\max}$ has no successors), and it makes explicit an assumption the prose leaves unstated: Lemma 5 needs the polygon inequalities, not only the two-step check in its proof.

Difficulty

The obvious argument checks separations only between consecutive aircraft, which is what the network of §6.1.2 does. Without the triangle inequality this misses aircraft two positions apart. The state $d$ repairs that but is capped at $d^{\max}$, so one must show that the cap loses nothing: a capped value still certifies the separation to the next aircraft. That uses the definition of $d^{\max}$ over the successors of a node in $G$, so the proof depends on how the network is pruned. Separations three or more positions apart are not tracked at all and rely on the polygon inequalities. Relating network paths to sequences (Theorem 1) requires reasoning about overlapping windows of the sequence and about the precedence pruning rule.

Formalization scope

Aircraft and positions are $0$-based (Fin n), stages $1$-based, and $n\ge 1$ (NeZero n). Times, windows and separations are natural numbers (periods); $d$, $d^{\min}$, $d^{\max}$ and time differences are integers, since $d^{\max}$ involves differences of separations that can be negative. Separation is required for all pairs of aircraft, not only consecutive ones. Minima are stated with IsLeast on sets of costs, never with a real infimum.

The following readings of the paper are committed:

• Polygon inequalities. Lemma 5 and the goal assume that for every chain $x_0,\dots,x_m$ of $m\ge 3$ hops between distinct aircraft, $\delta_{x_0x_m}\le\sum_i\delta_{x_ix_{i+1}}$. Without this hypothesis Lemma 5 is false: there are small instances violating the quadrilateral inequality whose minimum-cost path is infeasible. §7 of the paper asserts these inequalities for mixed operations; this mission states them as a hypothesis and makes no claim about the paper's Table 1.
• $\Gamma(i)$ is the full time window, not the narrowed set of §6.1.3, whose justification needs nondecreasing costs. With the full window Lemma 6 holds for every feasible schedule and arbitrary costs; it is stated in that stronger form.
• $k\ge 1$, so that every node beyond stage $1$ has a penultimate aircraft. Arc condition 4 is not imposed on arcs leaving stage $1$.
• Arc cost $c(i,t)$ of the paper is read as $c_{\mathrm{fin}(i)}(t)$.
• Precedence pruning uses the printed rule of §3.1; nodes unreachable from the source or the sink are not removed (this does not change the set of source-sink paths).
• Running times (§6.1.4, §6.3) and the bound $\lambda$ of recursion (4) are not formalized.

A trivializing formalization is ruled out: the networks are concrete definitions computed from the instance, not arbitrary graphs pinned by hypotheses, and the goal compares two independently defined minima, so it cannot hold by an empty feasible set or an unconstrained optimum.

A complete development needs basic list combinatorics (windows of a sequence, overlap of consecutive windows), the correspondence between bijections and paths, and finite minimization. The CPS network layer is shared with the other missions of this series and is reusable for any CPS scheduling result. Contributions on Theorem 1 alone are welcome, as it is independent of the time-expanded networks.

Selected references

• H. Balakrishnan, B. G. Chandran, Algorithms for Scheduling Runway Operations Under Constrained Position Shifting, Operations Research 58(6), 1650–1665, 2010. https://doi.org/10.1287/opre.1100.0869
• R. G. Dear, The Dynamic Scheduling of Aircraft in the Near Terminal Area, MIT Flight Transportation Laboratory Report R76-9, Massachusetts Institute of Technology, 1976 (as cited in the paper above).
• H. Lee, Tradeoff Evaluation of Scheduling Algorithms for Terminal-Area Air Traffic Control, Master's thesis, Massachusetts Institute of Technology, 2008 (source of the separation table; as cited in the paper above).

Motivation

Two-stage stochastic linear programming chooses a first-stage decision $x$ before a random parameter is revealed and pays an optimal second-stage (recourse) cost afterwards. The classical model fixes the distribution of the random parameter. In practice it is rarely known beyond a few moments, and a decision maker who is averse to risk does not evaluate the recourse cost by its plain expectation. Bertsimas, Doan, Natarajan and Teo (Math. Oper. Res. 35(3), 2010) take both points seriously: the distribution is only known to belong to the class of all distributions with given mean and second-moment matrix, the cost is passed through a convex piecewise-linear disutility, and the decision is evaluated against the worst distribution in the class.

Moment-based worst-case bounds go back to Scarf's newsvendor and to the Chebyshev-type bounds of the moment problem (Isii 1962; Bertsimas and Popescu 2005). Delage and Ye (Oper. Res. 58(3), 2010) showed that a broad class of such minimax problems is solvable in polynomial time by the ellipsoid method. For the case in which the uncertainty sits in the objective of the second-stage linear program, this paper gives a single semidefinite program (its Theorem 2.1, the subject of a companion mission) and, in §2.2, identifies the distributions that come arbitrarily close to the worst case. This mission is about the second result.

Setting

The first-stage region is $X=\{x\in\mathbb R^n : Ax=b,\ x\ge0\}$. For $x\in X$ the recourse set is $X(x)=\{w\in\mathbb R^d : Ww=h-Tx,\ w\ge0\}$ and the second-stage cost of an objective vector $q\in\mathbb R^d$ is

$$\mathcal Q(q,x)=\min_{w\in X(x)} q'w .$$

The disutility is $\mathbb U(t)=\max_{k=1,\dots,K}(\alpha_k t+\beta_k)$ with $\alpha_k\ge0$. The moment class $\mathcal P$ consists of the distributions $P$ of a random vector $\tilde q\in\mathbb R^d$ with $\mathbb E_P[\tilde q]=\mu$ and $\mathbb E_P[\tilde q\tilde q']=Q$. The worst-case value at $x$ is

$$Z(x)=\sup_{P\in\mathcal P}\mathbb E_P\big[\mathbb U(\mathcal Q(\tilde q,x))\big].$$

Its dual (6) is

$$Z_D(x)=\min_{Y,y,y_0}\ Q\cdot Y+\mu'y+y_0\quad\text{s.t.}\quad q'Yq+q'y+y_0\ge\mathbb U(\mathcal Q(q,x))\ \ \forall q\in\mathbb R^d ,$$

with $Y$ symmetric and $Q\cdot Y=\sum_{ij}Q_{ij}Y_{ij}$. Its semidefinite reformulation (8) has the dual (9):

$$Z_{DD}(x)=\max\ \sum_{k=1}^K (h-Tx)'p_k+\beta_kv_{k0}\quad\text{s.t.}\quad \sum_{k=1}^K\begin{pmatrix}V_k&v_k\\ v_k'&v_{k0}\end{pmatrix}=\begin{pmatrix}Q&\mu\\ \mu'&1\end{pmatrix},\ \begin{pmatrix}V_k&v_k\\ v_k'&v_{k0}\end{pmatrix}\succeq0,\ W'p_k\le\alpha_kv_k .$$

Its variables are scaled conditional moments: $v_{k0}$ is the probability that the $k$th piece of $\mathbb U$ is active, and $v_k$, $V_k$ are the first and second moments of $\tilde q$ on that event, multiplied by $v_{k0}$.

The standing assumptions are Assumption 3, $\{p\in\mathbb R^r : W'p\le q\}\ne\emptyset$ for every $q$, so that $\mathcal Q(q,x)$ is finite, and Assumption 4, $Q-\mu\mu'\succ0$. Recourse sets are assumed nonempty.

Formalization targets

Goal: Theorem 2.2

For every $x\in X$ there is a sequence $P_j\in\mathcal P$ with $\mathbb E_{P_j}[\mathbb U(\mathcal Q(\tilde q,x))]\to Z(x)$, and

$$Z(x)=Z_D(x)=Z_{DD}(x),$$

where all three are finite optimal values: a supremum over a nonempty bounded-above set, an infimum over a nonempty bounded-below set, and a supremum over a nonempty bounded-above set.

Milestones

1. Lemma 2.1: $Z_{DD}(x)\ge Z(x)$, in the form "each $P\in\mathcal P$ gives a feasible point of (9) whose objective equals $\mathbb E_P[\mathbb U(\mathcal Q)]$".
2. (9) has an optimal solution.
3. $\mathcal Q(\cdot,x)$ is positively homogeneous and superadditive.
4. If $W'p\le\alpha v$ with $\alpha\ge0$ then $\alpha\mathcal Q(v,x)\ge(h-Tx)'p$.
5. Jensen: $\mathbb E[\mathcal Q(\tilde r,x)]\le\mathcal Q(\mathbb E\tilde r,x)$, with $\mathcal Q(\tilde r,x)$ integrable.
6. An optimal solution of (9) can be chosen so that every block has $v_{k0}>0$ or vanishes.
7. Strong duality $Z(x)=Z_D(x)$ (§2.1).

Significance

Theorem 2.2 says that the semidefinite bound is tight and that the worst case is approached by explicit mixtures. With probability $v_{k0}$ the cost vector sits at the conditional mean $v_k/v_{k0}$, and with a small probability it is perturbed by a large Gaussian. The construction tells which scenarios a minimax solution guards against. The paper's numerical section uses it to stress-test solutions computed under other distributional assumptions. For the risk-neutral case ($K=1$) the bound collapses to Jensen's bound $\min_{w\in X(x)}\mu'w$. For $K>1$ it is a combination of Jensen bounds, one per piece of the disutility.

Theorem 2.2 is proved in the paper; no part of it, nor the strong duality of the moment problem that it relies on, is formalized on the platform or, to our knowledge, elsewhere. The mission asks for machine-checked proofs of the identity $Z=Z_D=Z_{DD}$ and of the steps of the extremal construction. Several of these are reusable beyond this paper: weak and strong duality of moment problems, the existence of optimal solutions of moment-type semidefinite programs, and Jensen's inequality for the value function of a linear program.

Difficulty

Most of the argument is linear programming and bookkeeping. The step $Z(x)=Z_D(x)$ is a strong-duality theorem for an infinite-dimensional linear program over measures. The paper cites it from Isii's theory of the moment problem, and none of that theory exists in Mathlib. The construction of near-extremal distributions also needs care. A single distribution in $\mathcal P$ generally cannot attain $Z(x)$, so the bound is reached only along a family whose second moments are matched by rare, large perturbations. Lemma 2.1 needs measurable selections of an active piece of $\mathbb U$ and of a dual optimal solution of the second-stage program as functions of $q$. When the optimal solution of (9) has zero-weight blocks, the mixture is undefined until the solution is first rearranged.

Formalization scope

Vectors are Fin d → ℝ, matrices Matrix (Fin r) (Fin d) ℝ, and distributions are probability measures on Fin d → ℝ with square-integrable coordinates. They are not densities as in the paper's (5). The moment class uses the published MomentDRO.Conf definitions, and $\mathbb E[\tilde q\tilde q']$ is the uncentred second moment. The paper writes $p$ both for the dimension of $q$ and for dual vectors. Here the dimension is $d$ and dual vectors are named π. Indices $k$ are zero-based. Bordered matrices are Matrix.fromBlocks on Fin d ⊕ Fin 1 and $\succeq0$ is Matrix.PosSemidef. $\mathcal Q$ is a real infimum and the optimal values are real sSup/sInf of value sets. Every statement that uses an optimal value also asserts IsLUB/IsGLB, so junk values cannot make a statement true.

As printed, Assumption 2 (complete recourse) and Assumption 3 for all $q$ contradict each other whenever $W$ has a row. The formalization keeps Assumption 3 for all $q$ and replaces complete recourse by nonemptiness of $X(x)$, which is what §2's proofs use. Assumption 1 is not used and is omitted. The hypotheses are jointly satisfiable, for example by $W=I$, $T=0$, $h=0$, $\mu=0$ and $Q=I$.

The sequence clause of Theorem 2.2 alone holds for every finite supremum, so it does not capture the theorem. The goal therefore also asserts the equalities $Z=Z_D=Z_{DD}$, with all three values genuine, and these carry the content. A formalization that drops them, or states them only through junk values, is ruled out.

A complete development needs the duality theory of the moment problem, Jensen's inequality for concave functions on $\mathbb R^d$, compactness arguments for semidefinite feasible sets, and multivariate Gaussian mixtures (ProbabilityTheory.multivariateGaussian in Mathlib). Proofs of individual milestones are welcome. So is a general moment-problem duality theorem from which strong_duality follows.

Selected references

• D. Bertsimas, X. V. Doan, K. Natarajan, C.-P. Teo, Models for Minimax Stochastic Linear Optimization Problems with Risk Aversion, Mathematics of Operations Research 35(3):580–602, 2010. https://doi.org/10.1287/moor.1100.0445
• E. Delage, Y. Ye, Distributionally Robust Optimization Under Moment Uncertainty with Application to Data-Driven Problems, Operations Research 58(3):595–612, 2010. https://doi.org/10.1287/opre.1090.0741
• K. Isii, On sharpness of Tchebycheff-type inequalities, Annals of the Institute of Statistical Mathematics 14:185–197, 1962. https://doi.org/10.1007/BF02868641
• D. Bertsimas, I. Popescu, Optimal Inequalities in Probability Theory: A Convex Optimization Approach, SIAM Journal on Optimization 15(3):780–804, 2005. https://doi.org/10.1137/S1052623401399903

Motivation

Zara ships inventory from a central warehouse to each of its stores every week, and for a short-lived fashion item the warehouse holds a limited amount of each size. Deciding how many units of each size to ship to each store is therefore a constrained allocation problem whose objective is the expected sales a store will realize from a given inventory. Caro and Gallien (working paper, 2007; published in Operations Research, 2010) built such a model, embedded it in a weekly shipment optimization, and tested it in a field experiment in Zara's store network. The store-level sales model has one unusual feature, taken from Zara's practice: as soon as one of the major sizes of an item runs out, the whole item is removed from display, so stock-outs of different sizes interact.

The expected sales under that policy have no closed form usable inside a mixed integer program. The paper replaces them by an explicit piecewise-linear function and asserts that this replacement is an upper bound. This mission formalizes that claim, the chain of identities and inequalities that lead to it, and the paper's statement that its shipment program represents the approximation exactly.

Setting

A reference is offered in a finite set of sizes $\mathcal S = \mathcal S^+ \cup \mathcal S^-$, with major sizes $\mathcal S^+$ and minor sizes $\mathcal S^- = \mathcal S \setminus \mathcal S^+$. Sale opportunities for size $s$ follow a Poisson process $N_s(t)$ with rate $\lambda_s > 0$, independent across sizes, where $t$ is the time since the last replenishment and $T > 0$ is the time between replenishments.

Given an inventory vector $q \in \mathbb N^{\mathcal S}$, the virtual stockout time of size $s$ is $\tau_s(q_s) = \inf\{t \ge 0 : N_s(t) = q_s\}$, and $\tau_{\mathcal A} = \min_{s \in \mathcal A}\tau_s(q_s)$ for a set of sizes $\mathcal A$. Writing $a \wedge b = \min(a,b)$, the number of sales in one period is

$$G(q) = \sum_{s \in \mathcal S^+} N_s(\tau_{\mathcal S^+} \wedge T) + \sum_{s \in \mathcal S^-} N_s(\tau_{\mathcal S^+ \cup \{s\}} \wedge T),$$

since every size stops selling when the first major size runs out, and a minor size also stops when it runs out itself. The expected sales function is $g_\lambda(q) = \mathbb E[G(q)]$.

For the approximation, let $\gamma(a,b) = \int_0^b v^{a-1}e^{-v}\,dv$ be the lower incomplete Gamma function, and define the tangent coefficients

$$a_k(\lambda) = \frac{\gamma(k+1, \lambda T)}{\lambda\, k!}, \qquad b_i(\lambda) = \sum_{k=0}^{i-1} a_k(\lambda),$$

with the tangent at $i = \infty$ equal to the constant $T$. For each size choose a nonempty finite set $\mathcal N(\lambda_s) \subseteq \mathbb N \cup \{\infty\}$ of tangent indices. The approximate expected sales function is

$$\tilde g_\lambda(q) = \lambda_{\mathcal S^+} \min_{s \in \mathcal S^+} \min_{i \in \mathcal N(\lambda_s)} \{a_i(\lambda_s)(q_s - i) + b_i(\lambda_s)\} + \sum_{s \in \mathcal S^-} \lambda_s \min_{s' \in \mathcal S^+ \cup \{s\}} \min_{i \in \mathcal N(\lambda_{s'})} \{a_i(\lambda_{s'})(q_{s'} - i) + b_i(\lambda_{s'})\},$$

with $\lambda_{\mathcal S^+} = \sum_{s\in\mathcal S^+}\lambda_s$. In Lean the objects are expectedSales, hA ($\mathbb E[\tau_{\mathcal A}\wedge T]$), a, b, tangent and gTilde in the namespace FastFashion.Approx.

Formalization targets

Goal: the approximation is an upper bound

For every independent Poisson family with positive rates, every $T > 0$, every nonempty $\mathcal S^+$, every choice of nonempty finite tangent sets, and every $q \in \mathbb N^{\mathcal S}$,

$$g_\lambda(q) \le \tilde g_\lambda(q).$$

The statement fixes no tangent set, so it covers the paper's numerical choice (7) and every refinement of it.

Milestones

1. Eq. (2): $g_\lambda(q) = \lambda_{\mathcal S^+}\mathbb E[\tau_{\mathcal S^+}\wedge T] + \sum_{s\in\mathcal S^-}\lambda_s\mathbb E[\tau_{\mathcal S^+\cup\{s\}}\wedge T]$.
2. Eq. (3): $\mathbb E[\tau_{\mathcal D}\wedge T] \le \min_{s\in\mathcal D}\mathbb E[\tau_s\wedge T]$ for nonempty $\mathcal D$.
3. Eqs. (4)–(5): $\mathbb E[\tau_s\wedge T] = \frac1{\lambda_s}\sum_{k=1}^{q_s}\mathbb P(N_s(T)\ge k) = \sum_{k=1}^{q_s}\frac{\gamma(k,\lambda_sT)}{\lambda_s\Gamma(k)}$.
4. The terms $a_k(\lambda)$ are positive and strictly decreasing in $k$.
5. Eq. (6): $\mathbb E[\tau_s\wedge T] = \min_{i\in\mathbb N\cup\{\infty\}}\{a_i(\lambda_s)(q_s-i)+b_i(\lambda_s)\}$, the minimum attained.

Further result: the MIP represents the approximation

In the shipment program (MIP) (13)–(19) of §3.2, with positive prices, every optimal solution has $z_j = \tilde g_{\lambda_j}(x_j + I_j)$ at every store $j$.

Significance

The upper bound is what makes the paper's optimization coherent: the MIP maximizes $\sum_j P_j \tilde g_{\lambda_j}$, and the bound guarantees that this objective never underestimates the expected revenue of a shipment plan, with an error controlled by the number of tangents. Identity (6) exhibits $\mathbb E[\tau_s \wedge T]$ as a concave function of $q_s$ with explicit Erlang-type slopes; (2) is a standard optional-sampling identity for compensated Poisson processes stopped at a bounded stopping time; and the MIP statement is the step that turns a minimum of affine functions into linear constraints.

The paper proves none of these in detail: (2), (4) and (5) are justified by a reference to the optional sampling theorem, (6) by a sentence on discrete concavity, and the upper bound and the MIP claim by one sentence each. None of the statements has a machine-checked proof. A formalization produces a checked chain from the Poisson model to the deterministic program, fixes the indexing error in the printed coefficients of (6), and isolates the exact hypotheses (nonempty major sizes, nonempty tangent sets, positive prices) under which the claims hold.

Difficulty

The deterministic parts — (3) given pathwise monotonicity, the envelope inequality given concavity, and the MIP argument — are short. The probabilistic identities are not. Equation (2) needs the optional sampling theorem for the compensated process $N_s(t) - \lambda_s t$ in continuous time, applied at $\tau_{\mathcal A} \wedge T$ (the paper cites Karatzas and Shreve 1991), which requires showing that $\tau_{\mathcal A}$ is a stopping time for the joint filtration of the family and that $N_s$ is still a martingale with respect to that larger filtration; this is where independence across sizes enters. Equation (4) needs the distribution of $\tau_s(q_s)$, the $q_s$-th arrival time, which is Erlang; the statement in the model is about first hitting times of a counting process, not about sums of exponential inter-arrival times, so the link between the two descriptions has to be built. Equation (5) needs the identity $\mathbb P(N(T) \ge k) = \gamma(k, \lambda T)/\Gamma(k)$ between Poisson tails and the incomplete Gamma function.

A tempting shortcut is to define $g_\lambda$ directly by formula (2), or $\mathbb E[\tau_s\wedge T]$ by formula (4); both make the corresponding milestones definitional and the goal a statement about formulas rather than about sales. The formalization defines $g_\lambda$ from $G$ and $h^{\mathcal A}$ from the stopping times.

Formalization scope

• Model. Sizes form a finite type; the major sizes are a Finset and the minor sizes its complement. The demand is a structure IsPoissonFamily λ N P: each $N_s$ is a counting process with $N_s(0)=0$, non-decreasing right-continuous paths with unit jumps, Poisson increments of mean $\lambda_s(t-u)$, independent increments, and the processes are independent across sizes. $P$ is a probability measure.
• Stockout times take values in $\mathbb R \cup \{+\infty\}$ (WithTop ℝ), so the infimum of an empty set is $+\infty$, never $0$; $\tau_{\mathcal A}\wedge T$ is a real number in $[0,T]$.
• Expectations are Bochner integrals. They are not junk: $0 \le G(q) \le \sum_s N_s(T)$, which is integrable, and $\tau_{\mathcal A}\wedge T \in [0,T]$.
• Corrected coefficients. As printed, $a_k = \gamma(k,\lambda T)/(\lambda\Gamma(k))$ and $b_1 = a_0$ involves $\Gamma(0)$; the formalization uses $a_k = \gamma(k+1,\lambda T)/(\lambda\,k!)$, matching the paper's description of $a_k$ as the probability that the $(k+1)$-th unit sells.
• Tangent sets. The rule (7), "$b_i(\lambda_s) \approx 0, 0.3T, 0.6T, 0.8T, 0.9T, T$", is approximate and is replaced by an arbitrary nonempty finite set $\mathcal N(\lambda_s) \subseteq \mathbb N\cup\{\infty\}$.
• Added hypotheses. $\mathcal S^+ \ne \emptyset$ (for (8) and the goal), nonempty $\mathcal D$ in (3), and $P_j > 0$ in the MIP statement.
• MIP. Optimality is defined as feasibility plus an objective at least that of every feasible point; existence of an optimum is not asserted.

The paper's further remark that $\tilde g_\lambda$ inherits the qualitative properties of Proposition 1, and the multicolor extension of Appendix §5.2, are not included. Contributions of general infrastructure are welcome: optional sampling for continuous-time counting processes, Erlang hitting-time laws for Poisson processes, and the Poisson-tail/incomplete-Gamma identity are all reusable well beyond this mission.

Selected references

• F. Caro, J. Gallien, Inventory Management of a Fast-Fashion Retail Network, working paper (August 2, 2007); published in Operations Research 58(2), 2010. https://doi.org/10.1287/opre.1090.0698
• I. Karatzas, S. E. Shreve, Brownian Motion and Stochastic Calculus, 2nd ed., Springer, 1991. https://doi.org/10.1007/978-1-4612-0949-2

Motivation

Facilities fail: plants close, warehouses flood, suppliers strike. Reliable facility location models choose facility sites knowing that each opened site may be unavailable, and they assign every customer a primary facility and an ordered list of backups. Snyder and Daskin (Transportation Science, 2005) introduced the level-assignment formulation with a common failure probability. Cui, Ouyang and Shen (Operations Research 58(4), 2010; working paper UCTC-FR-2010-02, February 2010) let every site $j$ have its own failure probability $q_j$, with failures independent. With site-dependent probabilities, even for fixed open sites, the best backup list for one customer is no longer simply the nearest sites in order of distance (their Example 1, p. 11).

The paper solves the model by Lagrangian relaxation. Relaxing the constraints that link assignments to open sites splits the problem into one relaxed subproblem (RSP$_i$) per customer $i$, solved at every subgradient iteration. The authors show that (RSP$_i$) is the minimization of a set function $\Phi_i$ over sets of at most $R$ sites, and their Proposition 3 asserts that $\Phi_i$ is supermodular, which makes the branch-and-bound algorithm of Goldengorin et al. for supermodular minimization applicable. This mission formalizes Proposition 3 and the steps of its proof (Appendix A.3).

Setting

Fix a customer $i$ with demand rate $\lambda_i \ge 0$ and unserved-demand penalty $\varphi_i$. There are $J$ regular sites $j = 0, \dots, J-1$ with unit costs $d_{ij}$, failure probabilities $0 \le q_j < 1$ and Lagrange multipliers $\mu_{ij}$. An emergency facility with index $J$ never fails ($q_J = 0$) and costs $d_{iJ} = \varphi_i$ per unit: being served by it means not being served. The customer is assigned at levels $r = 0, 1, \dots, R$ with $R \ge 1$. A level-$r$ facility serves the customer exactly when the facilities at levels $0, \dots, r-1$ have all failed.

The variables are $Y_{jr} \in \{0,1\}$ (site $j$ is the level-$r$ facility), $P_{jr}$ (the probability that $j$ serves at level $r$, given the earlier levels) and $W_{jr}$, which the linearization constraints force to equal $P_{jr} Y_{jr}$. The constraints of (RSP$_i$) say that every level is filled by one regular site or comes after the emergency facility, that each regular site is used at most once, that the emergency facility appears exactly once, and that

$$P_{j0} = 1 - q_j, \qquad P_{jr} = (1-q_j) \sum_{k=0}^{J-1} \frac{q_k}{1-q_k} W_{k,r-1} \quad (1 \le r \le R).$$

For a set $S \subseteq \{0, \dots, J-1\}$, $\Phi_i(S)$ is the minimum of

$$\sum_{j=0}^{J} \sum_{r=0}^{R} \lambda_i d_{ij} W_{jr} + \sum_{j \in S} \mu_{ij}$$

over the feasible points that use no regular site outside $S$. The customer's subproblem is $\min\{\Phi_i(S) : |S| \le R\}$.

Formalization targets

Goal: Proposition 3 in the form (18)

For every customer $i$, every $S \subseteq \{0, \dots, J-1\}$ and all regular sites $u \ne v$ outside $S$ with $|S| + 2 \le R$,

$$\Phi_i(S \cup \{u,v\}) - \Phi_i(S \cup \{u\}) \ \ge\ \Phi_i(S \cup \{v\}) - \Phi_i(S).$$

The paper states "$\Phi_i$ is supermodular" without restriction. That statement is false: for sets larger than $R$ the inequality can fail (an instance with $J = 5$, $R = 3$ is recorded in the goal's statement). The cardinality bound covers all the sets the subproblem ranges over, and the paper's proof uses it implicitly.

Milestones (Appendix A.3)

1. Closed form. If $|S| \le R$ and $S = \{j_1, \dots, j_n\}$ is listed by nondecreasing distance, then $\Phi_i(S) = \lambda_i \sum_{k=1}^{\bar n+1} C_k + \sum_{j \in S} \mu_{ij}$, where $\bar n$ counts the elements of $S$ with $d_{ij} \le \varphi_i$, $P_k = \prod_{\ell \le k} q_{j_\ell}$, $C_k = P_{k-1}(1-q_{j_k}) d_{ij_k}$ for $k \le \bar n$ and $C_{\bar n+1} = P_{\bar n}\varphi_i$.
2. Marginal cost. For $v \notin S$ with $|S| + 1 \le R$ and $d_{iv} \le \varphi_i$: $\Phi_i(S\cup\{v\}) - \Phi_i(S) = \lambda_i(1-q_v)\big[P_t d_{iv} - \sum_{k=t+1}^{\bar n+1} C_k\big] + \mu_{iv}$, with $t$ the number of elements of $S$ no farther than $v$. If $d_{iv} \ge \varphi_i$ the marginal cost is $\mu_{iv}$.
3. Sign. $P_t d_{iv} - \sum_{k=t+1}^{\bar n+1} C_k \le 0$ when $d_{iv} \le \varphi_i$.
4. Case 1 ($d_{iu} \le d_{iv}$) and Case 2 ($d_{iu} > d_{iv}$): explicit formulas for $\Phi_i(S\cup\{u,v\}) - \Phi_i(S\cup\{u\})$ in terms of the $C_k$ of $S$.

Significance

Supermodularity of $\Phi_i$ is what the paper's exact algorithm for (RSP$_i$) rests on: the branch-and-bound method of Goldengorin et al. prunes by comparing marginal costs, and its correctness requires them to be monotone. Each Lagrangian iteration solves $I$ such subproblems, so this property sits inside the paper's whole solution method. The closed form (milestone 1) is also a self-contained statement about the optimal backup order with site-dependent failure probabilities: once the set of sites is fixed, nearest-first is optimal, and sites beyond the penalty distance are never used.

Formally, nothing in this mission is machine-checked yet. The paper's argument has gaps that a formalization has to repair: the missing cardinality hypothesis; a "strict" sign claim (milestone 3) that is only weak when some $q_j = 0$ or $d_{iv} = \varphi_i$; counts printed as infima; and an intermediate inequality in Case 2 that does not hold as printed, although the case's conclusion does. A checked proof settles which version of Proposition 3 is true.

Difficulty

The algebra of the cases is routine once the closed form is available. The hard step is the closed form itself: $\Phi_i(S)$ is defined as the minimum of a mixed-integer program, and the paper justifies the closed form only by "a similar argument as in the proof of Proposition 2", an exchange argument. One has to show that every feasible point is a nearest-first chain truncated at the emergency facility, that $P$ and $W$ are then determined by $Y$, that reordering a chain by distance never increases the cost, and that adding a site within the penalty distance never hurts. With at most $R$ regular levels, the exchange must respect the level budget. This is exactly where the cardinality hypothesis enters.

A tempting shortcut is to define $\Phi_i$ by its closed form. That makes milestone 1 true by definition and detaches the goal from the optimization problem; the definition here is the program (5).

Formalization scope

Lean conventions: one customer at a time, with the index $i$ dropped in the definition. Regular sites are Fin J; all sites are Fin (J+1), with Fin.last J the emergency facility, whose cost $\varphi_i$ and probability $0$ are built into the extended data. Levels are Fin (R+1). Variables are real-valued, with $Y_{jr} \in \{0,1\}$ as a constraint. $\Phi_i(S)$ is the infimum of the set of feasible objective values. This set is nonempty and bounded below, and in fact finite, so the infimum is the minimum. Data hypotheses: $\lambda_i \ge 0$, $0 \le q_j < 1$, $R \ge 1$; costs, penalties and multipliers carry no sign assumption. The list $j_1, \dots, j_n$ is any duplicate-free list of $S$ sorted by distance. Ties are allowed.

Printed typos corrected in the definitions: the level constraint (4b) counts the emergency facility in its first sum; (5b) includes the linearization constraints (4h); (5c) covers regular site $0$; (5a) has $\lambda_i$ for the undefined $h_i$.

Excluding the configurations with $|S \cup \{u, v\}| > R$ from the goal is deliberate. Weakening the goal further, for example to $\lambda_i = 0$ or to sets on which $\Phi_i$ is modular, would trivialize it.

Contributions welcome: a proof of the closed form (an exchange argument on level chains, reusable for the other propositions of the paper), then the marginal-cost algebra and the two cases.

Selected references

• T. Cui, Y. Ouyang, Z.-J. M. Shen, Reliable Facility Location Design under the Risk of Disruptions, UCTC-FR-2010-02 (working paper, Feb. 2010); published in Operations Research 58(4):998–1011, 2010. https://doi.org/10.1287/opre.1090.0801
• L. V. Snyder, M. S. Daskin, Reliability Models for Facility Location: The Expected Failure Cost Case, Transportation Science 39(3):400–416, 2005. https://doi.org/10.1287/trsc.1040.0107
• B. Goldengorin, G. Sierksma, G. A. Tijssen, M. Tso, The Data-Correcting Algorithm for the Minimization of Supermodular Functions, Management Science 45(11):1539–1551, 1999. https://doi.org/10.1287/mnsc.45.11.1539

Returns and the retailer's incentive for sales effort

A manufacturer that sells through a retailer can accept returns: it pays a return credit $b$ for every unit the retailer has not sold at the end of the season. Returns policies are common in publishing, software and computer hardware, and since Pasternack (Marketing Science, 1985) they have been studied as a way to make the retailer order more. Retailers also raise demand through sales effort: merchandising, shelf space, point-of-sale advertising. A recurring view in the marketing and operations literature is that returns weaken this incentive. Padmanabhan and Png (1995, p. 70) write that "by reducing the risk of losses due to excess inventory, a returns policy lessens some of the retailer's incentive to invest in such efforts", and Kandel (1996, p. 348) makes the same argument for consignment.

T. A. Taylor, Supply Chain Coordination Under Channel Rebates with Sales Effort Effects (Management Science 48(8), 2002), studies a newsvendor retailer who chooses an order quantity and a sales effort level before demand is observed. Its Proposition 4 shows that in this model the conventional view is reversed: a larger return credit makes the retailer exert strictly more effort. This mission formalizes that proposition and the solution of the retailer's problem it rests on.

Setting

Prices satisfy $0<c<w<p$ and $s<c$ (Assumption A1): $p$ is the retail price, $w$ the wholesale price, $c$ the manufacturing cost and $s$ the salvage value, which may be negative. A demand factor $\xi\ge 0$ has a density $\varphi$ with $\varphi(\xi)>0$ for every $\xi\ge0$ (Assumption A4), distribution function $\Phi(Q)=\int_0^Q\varphi$ and partial mean $\Gamma(Q)=\int_0^Q\xi\,d\Phi(\xi)$.

The retailer chooses an effort level $e\ge0$, and demand is $e\xi$. Effort costs $V(e)$, where $V$ is strictly convex and strictly increasing with $V(0)=0$ (Assumption A5; the paper declares every convexity and monotonicity statement strict). Write $\Lambda(\gamma)=\gamma V'(\gamma)-V(\gamma)$.

Under a returns-only contract $(w,b)$ with $b\in[s,w)$, the retailer orders $Q\ge0$, exerts effort $e\ge 0$, and earns the expected profit

$$\underline R_b(Q,e)=-wQ+p\,E\min(Q,e\xi)+b\,E(Q-e\xi)^+-V(e).$$

This is the integrated channel's profit $\Pi(Q,e)=-cQ+pE\min(Q,e\xi)+sE(Q-e\xi)^+-V(e)$ with $w$ in place of $c$ and $b$ in place of $s$. An optimal pair is a maximizer of $\underline R_b$ over $Q\ge0$, $e\ge0$. The paper's $\underline e$ is the effort of such a pair, and $\underline Q_0$ is the critical fractile $\Phi(\underline Q_0)=(p-w)/(p-b)$.

Formalization targets

Goal: Proposition 4 (p. 1004)

If $s\le b_2<b_1<w$, $(Q_1,e_1)$ is an optimal pair under the credit $b_1$, $(Q_2,e_2)$ is an optimal pair under $b_2$, and $e_2>0$, then

$$e_2<e_1 .$$

The paper writes this as $\partial\underline e/\partial b>0$. Its proof shows strict monotonicity, and that is the statement here.

Milestone 1: the order for a given effort (§4.2, p. 1000)

For a fixed $e>0$, the unique maximizer of $Q\mapsto\underline R_b(Q,e)$ over $Q\ge0$ is $Q_2=e\,\underline Q_0$, and

$$\max_{Q\ge0}\underline R_b(Q,e)=e\,(p-b)\,\Gamma(\underline Q_0)-V(e).$$

Milestone 2: the optimal effort (§4.2, p. 1000)

An optimal pair $(Q,\underline e)$ with $\underline e>0$ satisfies

$$V'(\underline e)=(p-b)\,\Gamma(\underline Q_0),\qquad Q=\underline e\,\underline Q_0,\qquad \underline R_b(Q,\underline e)=\Lambda(\underline e),$$

and conversely every $e>0$ solving this first-order condition gives the optimal pair $(e\underline Q_0,e)$.

Significance

The result. Proposition 4 separates two effects of a return credit. For a fixed order quantity, a larger credit lowers the marginal value of effort: it pays the retailer for unsold units, and effort only matters through sold units. This is the fixed-quantity comparison on which the conventional view rests; Cachon's survey states it for buy-backs as Eq. (19) (on Prove2Me as CachonCoord.EffortNewsvendor.sec_6_4_1_effort_coordination, clause 1). Once the order quantity is chosen together with the effort, the larger credit raises the order, and the effort follows. For the multiplicative demand model the net effect is unambiguous for every demand density and every convex effort cost. A manufacturer that wants more retailer effort can therefore use the return credit as a lever, and a model that ignores the quantity response gets the sign wrong.

Formalizing it. The result is proved in the paper, in a four-line appendix argument that relies on the §4.2 solution of the retailer's problem; neither is machine-checked anywhere. The mission produces a checked newsvendor-with-effort solution (the scaling $Q_2=e\underline Q_0$ and the profit $\Lambda(\underline e)$), which the other missions of this series and any multiplicative-effort supply-chain model can reuse, and a checked statement of the comparative statics in the return credit.

Difficulty

The obvious argument differentiates the retailer's first-order condition in $b$ with the order held fixed, and it gives the wrong sign; the order quantity must be re-optimized. The correct comparison runs through the reduced problem in the effort alone, and it needs the §4.2 solution in full: the scaling of the optimal order with the effort, which turns $E\min(Q,e\xi)$ and $E(Q-e\xi)^+$ into newsvendor expectations of $\xi$ at $Q/e$; the value of the optimal order as a function of $e$; and the first-order characterization of the optimal effort. The comparison across credits then involves two objects: the function $\Lambda$, and the retailer's reduced profits under the two credits at a common effort level. The statement compares maximizers of two different optimization problems, not roots of an equation, so a formal proof must connect optimality of the pair to the first-order condition, which uses the strict convexity of $V$ and the positivity of the density.

Formalization scope

Everything lives in the namespace ChannelRebate.ReturnsEffort. The definitions file holds:

• Demand: a measurable density $\varphi$, zero on $(-\infty,0)$, positive on $[0,\infty)$, integrating to $1$, with finite mean;
• the law of $\xi$;
• $\Phi$ and $\Gamma$ as interval integrals;
• EffortCost: A5 with strict convexity and strict monotonicity on $[0,\infty)$ and $V(0)=0$;
• $\Lambda$;
• the retailer's profit returnsProfit;
• optimal orders and optimal pairs as maximizers over $Q\ge0$ (and $e\ge0$).

The expectations are the published CachonCoord.Newsvendor.expSales and expLeftover applied to the law of $e\xi$ (the image of the law of $\xi$ under $x\mapsto ex$).

The formalization makes the following commitments, each recorded on its item:

• $\Phi^{-1}$ is never an inverse function: $\underline Q_0$ is a positive solution of $\Phi(\underline Q_0)=(p-w)/(p-b)$.
• The paper writes $(\partial/\partial e)V$ without stating that $V$ is differentiable. Differentiability on $(0,\infty)$, with derivative $V'$, is a hypothesis.
• The paper restricts attention to strictly positive effort (p. 1000). The goal therefore assumes $e_2>0$; without it both optimal efforts could be $0$ when $V'(0^+)$ is large, and the strict inequality would fail.
• Existence of optimal pairs is a hypothesis, as on p. 999 ("assume the cost of effort function and demand distribution are chosen such that the existence of an optimal solution is assured").
• The credit satisfies $b<w$ strictly; at $b=w$ the critical fractile is undefined.

The goal is about optimal pairs of the joint problem. Defining $\underline e$ as the root of the first-order condition, or fixing the order quantity and varying $b$, would give a different and, in the second case, false statement; neither is the target.

Contributions are welcome:

• a proof of the scaling identity $E\min(Q,e\xi)=e\,E\min(Q/e,\xi)$;
• a proof of the newsvendor value identity $(p-b)E\min(q,\xi)-(w-b)q=(p-b)\Gamma(q)$ at the critical fractile, reusable for any newsvendor with a density;
• proofs of the two milestones;
• the goal theorem.

The two facts the paper's proof uses — that $\Lambda$ is strictly increasing on $(0,\infty)$, and that the retailer's reduced profit at a fixed effort increases with the credit — may be posted as supporting theorems.

Selected references

• T. A. Taylor, Supply Chain Coordination Under Channel Rebates with Sales Effort Effects, Management Science 48(8):992–1007, 2002. https://doi.org/10.1287/mnsc.48.8.992.168
• B. A. Pasternack, Optimal Pricing and Return Policies for Perishable Commodities, Marketing Science 4(2):166–176, 1985. https://doi.org/10.1287/mksc.4.2.166
• V. Padmanabhan, I. P. L. Png, Returns Policies: Make Money by Making Good, Sloan Management Review 37(1):65–72, 1995.
• E. Kandel, The Right to Return, Journal of Law and Economics 39(1):329–356, 1996. https://doi.org/10.1086/467352
• G. P. Cachon, Supply Chain Coordination with Contracts, in Handbooks in OR & MS 11, Elsevier, 2003, §6.4.1. https://doi.org/10.1016/S0927-0507(03)11006-7