Probability

Motivation

Perishable products, among them fresh food, blood platelets and pharmaceuticals, lose their value after a fixed number of periods. Their inventory control has been studied since the 1970s (Nahmias, Perishable inventory theory: a review, Operations Research 1982). The optimal policy of the standard lost-sales model depends on the whole age profile of the stock and is computationally intractable when the lifetime is long. Practitioners therefore use base-stock policies, which raise the total inventory to a fixed level every period. Before Bu, Gong & Chao (SSRN 3724966, accepted at Management Science, 2022), no guarantee was known on how far the best such policy, or any explicitly computable one, is from optimal.

This mission concerns the regime of a large unit penalty cost. Firms in retail and manufacturing often run at very high service levels (Huh et al. 2009; Wei et al. 2021), which in a cost-based model means that the unit lost-sales penalty $p$ is much larger than the unit holding cost $h$. The question is whether a simple base-stock policy remains near-optimal as $p$ grows.

Setting

A product has a fixed lifetime of $m\ge1$ periods. Demands $D_1,D_2,\dots$ are i.i.d. copies of a non-negative random variable $D$ with $0<\mathbb E[D]<\infty$ and distribution function $F(x)=\mathbb P(D\le x)$. At the start of period $t$ the state is $x_t=(x_{t,1},\dots,x_{t,m-1})$, where $x_{t,i}$ is the stock whose remaining lifetime is at most $i$ periods, and $x_{t,0}:=0$. The firm orders $q_t\ge0$ and the total level becomes $x_{t,m}=x_{t,m-1}+q_t$ (zero lead time). Demand is served oldest first (FIFO issuance) and unmet demand is lost. The outdated quantity is $o_t=(x_{t,1}-D_t)^+$, and the dynamics are

$$x_{t+1,i}=(x_{t,i+1}-D_t-o_t)^+,\qquad i=1,\dots,m-1,$$

starting from the empty state $x_1=0$. The period cost is $C^\pi_t=h(x^\pi_{t,m}-D_t)^++p(D_t-x^\pi_{t,m})^++\theta o^\pi_t$, with $h>0$, $p>0$ and an additional outdating cost $\theta\ge0$. An admissible policy orders $q_t=\varphi^\pi_t(x_t)$ with each $\varphi^\pi_t$ a non-negative measurable function of the state. Its long-run average cost is $C^\pi=\limsup_{T\to\infty}\frac1T\sum_{t=1}^T\mathbb E[C^\pi_t]$, and $\mathrm{OPT}=\inf_\pi C^\pi$ over all admissible policies.

The base-stock policy $\pi_S$ orders $(S-x_{t,m-1})^+$, and $C(S)$ is its average cost. $\mathbb E[O_\infty(S)]$ is its long-run average outdated quantity. The heuristic level $\widetilde S$ is any minimizer over $[0,\infty)$ of

$$\widetilde C(S)=h\mathbb E[(S-D)^+]+p\mathbb E[(D-S)^+]+\frac\theta m\mathbb E\Big[\Big(S-\sum_{i=1}^mD_i\Big)^+\Big].$$

Two further objects appear: the upper support $\bar D=\sup\{x:F(x)<1\}\in[0,\infty]$ (demand is bounded when $\bar D<\infty$), and the floor level $\underline S=\arg\min_{S\ge0}\{h\mathbb E[(S-D)^+]+p\mathbb E[(D-S)^+]+\theta S\}$. A subscript $p$ marks dependence on the penalty: $C_p$, $\mathrm{OPT}_p$, $\widetilde S_p$.

Formalization targets

Goal: Theorem 3 (p. 13)

$$\lim_{p\to\infty}\big(C_p(\widetilde S_p)-\mathrm{OPT}_p\big)=0,$$

with $m$, $h$, $\theta$ and the demand law fixed, for every selection $p\mapsto\widetilde S_p$ of minimizers. No boundedness assumption on demand is made.

Milestones

1. (25), p. 24, for every demand law: $C(\widetilde S)-\mathrm{OPT}\le\theta\big(\mathbb E[(D-\widetilde S/m)^+]-\mathbb E[(\frac1m\sum_{i=1}^mD_i-\widetilde S/m)^+]\big)$.
2. Lemma 6, p. 22: if $\bar D<\infty$, some optimal policy has $x_{t,m}\ge\underline S$ in every period on every demand path.
3. (20), p. 22: such a policy outdates cumulatively at least as much as $\pi_{\underline S}$, pathwise.
4. Proposition 3, p. 22: if $\bar D<\infty$, $\mathrm{OPT}\ge h\mathbb E[(\underline S-D)^+]+\theta\mathbb E[O_\infty(\underline S)]$.
5. (EC.13), p. ec6: if $\bar D<\infty$, $p\mathbb E[(D-\widetilde S)^+]\le p(\bar D-\widetilde S)\mathbb P(D>\widetilde S)\le(h+\theta)(\bar D-\widetilde S)$.
6. (EC.15), p. ec6: $\mathbb E[O_\infty(S_2)]\le\mathbb E[O_\infty(S_1)]+S_2-S_1$ for $0\le S_1\le S_2$.
7. (26), p. 24: if $\bar D<\infty$, $C(\widetilde S)-\mathrm{OPT}\le(h+\theta)(\bar D-\underline S)$.

Significance

Theorem 3 shows that the explicitly computable policy $\pi_{\widetilde S}$ is asymptotically optimal in the high-service regime. The optimal policy is a function of the whole age vector, whereas $\widetilde S$ is the minimizer of a one-dimensional convex function. Together with the companion results of the paper, in the lifetime $m$, the demand population and the outdating cost $\theta$, this gives a uniform picture of when a single stock level suffices for a perishable product. Lemma 6 and Proposition 3 are of independent interest: a uniform floor on the optimal order-up-to level and a lower bound on the optimal average cost that does not require solving the dynamic program.

The result is proved in the paper; it has not been formalized. A machine-checked development requires a perishable inventory model, long-run average costs over an infinite i.i.d. demand path, and, for Lemma 6, the existence of an average-optimal policy. The last step requires a vanishing-discount argument.

Difficulty

The unbounded-demand case rests on (25). The lower bounds it combines (Lemma 2 and Proposition 2 of the paper) are posed in mission 1 of this series and only cited here. The bounded-demand case is harder. One would like to compare $\pi_{\widetilde S}$ with an optimal policy directly, but a priori there is no optimal policy at all: $\mathrm{OPT}$ is an infimum over a large class of state-feedback policies on a continuous state space. Lemma 6 asserts that the infimum is attained, and attained by a policy whose order-up-to level never drops below $\underline S$. The paper obtains it from the discounted problem (Nandakumar & Morton 1993) and a vanishing-discount limit, verifying the conditions of Schäl (1993, Theorem 3.8) and in particular a uniform bound on relative discounted values (EC.34). Schäl's theorem is posed separately on Prove2Me as a statement (SchalAvg.AvgOpt.theorem_3_8, not proved), which is context and not part of this mission. Bounding the lost-sales term by a quantity independent of $p$, as (EC.13) does, needs the first-order condition at a minimizer of $\widetilde C$, which is a non-smooth convex function.

Formalization scope

• Time is zero-based: Lean period $t$ is the paper's period $t+1$.
• State: Fin (m - 1) → ℝ of cumulative levels, with $x_{t,0}:=0$, so $m=1$ (empty state, everything left over outdates) is included, not excluded.
• Parameters: a record $(m,h,p,\theta)$ with the standing hypotheses $m\ge1$, $h>0$, $p>0$, $\theta\ge0$. In Theorem 3 only the field $p$ varies.
• Expectations and costs are lower Lebesgue integrals over the i.i.d. path law (CappedBaseStock.demandPathLaw), valued in $[0,\infty]$. Long-run averages are limsups of Cesàro averages.
• Policies: the class $\Pi$ of the paper: time-dependent, deterministic, measurable functions of the current state. $\mathrm{OPT}$ is the infimum over all of $\Pi$, not over base-stock policies.
• $C(S)$ is the simulated long-run average cost of $\pi_S$, not a formula. $\mathbb E[O_\infty(S)]$ is the long-run average outdating of $\pi_S$ from the empty state.
• $\widetilde S$ is any minimizer of $\widetilde C$; all statements quantify over every minimizer. $\underline S$ is the least minimizer of its function, the weaker choice for Lemma 6.
• Gaps "$A-\mathrm{OPT}\le B$" are stated as $A\le\mathrm{OPT}+B$ in $[0,\infty]$. The limit uses real values, which is faithful because $C_p(S)\le hS+p\mathbb E[D]+\theta S<\infty$.
• Lemma 6 requires an exactly optimal policy and a floor on every demand path.

Trivializing formalizations are ruled out. OPT is not restricted to base-stock policies, $C(S)$ is not defined by its formula (3), $\widetilde S$ is not replaced by a closed form, and $m$, $\theta$, $h$ and the demand law are kept general.

The FIFO lemmas the proof uses, namely Lemma 1, Lemma 2, Proposition 2 and the recursion (19), are posed in mission 1 of this series and are not restated. The development reuses the published demand layer CappedBaseStock_Model and the newsvendor functions LostSalesOrderUpTo.Asymptotic.Backorder. A general vanishing-discount theorem for Borel-state average-cost control would be reusable well beyond this mission; contributions toward it, and toward the convexity and first-order conditions of newsvendor-type costs, are welcome.

Selected references

• X. Bu, X. Gong, X. Chao, Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems, accepted manuscript, Management Science, 2022. SSRN 3724966, https://ssrn.com/abstract=3724966
• S. Nahmias, Perishable inventory theory: a review, Operations Research 30(4), 1982. https://doi.org/10.1287/opre.30.4.680
• P. Nandakumar, T. E. Morton, Near myopic heuristics for the fixed-life perishability problem, Management Science 39(12), 1993. https://doi.org/10.1287/mnsc.39.12.1490
• M. Schäl, Average optimality in dynamic programming with general state space, Mathematics of Operations Research 18(1), 1993. https://doi.org/10.1287/moor.18.1.163
• W. T. Huh, G. Janakiraman, J. A. Muckstadt, P. Rusmevichientong, Asymptotic optimality of order-up-to policies in lost sales inventory systems, Management Science 55(3), 2009. https://doi.org/10.1287/mnsc.1080.0945

Motivation

Public and nonprofit services such as food banks, shelters, free clinics and legal aid often run with too little capacity and serve two kinds of users: people with no alternative, and people who have a reasonable outside option. When the queue is long, a user who has an alternative but joins anyway imposes waiting costs on everyone behind them, including the users who cannot go elsewhere. Pricing is usually ruled out in such settings, which leaves the provider one lever: what it tells arriving users about congestion.

Anunrojwong, Iyer and Manshadi (arXiv:2005.07253v3; Management Science, 2023) study this lever as a Bayesian persuasion problem in a queue, building on the revenue-maximization model of Lingenbrink and Iyer (Operations Research 67(5):1397–1416, 2019). The natural benchmark is full information: announce the queue length and let users decide. This mission formalizes the paper's answer to when full information can be improved for both user types at once, and by how much.

Setting

A single server serves users first come, first served, with exponential service times of rate $1$. High-need users (type H) arrive as a Poisson stream of rate $\lambda_H\ge0$ and always join. Low-need users (type L) arrive at rate $\lambda_L>0$ and either join or take an outside option worth $0$. Write $\lambda=\lambda_L+\lambda_H\le1$. A type-$i$ user who joins with $n$ users already present receives utility $u_i(n)$. The standing assumptions are $u_i(0)>0$, $u_i(k)<0$ for some $k$, each $u_i$ strictly decreasing, and the increments $u_L(n)-u_L(n+1)$ non-increasing (Assumption 1).

By a revelation-principle argument (Lemma 1 of the paper, from Lingenbrink and Iyer), a recommendation mechanism that users obey is described by the queue's stationary distribution $\pi=(\pi_n)_{n\ge0}$. An admission policy is a distribution with $\lambda_H\pi_n\le\pi_{n+1}\le\lambda\pi_n$ for all $n$; their set is $\Pi_{AP}$. A signaling mechanism is an admission policy that also satisfies the obedience constraints

$$J(\pi)=\sum_{n\ge0}(\pi_{n+1}-\lambda_H\pi_n)u_L(n)\ge0,\qquad L(\pi)=\sum_{n\ge0}(\lambda\pi_n-\pi_{n+1})u_L(n)\le0,$$

called (JOIN) and (LEAVE); their set is $\Pi_{SM}$. The welfare of the two types is $W_L(\pi)=J(\pi)$ and $W_H(\pi)=\lambda_H\sum_n\pi_nu_H(n)$. A policy $\hat\pi$ Pareto-dominates $\pi$ if it is at least as good for both types and strictly better for one; $\pi$ is Pareto-efficient within a class if no member of the class dominates it.

A threshold policy $\pi_x$, $x=m+a\ge0$, admits L users when fewer than $m$ users are present, admits them with probability $a$ at $m$, and turns them away above $m$. Write $W_L(x)$, $W_H(x)$ and $L(x)$ for its welfare and (LEAVE) value. The full-information threshold $m_{fi}$ is the smallest $k$ with $u_L(k)<0$, and the full-information mechanism is $\mathsf{fi}=\pi_{m_{fi}}$.

Formalization targets

Goal: Proposition 3(1)–(2)

For $\lambda_H\in(0,1)$, with $u_L,u_H$ fixed, there is a threshold $\bar\Lambda_L(\lambda_H)\in(0,1-\lambda_H]$ such that some signaling mechanism Pareto-dominates $\mathsf{fi}$ if and only if $\lambda_L\ge\bar\Lambda_L(\lambda_H)$, and

$$\bar\Lambda_L(\lambda_H)\ \ge\ (1-\lambda_H)\,\frac{u_L(m_{fi}-1)}{u_L(0)-\sum_{k=1}^{m_{fi}-1}\lambda_H^k\big(u_L(k-1)-u_L(k)\big)}\ >\ 0 .$$

If moreover $\lambda<1$, $u_L(m_{fi}-1)\le W_L(\mathsf{fi})$, $u_H(m_{fi})\le W_H(\mathsf{fi})$, $L(m_{fi}-1)\le0$ and $W_H(\mathsf{fi})>0$, then a signaling mechanism $\mathsf{sm}$ exists with

$$W_L(\mathsf{sm})\ge\beta_{L,sm}W_L(\mathsf{fi}),\qquad W_H(\mathsf{sm})\ge\beta_{H,sm}W_H(\mathsf{fi}),$$

where $\beta_{L,sm}=1+\frac{\lambda_H(1-\lambda)\lambda_L\lambda^{m_{fi}-1}}{1-\lambda_H-\lambda_L\lambda^{m_{fi}-1}}>1$ and $\beta_{H,sm}=1+\frac{(1-\lambda_H)(1-\lambda)\lambda_L\lambda^{m_{fi}-1}}{1-\lambda_H-\lambda_L\lambda^{m_{fi}-1}}>1$.

Milestones

• Lemma 3: the geometric sandwich $\lambda_H^{k-q}\pi_q\le\pi_k\le\lambda^{k-q}\pi_q$ on $\Pi_{AP}$.
• Theorems 1 and 2: Pareto-efficient signaling mechanisms and admission policies have a threshold structure with threshold at most $m_{fi}$.
• Lemma 2: maximizers of $\theta W_L+(1-\theta)W_H$ exist.
• Theorem 3: when (LEAVE) is slack, efficiency within $\Pi_{SM}$ and within $\Pi_{AP}$ coincide.
• Lemma 5(1)–(2): $W_H(x)$ is strictly decreasing, and $W_L(x)$ is unimodal and monotone between consecutive integers.
• $\mathsf{fi}\in\Pi_{SM}$ with $L(\mathsf{fi})<0$.
• Theorem 4: exactly one of "$\mathsf{fi}$ is Pareto-efficient among admission policies" and "a signaling mechanism dominates $\mathsf{fi}$" holds, the first if and only if $W_L(m_{fi})>W_L(m_{fi}-1)$.
• From the proof of Proposition 3: the equivalence of that condition with $f(\lambda_L,\lambda_H)<0$, an identity for $W_L(m-1)$ and an inequality for $W_H(m-1)$, for $1\le m\le m_{fi}$.

Significance

The proposition gives a clean regime split. Full information is already Pareto-efficient when low-need demand is light. Once $\lambda_L$ crosses an explicit level, revealing everything leaves welfare on the table for both types, so a provider who cares about either group has a reason to hide some queue information. The lower bound on $\bar\Lambda_L$ is explicit in the primitives, and the factors $\beta_{L,sm},\beta_{H,sm}$ give a guaranteed improvement, not only an existence statement. Theorem 4, the milestone behind part 1, reduces the comparison to two adjacent thresholds.

The paper proves these results on paper. To our knowledge none of them has a machine-checked proof. A formal development checks the "little algebra" steps that the paper compresses (the equivalence with $f<0$, the welfare identities of p. 41–42). It also produces a reusable layer for persuasion in birth–death queues: obedient mechanisms as distributions, threshold policies, and Pareto efficiency within a class. The companion missions of this series (threshold structure, the homogeneous case, first-best) are stated over the same layer.

Difficulty

The threshold $\bar\Lambda_L$ comes from analysing the sign of $f(\cdot,\lambda_H)$ on $(0,1-\lambda_H]$. Translating "fi is not dominated" into that sign condition is where the work lies. The obvious attempt, comparing $\mathsf{fi}$ only with nearby threshold policies, settles one direction: if $W_L(m_{fi}-1)\ge W_L(m_{fi})$, the threshold $m_{fi}-1$ dominates. The converse needs every competitor in $\Pi_{AP}$, not just threshold policies. That requires the structure theorem for efficient admission policies, the existence of maximizers, and unimodality of $W_L$, followed by a transfer from $\Pi_{AP}$ to $\Pi_{SM}$ that only works because (LEAVE) is slack at $\mathsf{fi}$. The welfare series are infinite, and the threshold family is parametrised by a real $x$ whose fractional part enters nonlinearly, so the comparisons are not finite-dimensional linear algebra.

Formalization scope

Everything is stated over a structure Model with real fields $\lambda_L,\lambda_H$ and utilities $u_L,u_H:\mathbb N\to\mathbb R$, with a predicate Standing holding the standing assumptions ($\lim_ku_i(k)<0$ is encoded as $\exists k,\ u_i(k)<0$). Queue lengths are natural numbers, and the two types are separate fields. Membership in $\Pi_{AP}$ includes summability of $\pi_nu_L(n)$ and $\pi_nu_H(n)$: the paper treats all welfare as finite, and an unrestricted tsum would assign $0$ to divergent welfare. $W_L$ is the right-hand form of (2), with no division by $\lambda_L\pi_n$. A finite threshold requires $\pi\in\Pi_{AP}$, $\pi_m>0$ and a joining fraction in $[0,1]$, as in Definition 2. Threshold policies are defined from their unnormalised weights, $\mathsf{fi}$ is $\pi_{m_{fi}}$ as a distribution, and Pareto efficiency is Definition 1 within an explicit class. "Exactly one" is exclusive or.

Added hypotheses, each disclosed in the item that carries it:

1. Convergence of $\sum_n\lambda_H^nu_H(n)$. This is the finite-welfare convention, equivalent to $\Pi_{AP}\ne\emptyset$ when $\lambda_H>0$.
2. Lemma 2's hypothesis ($\lambda<1$, or $u_L,u_H\to-\infty$) wherever existence of maximizers is used.
3. $u_L(m_{fi}-1)\ne0$ in Proposition 3. Without it the claimed $\bar\Lambda_L>0$ is false.
4. $\lambda_H>0$ in Lemma 5(1) and Theorem 4, as required by §4.2's heterogeneous setting. For $\lambda_H=0$, $W_H\equiv0$, and Theorem 4's strict adjacent-threshold comparison can fail at a tie.

The page's range $\lambda_L\in[\bar\Lambda_L,1)$ is intersected with $\lambda\le1$. In part 2, "$\mathsf{sm}$" is read existentially.

Ruled out as trivializing: choosing $\bar\Lambda_L$ after $\lambda_L$ (the goal quantifies it once, with $\lambda_H,u_L,u_H$ fixed); defining $\mathsf{fi}$ through its welfare; replacing Pareto efficiency by maximization of a weighted welfare; replacing exclusive or by inclusive or; and any constant that differs from the page's $\beta_{L,sm}$, $\beta_{H,sm}$ or lower bound symbol for symbol.

A complete development needs geometric and arithmetico-geometric series, rearrangement of infinite sums over $\mathbb N$, and convexity arguments in the space of summable sequences. Proofs of any milestone are welcome, as are lemmas about threshold policies that the other missions of the series can reuse.

Selected references

• J. Anunrojwong, K. Iyer, V. Manshadi, Information Design for Congested Social Services: Optimal Need-Based Persuasion, Management Science, 2023; read as arXiv:2005.07253v3 (2022). https://arxiv.org/abs/2005.07253
• D. Lingenbrink, K. Iyer, Optimal Signaling Mechanisms in Unobservable Queues, Operations Research 67(5):1397–1416, 2019.
• E. Kamenica, M. Gentzkow, Bayesian Persuasion, American Economic Review 101(6), 2011. https://doi.org/10.1257/aer.101.6.2590
• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 5th ed., Wiley, 2018.

Motivation

Retailers and restaurants increasingly deliver orders from their own stores within an hour or less. Orders arrive throughout the day, a fixed pool of drivers is based at the store, and in each dispatch wave the operator must decide how many drivers to send out now and along which routes. Sending many drivers now gives short delivery times for the current orders but leaves few drivers for orders that arrive while those drivers are still on the road. Liu and Luo (arXiv:2107.13058, Manufacturing & Service Operations Management, 2023) model this trade-off as a finite-horizon stochastic dynamic program and propose a rollout policy built on a tractable approximation of its cost-to-go. Their Theorem 1 justifies the approximation: with suitable parameters it lies below the true expected cost-to-go, with other parameters it lies between that cost and the cost of any feasible simple policy, and in the last period it is exact. This mission formalizes that theorem.

Setting

A store (the depot $0$) serves a finite set $\mathcal I$ of customer locations over $N$ periods with strictly increasing decision epochs $t_1 < \dots < t_N$. A fleet of $\bar K$ drivers carries at most $Q$ items per trip; travel times $\tau(i,j) \ge 0$, an on-site service time $s \ge 0$ and a delivery target $L_{\max}$ are given. At epoch $t_n$ the operator observes the demand of period $n$: the set $\mathcal I^n \subseteq \mathcal I$ of locations with an order and the quantities $q^n_i$, drawn from a finitely supported law $\mathbb Q^n$, independently across periods.

The driver status $\zeta^n = (\zeta^n_1,\dots,\zeta^n_N)$ records how many drivers are still en route in each period $n'$ because of earlier dispatches, so $\bar K - \zeta^n_n$ drivers are available at $t_n$. A decision $Y^n$ is a set of depot-to-depot routes $0 \to i_1 \to \dots \to i_m \to 0$, one per dispatched driver. It is feasible if it uses at most $\bar K - \zeta^n_n$ drivers, serves every current order exactly once, loads at most $Q$ items per route, and delivers every order within $L_{\max}$. The delivery times are $u_{i_1} = \tau(0,i_1)$ and $u_{i_{k+1}} = u_{i_k} + s + \tau(i_k,i_{k+1})$; the cost of $Y^n$ is $\sum_{i \in \mathcal I^n} u_i(Y^n)$. A driver whose route lasts longer than $t_{n'} - t_n$ is counted as en route in period $n'$; this is the transition (9) from $\zeta^n$ to $\zeta^{n+1}$.

The cost-to-go $\mathcal H_n(\mathcal I^n, q^n, \zeta^n)$ is the minimum over feasible $Y^n$ of the period's cost plus $\mathbb E_{\mathbb Q^{n+1}}[\mathcal H_{n+1}]$ at the resulting status, with $\mathcal H_N$ the period cost alone ((7)–(8)). The single-period cost $\mathcal H^s(K, \mathcal I^n, q^n)$ is the minimum cost of serving the demand with at most $K$ drivers.

The approximation $\mathbf{APT}^n(\zeta^n)$ (10) replaces the future by single-period problems coupled only through driver counts:

$$V^n_{APT}(\zeta^n) = \min_{K^{n'} \in \mathbb N} \sum_{n'=n}^{N} \mathbb E_{\mathbb Q^{n'}}\big[\mathcal H^s(K^{n'}, \mathcal I^{n'}, q^{n'})\big] \ \ \text{s.t.}\ \ \sum_{m=n}^{n'} \omega^{n'}_m(K^m) \le \bar K - \zeta^n_{n'},\ \ n' = n,\dots,N,$$

where $\omega^{n'}_{n'}(K) = K$ and the nonnegative parameters $\omega^{n'}_m(K^m)$, $m < n'$, estimate how many of the $K^m$ drivers dispatched in period $m$ are still en route in period $n'$. A static myopic policy dispatches a state-independent number $K^{n',sm}$ of drivers in each period and routes them to minimize the single-period cost; it is feasible from $(n,\zeta^n)$ if it never asks for more drivers than are available and its single-period problems are always feasible.

Formalization targets

Goal: Theorem 1 (p. 13)

For $1 \le n \le N$ and a status with $\zeta^n_{n'} \le \bar K$:

$$\exists\,\omega:\ V^n_{APT}(\zeta^n;\omega) \le \mathbb E_{\mathbb Q^n}[\mathcal H_n], \qquad \forall\,\pi^{sm}\ \text{feasible}\ \exists\,\omega:\ \mathbb E_{\mathbb Q^n}[\mathcal H_n] \le V^n_{APT}(\zeta^n;\omega) \le J_n(\pi^{sm}),$$

and $V^N_{APT}(\zeta;\omega) = \mathbb E_{\mathbb Q^N}[\mathcal H_N(\cdot,\zeta)]$ for every $\omega$.

Milestones (Appendix D, pp. 34–35, and Lemma 1, p. 12)

1. With $\omega^{n'}_m \equiv 0$ for $m < n'$: $V^n_{APT} = \sum_{n'} \mathbb E[\mathcal H^s(\bar K - \zeta^n_{n'})] \le \mathbb E[\mathcal H_n]$.
2. For $n < N$ and a feasible static myopic policy: $\mathbb E[\mathcal H_n] \le J_n(\pi^{sm})$, and some $\omega$ gives $V^n_{APT} = J_n(\pi^{sm})$.
3. At $n = N$: $\mathbb E[\mathcal H_N] = \min_{K^N \le \bar K - \zeta^N_N} \mathbb E[\mathcal H^s(K^N,\cdot)]$.
4. Lemma 1: $\mathcal H_n$ and, for nonnegative $\omega$, $V^n_{APT}$ are nondecreasing in $\zeta^n$.

Significance

The rollout policy AJRP of the paper solves, at each epoch, the current routing problem together with $\mathbf{APT}^{n+1}$ as a stand-in for the future. Theorem 1 is what connects that stand-in to the dynamic program: it shows that the en route parameters move the approximation between a valid lower bound and the cost of an implementable policy, and its exactness part yields the paper's Corollary 1 (AJRP is optimal for $N = 2$). Lemma 1 shows the approximation keeps the monotonicity of the true value in the driver status.

The paper's proofs are in its Online Appendix (Appendix D). They are short but informal, and the formal statement here differs from the printed one in three pinned-down respects: the single-period cost is read with at most $K$ drivers, as the proofs use it; the upper bound is capped by the policy's cost, since otherwise it is vacuous; and the parameter choice printed for the upper bound has to be corrected in the last period. No part of the result has a machine-checked proof. A formal proof makes these readings definitive, and it produces a reusable Lean model of multi-period dispatching with routes, en route drivers and a Bellman recursion over a random demand.

Difficulty

Every part is a backward induction on the remaining periods, but the inductions run over a state that grows: the status $\zeta^{n+1}$ depends on the durations of the routes chosen in period $n$, and the infimum in (7) is over finite lists of routes, not over a finite action set. The lower bound needs that a larger status can only raise the cost; the upper bound needs that a policy which is feasible on its reachable states stays feasible after every realized demand. Exchanging the expectation with the minimum over the driver count in the last period is not a general fact and holds only because the single-period cost is nonincreasing in the number of available drivers. The obvious choice of parameters for the upper bound, the one printed in the proof, does not bound the last period's count and fails.

Formalization scope

Locations are a type with the depot as none; periods are 1-based natural numbers and every statement carries $1 \le n \le N$. Costs and values lie in $[0,\infty]$; every minimum is an infimum, equal to $+\infty$ on an empty feasible set; expectations are sums against the probability mass function of $\mathbb Q^n$. A decision is a list of nonempty routes covering the current orders exactly once. The parameters $\omega$ are nonnegative reals by their type, with the diagonal $\omega^{n'}_{n'}(K) = K$ written into (10). The available drivers in the dynamic program are $\bar K - \zeta^n_n$ in $\mathbb N$; in APT the right-hand side is the real $\bar K - \zeta^n_{n'}$.

Standing assumptions, shared by every statement: $N \ge 1$; strictly increasing epochs; finitely supported, period-independent demand laws; $q^n_i = 0$ off $\mathcal I^n$. Added hypothesis: $\zeta^n_{n'} \le \bar K$ for $n \le n' \le N$ (the en route drivers belong to the fleet). Disclosed readings: travel times do not depend on the period; delivery times follow the recursion of Appendix C with equality, starting from the depot leg; a policy's expected cost is defined recursively along its decisions.

Ruled out: defining $\mathcal H_N$ or $\mathcal H^s$ through the APT objective (exactness would become definitional); decision sets that may leave orders unserved (every cost would vanish); an upper bound without the cap by the policy's cost; negative parameters $\omega$.

The development needs the model and its recursion (provided as one definition file), monotonicity of $\mathcal H^s$ in $K$, and induction principles for the well-founded recursions. Proofs of the milestones in any order are welcome; Lemma 1 is not used by the paper's proof of Theorem 1 but is a natural first step.

Selected references

• S. Liu, Z. Luo, On-Demand Delivery from Stores: Dynamic Dispatching and Routing with Random Demand, Manufacturing & Service Operations Management, 2023; preprint arXiv:2107.13058v3, 2022. https://arxiv.org/abs/2107.13058
• W. B. Powell, Approximate Dynamic Programming: Solving the Curses of Dimensionality, 2nd ed., Wiley, 2011. https://doi.org/10.1002/9781118029176
• D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 4th ed., Athena Scientific, 2017 (rollout policies, Ch. 6).

Perishable inventory and the base-stock question

Blood platelets, fresh produce, dairy and many pharmaceuticals have a fixed shelf life: a unit that has not been used within $m$ periods of its arrival must be discarded. Managing such stock is a classical problem of inventory theory, going back to Nahmias (1975), and it remains of practical interest for hospital blood banks and grocery retail. The difficulty is structural. The state of the system is the whole age profile of the stock, a vector of dimension $m-1$, and the optimal policy depends on all of it. Dynamic programming over this state is intractable even for moderate lifetimes, so practice relies on simple heuristics, above all base-stock policies, which raise the total stock to a fixed level $S$ every period.

For decades the performance of base-stock policies in this system was understood only numerically. Chazan and Gal (1977) and Cooper (2001) bounded the long-run outdating of a base-stock policy; Nandakumar and Morton (1993) built a base-stock policy from bounds on the optimal order-up-to level and showed numerically that it performs close to optimal. Bu, Gong and Chao (SSRN 3724966, accepted by Management Science, 2022) give the first theoretical guarantees, comparing a simple base-stock policy with the optimal policy in several asymptotic regimes. This mission formalizes the first of them: the optimality gap decays exponentially in the lifetime $m$.

Setting

Time is discrete, $t=1,2,\dots$. Demands $D_1,D_2,\dots$ are i.i.d. copies of a nonnegative random variable $D$ with $0<\mathbb E[D]<\infty$ and distribution function $F(x)=\mathbb P(D\le x)$; $F^{-1}(x)=\inf\{y:F(y)\ge x\}$.

At the start of period $t$ the state is $\mathbf x_t=(x_{t,1},\dots,x_{t,m-1})$, where $x_{t,i}$ is the stock whose remaining lifetime is at most $i$ periods. The firm orders $q_t\ge0$, which arrives immediately and raises the total level to $x_{t,m}=x_{t,m-1}+q_t$ (with $x_{t,0}=0$). Demand is served oldest-first (FIFO issuance) and unmet demand is lost. Stock reaching the end of its life is outdated:

$$o_t=(x_{t,1}-D_t)^+,\qquad x_{t+1,i}=(x_{t,i+1}-D_t-o_t)^+,\quad i=1,\dots,m-1.$$

The system starts empty. Each period costs

$$C^\pi_t=h(x^\pi_{t,m}-D_t)^++p(D_t-x^\pi_{t,m})^++\theta o^\pi_t,$$

with holding cost $h>0$, lost-sales penalty $p>0$ and additional outdating cost $\theta\ge0$. A policy is admissible if each order is a nonnegative measurable function of the current state; $\Pi$ is the set of admissible policies. The long-run average cost is $C^\pi=\limsup_{T\to\infty}\frac1T\sum_{t=1}^T\mathbb E[C^\pi_t]$, and $\mathrm{OPT}=\inf_{\pi\in\Pi}C^\pi$.

The base-stock policy $\pi_S$ orders $(S-x_{t,m-1})^+$; its cost is $C(S)$. The heuristic level $\widetilde S$ is a minimizer over $[0,\infty)$ of

$$\widetilde C(S)=h\,\mathbb E[(S-D)^+]+p\,\mathbb E[(D-S)^+]+\frac\theta m\,\mathbb E\Big[\Big(S-\sum_{i=1}^mD_i\Big)^+\Big],$$

and $S^{NP}=F^{-1}(p/(p+h))$ is the newsvendor level.

Formalization targets

Goal: Theorem 1 (p. 11)

For every $\lambda>0$ and $m\ge1$,

$$C_m(\widetilde S_m)-\mathrm{OPT}_m\le\frac{(m-1)\theta}{\lambda me}\,e^{\lambda S^{NP}}\big(\mathbb E[e^{-\lambda D}]\big)^m .$$

The bound holds for every minimizer $\widetilde S_m$ and every demand law with positive finite mean. Since $\mathbb E[e^{-\lambda D}]<1$, the gap decays exponentially in $m$.

Milestones

1. (19), the FIFO outdating recursion $o^\pi_{t+m-1}=\big(x^\pi_{t,m}-\sum_{i=t}^{t+m-1}D_i-\sum_{j=t}^{t+m-2}o^\pi_j\big)^+$, for every admissible policy and every demand path.
2. Lemma 1: $C(S)=h\,\mathbb E[(S-D)^+]+p\,\mathbb E[(D-S)^+]+\theta\,\mathbb E[O_\infty(S)]$, with the long-run average outdating $\mathbb E[O_\infty(S)]$ the same from every initial state.
3. Lemma 2: $\frac1m\mathbb E[(S-\sum_{i\le m}D_i)^+]\le\mathbb E[O_\infty(S)]\le\min\{\mathbb E[(S/m-D)^+],\mathbb E[(S-\sum_{i\le m}D_i)^+]\}$.
4. (5): $F^{-1}(\frac p{p+h+\theta})\le\widetilde S\le F^{-1}(\frac p{p+h})$.
5. (15): $\sum_{i=t}^{t+m-1}o^\pi_i\ge(x^\pi_{t,m}-\sum_{i=t}^{t+m-1}D_i)^+$.
6. Proposition 2: $\mathrm{OPT}\ge\widetilde C(\widetilde S)$.
7. (21): $C(\widetilde S)-\mathrm{OPT}\le\frac{(m-1)\theta}m\,\mathbb E[(\widetilde S-\sum_{i\le m}D_i)^+]$.

Significance

Theorem 1 says that a single explicit base-stock level, computable from the demand law by a one-dimensional convex search, is nearly optimal once the lifetime is moderately long, with an explicit, distribution-dependent rate. It explains why the non-perishable newsvendor intuition carries over to long-lived products, and it is the first of seven guarantees in the paper. Its ingredients are reused throughout: Lemmas 1 and 2, Proposition 2 and the gap bound (21) are posed in this mission and used, without restatement, by missions 2 to 4 of this series (demand population size, penalty cost, outdating cost).

The result is proved on paper; nothing about perishable inventory has been machine-checked. A formal development would provide a reusable model of FIFO perishable dynamics with long-run average costs, sample-path inequalities for outdating, and the first verified optimality-gap bound for an inventory heuristic in a high-dimensional state space.

Difficulty

Most of the argument is sample-path bookkeeping plus Jensen's inequality, but two steps are not routine. Lemma 1 asserts that the long-run average outdating of $\pi_S$ exists and does not depend on the initial state. The natural route through a stationary distribution fails: when $\mathbb P(D<S/m)=1$ the chain can be periodic and has no steady state, so the identity must hold for Cesàro averages directly; in the aperiodic case the paper uses a minorization condition (Meyn and Tweedie, Theorem 16.0.2). Proposition 2 compares every admissible policy with the heuristic cost, which needs the independence of the order-up-to level $x^\pi_{t,m}$ from current and future demands, and a conditional Jensen step for nonlinear expectations of a policy-dependent quantity.

Formalization scope

The Lean development fixes the following conventions.

• Time is zero-based: Lean period $t$ is the paper's period $t+1$.
• The state is Fin (m - 1) → ℝ holding the cumulative levels, with $x_{t,0}=0$, so $m=1$ (empty state, all leftover stock outdates) is included; $m\ge1$, $h>0$, $p>0$, $\theta\ge0$ are fields of the parameter record.
• Base-stock levels range over $[0,\infty)$ (ℝ≥0).
• The trajectory is a recursion on the demand path, so the state of period $t$ depends only on $D_1,\dots,D_{t-1}$.
• Costs and averages take values in $[0,\infty]$; expectations are lower Lebesgue integrals over the i.i.d. path law; averages run over $T+1$ periods, which has the same limsup.
• $\Pi$ is the paper's class: time-dependent measurable state-feedback orders.
• $\mathbb E[O_\infty(S)]$ is the long-run average expected outdating of $\pi_S$ from the empty state.
• "$\widetilde S$ is a minimizer" is a predicate, and the goal, (21) and Proposition 2 quantify over every minimizer; the upper half of (5) is stated for the least minimizer.
• Gaps are written $C(\widetilde S)\le\mathrm{OPT}+B$, equivalent to the paper's form since $\mathrm{OPT}\le C(0)<\infty$.
• (15) and Proposition 2 are stated for FIFO only, although the paper states them for any issuance policy.
• The demand law and the newsvendor functions are the published definitions CappedBaseStock_Model and LostSalesOrderUpTo.Asymptotic.Backorder.

Trivializing readings are excluded: $C(S)$ is the simulated cost of $\pi_S$, not a formula; $\mathrm{OPT}$ ranges over all admissible policies, not only base-stock ones; $\widetilde S$ is the argmin predicate, not a closed form; $m$, $\theta$ and the demand law are general; and no gap is stated with truncated subtraction. Contributions of any of the milestones, of general facts about Cesàro limits of Markov chains, or of the convexity of $\widetilde C$, are welcome.

Selected references

• J. Bu, X. Gong, X. Chao, Asymptotic Optimality of Base-Stock Policies for Perishable Inventory Systems, Management Science, 2022 (accepted manuscript, SSRN 3724966). https://ssrn.com/abstract=3724966
• D. Chazan, S. Gal, A Markovian model for a perishable product inventory, Management Science 23(5), 1977. https://doi.org/10.1287/mnsc.23.5.512
• W. L. Cooper, Pathwise properties and performance bounds for a perishable inventory system, Operations Research 49(3), 2001. https://doi.org/10.1287/opre.49.3.455.11221
• S. Nahmias, Optimal ordering policies for perishable inventory—II, Operations Research 23(4), 1975. https://doi.org/10.1287/opre.23.4.735
• P. Nandakumar, T. E. Morton, Near myopic heuristics for the fixed-life perishability problem, Management Science 39(12), 1993. https://doi.org/10.1287/mnsc.39.12.1490
• S. P. Meyn, R. L. Tweedie, Markov Chains and Stochastic Stability, Springer, 1993. https://doi.org/10.1007/978-1-4471-3267-7

Motivation

Best subset selection fits a linear model using at most $k$ of $p$ candidate predictors. When the noise level is high relative to the signal, it overfits. Mazumder, Radchenko and Dedieu (arXiv:1708.03288v4; Operations Research, 2023) add a shrinkage penalty $\lambda\|\beta\|_q$, $q\in\{1,2\}$, to the best-subsets problem and prove oracle inequalities for the resulting estimators. Their main error bounds (Theorems 2–5) are proved in the same way: a deterministic argument shows the bound holds whenever the noise vector lies in one of four explicit sets, and a separate probabilistic result shows that each set has probability close to one. This mission formalizes that probabilistic result, Theorem 1 of the paper (p. 13, proof in Supplement B.1, pp. 38–39).

The four events combine several tools of high-dimensional statistics. The event $\mathcal F$ controls the noise through a sorted-$\ell_1$ (SLOPE-type) norm; its probability bound is Theorem 4.1 of Bellec, Lecué and Tsybakov, Slope meets Lasso (Ann. Statist. 2018). The event $\mathcal G_s$ is a sparse version of a $\chi^2$ deviation bound, adapted from Lemma 8 of Raskutti, Wainwright and Yu (IEEE Trans. Inf. Theory 2011). The event $\mathcal H$ is the classical Gaussian maximal inequality behind Lasso and Dantzig-selector analyses.

Setting

Observations follow the model

$$y = f^* + \epsilon \qquad (15)$$

in $\mathbb R^n$. The mean $f^*$ is deterministic and unknown. The noise $\epsilon$ has independent $N(0,\sigma^2)$ coordinates, with $\sigma>0$. The design $X\in\mathbb R^{n\times p}$ is deterministic, and its columns have unit Euclidean norm.

For $u\in\mathbb R^p$, $\|u\|$ is the Euclidean norm, $\|u\|_1$ the $\ell_1$ norm, $\|u\|_\infty$ the largest absolute coordinate, and $\|u\|_0$ the number of non-zero coordinates. For an integer $s\in[p]=\{1,\dots,p\}$, $B_0(s)=\{u\in\mathbb R^p:\|u\|_0\le s\}$. The non-increasing rearrangement $u^\sharp_1\ge\dots\ge u^\sharp_p$ lists $|u_1|,\dots,|u_p|$ in non-increasing order. Logarithms are natural, and $\delta_0\in(0,1]$ is a confidence parameter.

The four events (p. 13) are sets of noise vectors:

$$\mathcal E_s=\bigl\{\epsilon^\top Xu\le[4+\sqrt2]\,\sigma\sqrt{s\log(2ep/s)}\,\|u\|,\ \forall u\in B_0(s)\bigr\},$$ $$\mathcal F=\Bigl\{\epsilon^\top Xu\le[4+\sqrt2]\,\sigma\max\Bigl(\sum_{j=1}^p u^\sharp_j\sqrt{\log(2p/j)},\ \sqrt{\log(1/\delta_0)}\,\|Xu\|\Bigr),\ \forall u\in\mathbb R^p\Bigr\},$$ $$\mathcal G_s=\bigl\{\epsilon^\top Xu\le\sigma\sqrt{5s\log(ep/s)+\log(1/\delta_0)}\,\|Xu\|,\ \forall u\in B_0(s)\bigr\},$$ $$\mathcal H=\bigl\{\|X^\top\epsilon\|_\infty\le\sigma\sqrt{2\log(2p)}+\sigma\sqrt{2\log(1/\delta_0)}\bigr\}.$$

Formalization targets

Goal: Theorem 1 (with the $\mathcal G_s$ part corrected)

For $s\in[p]$ and $\delta_0\in(0,1]$:

$$\mathbb P(\mathcal E_s)\ge1-\frac{s}{4ep},\qquad\mathbb P(\mathcal F)\ge1-\frac{\delta_0}2,\qquad\mathbb P(\mathcal G'_s)\ge1-\delta_0,\qquad\mathbb P(\mathcal H)\ge1-\delta_0,$$

where $\mathcal G'_s$ is $\mathcal G_s$ with $3\log(1/\delta_0)$ in place of $\log(1/\delta_0)$ under the root. Each event is also asserted to be measurable.

The printed claim $\mathbb P(\mathcal G_s)\ge1-\delta_0$ is false. Take $n=p=s=1$ and $X=[1]$. Then $\mathcal G_s=\{|\epsilon|\le\sigma\sqrt{5+L}\}$ with $L=\log(1/\delta_0)$, and $\mathbb P(\mathcal G_s^c)=2\bar\Phi(\sqrt{5+L})$, which exceeds $e^{-L}=\delta_0$ once $L\ge9$. The corrected constant $3$ is what the argument the paper cites actually gives. Downstream, the paper uses $\mathbb P(\mathcal G_s)$ only inside inequalities that hold up to universal constants, so the correction does not affect its other results.

Milestones

The proof in B.1 is followed step by step:

1. (27): $\|Xu\|\le\|u\|_1\le\sqrt s\|u\|$ on $B_0(s)$, and at $\delta_0=s/(2ep)$, $\sqrt{\log(1/\delta_0)}\|Xu\|\le\sqrt{s\log(2ep/s)}\|u\|$;
2. $\log(s!)\ge s\log(s/e)$, referenced from the platform as $(s/e)^s\le s!$;
3. $\sum_{j=1}^s\log(2p/j)=s\log(2p)-\log(s!)\le s\log(2ep/s)$;
4. (28): $\sum_j u^\sharp_j\sqrt{\log(2p/j)}\le\|u\|\sqrt{\sum_{j\le s}\log(2p/j)}\le\sqrt{s\log(2ep/s)}\|u\|$ on $B_0(s)$;
5. $\mathcal F\subseteq\mathcal E_s$ when $\delta_0=s/(2ep)$;
6. $\mathbb P(\mathcal F)\ge1-\delta_0/2$;
7. $\mathbb P(\mathcal H)\ge1-\delta_0$;
8. $\mathbb P(\mathcal G'_s)\ge1-\delta_0$.

Significance

The result. Theorem 1 is the only probabilistic input to the paper's statistical theory. Theorem 2 ($\ell_2$ shrinkage) is proved on $\mathcal E_{2k}$, $\mathcal F$ and $\mathcal G_{2k}$. Theorem 3 ($\ell_1$ shrinkage) uses $\mathcal H$ as well. The lower bound for best subsets (Theorem 4) and the BIC-type choice of $k$ (Theorem 5) also rely on $\mathcal G_s$. Every high-probability bound and every expected-error bound in §3 is obtained by combining a deterministic inequality with this theorem. The event $\mathcal F$ is also of independent use: it gives the sorted-$\ell_1$ control of Gaussian noise used in SLOPE and Lasso analyses.

Formalizing it. All four bounds are known results; the mission formalizes them. The deterministic reduction $\mathcal F\subseteq\mathcal E_s$ is elementary. The three probability bounds need Gaussian machinery: a sorted-$\ell_1$ deviation bound (the hardest part), a $\chi^2$ tail bound with a union over supports, and a Gaussian maximal inequality. None of these has a machine-checked proof in Mathlib for this setting. The formal statement of the $\mathcal G_s$ bound with its corrected constant is a contribution of its own, because the printed form is false.

Difficulty

The $\mathcal E_s$ and $\mathcal H$ parts are routine once the Gaussian tools exist. The $\mathcal G'_s$ part is a uniform statement over all $\binom ps$ supports at once, and the explicit constants $5$ and $3$ leave no room for a lossy tail bound: a generic sub-Gaussian estimate does not reach them.

The $\mathcal F$ part is the hardest. It is uniform over all of $\mathbb R^p$, not over a sparse set. A union bound over the coordinates of $X^\top\epsilon$ gives the flat weight $\sqrt{\log p}$ on every coordinate, not the decreasing weights $\sqrt{\log(2p/j)}$, and it does not produce the explicit constant $4+\sqrt2$. The bound of Bellec, Lecué and Tsybakov has to be formalized in full, under this paper's normalization (unit columns rather than columns of norm $\sqrt n$).

Formalization scope

• Model. Vectors are functions Fin n → ℝ, and $X$ is Matrix (Fin n) (Fin p) ℝ with unit columns ($\sum_i X_{ij}^2=1$). Mathlib's default norm on Fin m → ℝ is the sup norm, so the Euclidean, $\ell_1$, $\ell_\infty$ and $\ell_0$ norms are explicit definitions. Indices are 0-based: j : Fin p stands for the paper's $j+1$.
• Probability space. The probability space is $\mathbb R^n$ with the product law $N(0,\sigma^2)^{\otimes n}$ of $\epsilon$ (the model (15)). Events are sets of noise vectors defined by the printed inequalities, quantified over all $u$ in the stated range. Probabilities are taken as real numbers, and measurability of each event is part of each conclusion, not a hypothesis.
• Sorted sum. $\sum_j u^\sharp_j\sqrt{\log(2p/j)}$ is encoded as the maximum over all permutations $\pi$ of $\sum_j|u_{\pi(j)}|\sqrt{\log(2p/j)}$. The weights are non-negative and non-increasing for $j\le p$, so by the rearrangement inequality this equals the paper's sum. Summing $|u_j|$ in index order would be a different, smaller quantity.
• Constants. Every constant is the printed one ($4+\sqrt2$, $2ep$, $5s\log(ep/s)$, $\sqrt{2\log(2p)}$, $s/(4ep)$, $\delta_0/2$), except the disclosed $3$ in $\mathcal G'_s$.
• Hypotheses. The theorem assumes $1\le s\le p$, $0<\delta_0\le1$, $\sigma>0$ and unit columns. The $\mathcal E_s$ bound has no free $\delta_0$: it is the $\mathcal F$ bound at $\delta_0=s/(2ep)$.
• Ruled-out trivializations. None of the following is a faithful formalization: replacing the max in $\mathcal F$ by a sum, dropping "$\forall u\in B_0(s)$", replacing $u^\sharp$ by $|u|$ in index order, or taking the probability of a set not proved measurable.
• Not formalized. The oracle inequalities (Theorems 2–5, the other missions of this series), Corollaries 1–6, Propositions 1–4 and the numerics.
• Infrastructure needed and reusable. A complete development needs Gaussian rotation invariance, $\chi^2$ tails, Gaussian concentration for Lipschitz functions, and a sorted-$\ell_1$ deviation bound. All of these are reusable well beyond this mission, and proofs of any milestone are welcome.

Selected references

• R. Mazumder, P. Radchenko, A. Dedieu, Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low, Operations Research, 2023; arXiv:1708.03288v4 (the version formalized). https://arxiv.org/abs/1708.03288
• P. C. Bellec, G. Lecué, A. B. Tsybakov, Slope meets Lasso: improved oracle bounds and optimality, Annals of Statistics 46(6B), 2018. https://doi.org/10.1214/17-AOS1670
• G. Raskutti, M. J. Wainwright, B. Yu, Minimax rates of estimation for high-dimensional linear regression over ℓq-balls, IEEE Transactions on Information Theory 57(10), 2011. https://doi.org/10.1109/TIT.2011.2165799
• B. Laurent, P. Massart, Adaptive estimation of a quadratic functional by model selection, Annals of Statistics 28(5), 2000. https://doi.org/10.1214/aos/1015957395