Operations Research

Motivation

Best subset selection fits a linear model using at most $k$ of $p$ available predictors: it minimizes the residual sum of squares $\|y-X\beta\|^2$ over all $\beta$ with at most $k$ nonzero coordinates. It is the classical benchmark for sparse regression, and mixed-integer optimization has made it computable at scales that used to be out of reach (Bertsimas, King & Mazumder, 2016). When the signal-to-noise ratio is low, however, best subsets overfits, and Mazumder, Radchenko & Dedieu propose to add a shrinkage penalty $\lambda\|\beta\|_q$ ($q\in\{1,2\}$) to it. Their oracle inequalities for the penalized estimators hold for a fixed model size $k$, and the practitioner still has to choose $k$.

§3.5 of the paper removes that choice. It replaces the cardinality constraint with BIC-type penalties that depend on the candidate model size, and Theorem 5 shows that the resulting estimators satisfy oracle inequalities for the expected prediction error over all of $\mathbb R^p$, with no condition on the design beyond the normalization of its columns. This mission formalizes Theorem 5 and the steps of its printed proof.

Setting

We observe $y=f^*+\epsilon\in\mathbb R^n$. The mean $f^*\in\mathbb R^n$ is deterministic and unknown, and $\epsilon$ has independent $N(0,\sigma^2)$ entries with $\sigma>0$. The design $X\in\mathbb R^{n\times p}$ is deterministic, with $p\ge1$ and columns of unit Euclidean norm. The prediction error of an estimate $\hat\beta$ is $\|f^*-X\hat\beta\|^2$. For $\beta\in\mathbb R^p$, $\|\beta\|$ is the Euclidean norm, $\|\beta\|_1=\sum_j|\beta_j|$, and $\|\beta\|_0$ is the number of nonzero coordinates.

For nonnegative tuning parameters $a$ and $b$, the data-dependent penalties are

$$\lambda_\beta=a\sqrt{\|\beta\|_0\log(ep/\|\beta\|_0)},\qquad \mu_\beta=b\log(ep/\|\beta\|_0),$$

with the convention $0\cdot\infty=0$, so the empty model is not penalized. The BIC-type estimators are

$$\hat\beta^B_2\in\arg\min_{\beta}\ \|y-X\beta\|^2+\lambda_\beta\|\beta\|+\mu_\beta\|\beta\|_0,\qquad \hat\beta^B_1\in\arg\min_{\beta}\ \|y-X\beta\|^2+\lambda\|\beta\|_1+\mu_\beta\|\beta\|_0,$$

where $\lambda\ge0$ is a fixed number. Both are unconstrained problems. Solving them is equivalent to solving the constrained problems with $\|\beta\|_0\le k$ for each $k$ and then choosing $k$ by the penalty. A minimizer exists but need not be unique.

The proof works on events of the noise vector. For an integer $s$ and $\delta_0\in(0,1]$ the event $G'_s$ requires

$$\epsilon^\top Xu\le\sigma\sqrt{5s\log(ep/s)+3\log(1/\delta_0)}\,\|Xu\|\qquad\text{for every }u\text{ with }\|u\|_0\le s .$$

Formalization targets

Goal: Theorem 5 (p. 21)

There exist universal constants $a_0,b_0,c_0$ such that, if $a\ge a_0\sigma$ or $b\ge b_0\sigma^2$,

$$\mathbb E\|f^*-X\hat\beta^B_2\|^2\lesssim\inf_{\beta\in\mathbb R^p}\Big[\|f^*-X\beta\|^2+\lambda_\beta\|\beta\|+\mu_\beta\|\beta\|_0\Big]+\sigma^2,$$

and, if $\lambda\ge c_0\sigma\sqrt{\log(ep)}$ or $b\ge b_0\sigma^2$,

$$\mathbb E\|f^*-X\hat\beta^B_1\|^2\lesssim\inf_{\beta\in\mathbb R^p}\Big[\|f^*-X\beta\|^2+\lambda\|\beta\|_1+\mu_\beta\|\beta\|_0\Big]+\sigma^2 .$$

Here $\lesssim$ hides one universal multiplicative constant. The constants are not specified, so the goal records the shape of the bound and is not invalidated by later improvements of the constants.

Milestones (proof of Theorem 5, B.13, and B.5)

1. (51): the deterministic basic inequality for $\hat\beta^B_2$.
2. (54): for $a\gtrsim\sigma$, with probability at least $1-\delta_0/2$, $\|f^*-X\hat\beta\|^2+\mu_{\hat\beta}\|\hat\beta\|_0\lesssim\|f^*-X\beta\|^2+\lambda_\beta\|\beta\|+\sigma^2\log(1/\delta_0)+\mu_\beta\|\beta\|_0$.
3. The union bound over model sizes: with $G=\bigcap_{s=1}^pG'_s$, where $G'_s$ is taken at $\delta_0=(s/[ep])^s\epsilon_0$, we have $P(G^c)\le\epsilon_0$.
4. (55): for $b\gtrsim\sigma^2$, the analogue of (54) with probability at least $1-\epsilon_0$.
5. (56): under either condition, the high-probability oracle inequality with $\inf_\beta$ and $\sigma^2\log(1/\delta_0)$.
6. The tail-to-expectation step of B.5: if $W\le\kappa\log(1/\delta_0)$ with probability at least $1-\delta_0/2$, then $\mathbb EW^+\le\kappa/2$.
7. (58): the high-probability counterpart of (56) for $\hat\beta^B_1$.

Significance

The result. Theorems 2 and 3 of the paper give oracle inequalities only over the sparsity class $\{\|\beta\|_0\le k\}$ for a $k$ fixed in advance. Theorem 5 makes the model size data-driven. Its bounds hold over all of $\mathbb R^p$ and need no restricted-eigenvalue or sparse-eigenvalue condition on $X$. Corollary 6 of the paper deduces from it that the estimators attain the error rates of Corollaries 3 and 4 while selecting models of the same order as the true model size. The paper also notes that the slow-rate bound for $\hat\beta^B_1$ with $b=0$ is a bound for the Lasso.

Formalizing it. Theorem 5 is a published result with a printed proof (Supplement B.13). The proof is written up to unspecified universal constants, and it defers two steps to other parts of the paper ("repeating the argument after inequality (32)" and "repeating the argument in the proof of Corollary 3"). A formal proof makes every constant and every deferred step explicit. No part of the paper has been machine-checked, to the best of our search.

Difficulty

The argument is long rather than deep. The obvious first attempt fixes the selected model size $\hat k=\|\hat\beta\|_0$ and applies a high-probability bound for that size. This fails because $\hat k$ is random and depends on $\epsilon$, so a bound for each fixed $s$ says nothing about the random $\hat k$. The noise term must be controlled simultaneously over all model sizes, at a total failure probability that does not grow with $p$. The second obstacle is the passage from high-probability bounds, which hold for every $\delta_0$ and grow like $\log(1/\delta_0)$, to a bound in expectation. That passage needs the high-probability statement with a constant that is uniform in $\delta_0$.

Formalization scope

• Representation. Vectors are Fin n → ℝ and Fin p → ℝ, and the design is a Matrix (Fin n) (Fin p) ℝ.

  • The norms $\|\cdot\|$, $\|\cdot\|_1$ and $\|\cdot\|_0$ are explicit definitions (l2, l1, l0), because Mathlib's norm on Fin m → ℝ is the sup norm.
  • The noise law is the product of $n$ centred Gaussians with variance $\sigma^2$ (noiseLaw).
  • Logarithms are natural, and $e=\exp(1)$.

• Model. The standing hypotheses are:

  • unit-norm columns of $X$;
  • $\sigma>0$ and $p\ge1$;
  • $a,b\ge0$, and $\lambda\ge0$ for $\hat\beta^B_1$.

  The quantities $X$, $f^*$, $\sigma$, $a$, $b$, $\lambda$ and the penalties are inputs. The randomness is the law of $\epsilon$ alone, and $y=f^*+\epsilon$.

• Estimators are argmin predicates IsBIC2, IsBIC1: "$\hat\beta$ minimizes the objective over all of $\mathbb R^p$". Every statement holds for every minimizer.

  • In Theorem 5 an estimator is a measurable map $y\mapsto\hat\beta(y)$ that is a minimizer for every $y$, and the bound is claimed for every such selection.
  • The expectation is a lower Lebesgue integral in $[0,\infty]$, so a non-integrable error cannot make the bound vacuous.

• Constants.

  • "$\lesssim$" is one universal constant $C>0$, quantified before every other parameter.
  • "$\inf_\beta[\dots]$" is written as "for every $\beta$".
  • "With probability at least $1-\delta$" is the existence of a measurable event of probability at least $1-\delta$ on which the inequality holds.
  • The constants $a_0$, $b_0$ and $c_0$ carry no sign, as on the page.

• Correction. Theorem 1 of the paper states $P(G_s)\ge1-\delta_0$ for an event with coefficient $1$ on $\log(1/\delta_0)$. That bound is false for small $\delta_0$ (already for $n=p=s=1$). The union bound here uses the corrected event $G'_s$ with coefficient $3$, which inside $\lesssim$ changes nothing downstream.

• Ruled out. None of the following counts as a formalization of the goal:

  • an arbitrary or non-measurable selection of the minimizer;
  • a Bochner integral, which is $0$ for a non-integrable error;
  • a constant that depends on $n$, $p$, $\delta_0$ or the design;
  • a fixed $\delta_0$ or $\epsilon_0$.

• Not formalized here. The fixed-$k$ oracle inequalities (Theorems 2 and 3), the noise events of Theorem 1, the lower bound (Theorem 4), Corollaries 1–6 and the numerical study are not part of this mission. Some of them are the subjects of the other missions of this series. The proof of Theorem 5 needs the probability bounds for the events $F$ and $G'_s$ of Theorem 1 and the deterministic arguments of Theorems 2 and 3. A solver may prove them here or import them once they are published.

• Contributions welcome.

  • Gaussian chi-square tail bounds (Laurent–Massart);
  • the bound for the sorted-$\ell_1$ event $F$ (Bellec, Lecué & Tsybakov);
  • the existence of measurable selections of the argmin;
  • the layer-cake step.

  These are reusable well beyond this paper.

Selected references

• R. Mazumder, P. Radchenko, A. Dedieu, Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low, arXiv:1708.03288v4, 2022; Operations Research, 2023. https://arxiv.org/abs/1708.03288
• D. Bertsimas, A. King, R. Mazumder, Best subset selection via a modern optimization lens, Annals of Statistics 44(2), 2016. https://doi.org/10.1214/15-AOS1388
• 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
• 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
• L. Birgé, P. Massart, Gaussian model selection, Journal of the European Mathematical Society 3, 2001. https://doi.org/10.1007/s100970100031

Why a lower bound for best subsets

Best subset selection fits a linear model by least squares using at most $k$ of $p$ available predictors. It is the classical $\ell_0$-constrained estimator of sparse regression. Mixed-integer optimization now computes it for problems with thousands of variables (Bertsimas, King & Mazumder 2016), so its statistical behaviour matters in practice. Simulations in Hastie, Tibshirani & Tibshirani 2020 found that it predicts worse than shrinkage methods such as the Lasso when the signal-to-noise ratio (SNR) is low.

Mazumder, Radchenko and Dedieu (arXiv:1708.03288v4; Operations Research, 2023) add an $\ell_1$ or $\ell_2$ shrinkage penalty to best subsets. They prove upper bounds of two kinds: slow rates, linear in the tuning parameter $\lambda$, and fast rates, quadratic in $\lambda$. Theorems 2 and 3 of the paper give them for the shrunken estimators. For best subsets, the paper only has a fast-rate bound, of order $\sigma^2 k\log(ep/k)$. When $\|\beta^*\|/\sigma$ is small, the shrunken estimators' slow rate beats that bound. Theorem 4, the goal of this mission, shows that the comparison is meaningful: in that regime best subsets really does incur an error of the order of its upper bound.

Setting

The data follow the linear model

$$y = X\beta^* + \epsilon ,\qquad y,\epsilon\in\mathbb R^n,\ \beta^*\in\mathbb R^p ,$$

where the design $X$ is a deterministic real $n\times p$ matrix whose columns have unit Euclidean norm. The noise $\epsilon$ has independent $N(0,\sigma^2)$ entries, with $\sigma>0$. Write $\|v\|$ for the Euclidean norm, $\|v\|_1=\sum_i|v_i|$, $\operatorname{supp}(v)=\{i:v_i\ne0\}$ and $\|v\|_0=|\operatorname{supp}(v)|$. The $\ell_0$ ball is $B_0(s)=\{u\in\mathbb R^p:\|u\|_0\le s\}$. The minimal $s$-sparse eigenvalue of $X$ is

$$\gamma_s=\min_{u\ne0,\ u\in B_0(s)}\frac{\|Xu\|}{\|u\|} .$$

A best-subsets solution of size $k$ is any minimizer

$$\hat\beta_{\ell_0}\in\arg\min\ \|y-X\beta\|^2\quad\text{s.t.}\quad\|\beta\|_0\le k .\tag{1}$$

A constant is universal if it does not depend on $n,p,k,X,\sigma,\beta^*$. The symbols $\lesssim$ and $\gtrsim$ mean $\le$ and $\ge$ up to positive universal factors. Logarithms are natural, and $e=\exp(1)$.

Formalization targets

Goal: Theorem 4 (p. 18)

There are universal constants $c_0,c,C>0$ such that the following holds. Suppose $2\le k\le p$, $\|\beta^*\|_0\le k$ and $\|\beta^*\|\le c_0\sigma\gamma_k\sqrt{k\log(ep/k)}$. Then, with probability at least $1-2(ep/k)^{-c\gamma_k^2k}-(ep/k)^{-k}$, every best-subsets solution satisfies

$$\|X\hat\beta_{\ell_0}-X\beta^*\|^2\ \ge\ C\,\sigma^2\gamma_k^2\,k\log(ep/k).$$

The constants are left unfixed, as in the paper. The statement asserts the order of the error, which is what the comparison with the upper bounds needs.

Milestones

1. Maurey approximation (p. 44). For unit columns and every $\beta^*$, some $\tilde\beta^*$ with $\|\tilde\beta^*\|_0\le k/2$ has $\|X\beta^*-X\tilde\beta^*\|^2\le2\|\beta^*\|_1^2/k$.
2. (39) (p. 44). With $\Delta^*=X\beta^*-X\tilde\beta^*$, define $G(\beta)=\|y-X\beta\|^2-\|y-X\tilde\beta^*\|^2$ and $H(u)=\|Xu\|^2-2(\Delta^*+\epsilon)^\top Xu$. Then $G(\beta)$ equals $\|X\beta-X\tilde\beta^*\|^2+2(\Delta^*+\epsilon)^\top(X\tilde\beta^*-X\beta)$, and $\min_{\|\beta\|_0\le k}G\le\min H(u)$ over $u$ supported off $\operatorname{supp}(\tilde\beta^*)$ with $\|u\|_0\le k/2$.
3. (40) (p. 45). $\min_{\|\beta\|_0\le k}G(\beta)\le-\max_{v\in\mathcal V_k}|(\Delta^*+\epsilon)^\top Xv|^2$, where $\mathcal V_k$ is the set of $v$ supported off $\operatorname{supp}(\tilde\beta^*)$ with $\|v\|_0\le k/2$ and $\|Xv\|=1$.
4. Lemma 1 (p. 44). Let $S$ have $q$ elements and let $s\in[1,q]$ be an integer. Then $\max|\epsilon^\top Xv|\gtrsim\sigma\gamma_{2s}\sqrt{s\log(eq/s)}$ over $\operatorname{supp}(v)\subseteq S$, $\|v\|_0\le s$, $\|Xv\|=1$, with probability at least $1-2(eq/s)^{-\tilde c\gamma_{2s}^2s}$.

Significance

Theorem 4 matches the fast-rate upper bound for best subsets from Corollary 1 of the paper. When $\gamma_k$ is bounded below, the prediction error of best subsets is of exact order $\sigma^2k\log(ep/k)$ in the low-SNR regime (Remark 10). This is the theoretical counterpart of the empirical observation that best subsets overfits at low SNR. It is also what makes the paper's case for shrinkage a theorem rather than a comparison of upper bounds. The paper's Proposition 4 applies it to a concrete correlated design, where it gives a ratio of prediction errors between best subsets and its $\ell_2$-shrunken version that grows with $k$.

The result is proved in the paper; this mission formalizes it. No formalization of this result exists on the platform. The mission also produces a reusable Gaussian lower bound on sparse correlations (Lemma 1) and a deterministic reduction of the best-subsets objective, (39)–(40), which are of independent use for $\ell_0$ estimators.

Difficulty

An upper bound on best subsets follows from comparing $\hat\beta_{\ell_0}$ with $\beta^*$ in a basic inequality. A lower bound must hold for every minimizer, and $\beta^*$ itself gives no lower bound. The first idea is to compare with the noiseless fit. It fails because the noise can be fitted by sparse directions, which is exactly the effect to be quantified. The difficult step is Lemma 1. It requires a large set of sparse directions that remain separated after multiplication by $X$, a lower bound on the expected maximum of a Gaussian process over that set, and concentration of that maximum around its mean, with all constants universal. A second subtlety is that the statement is about every minimizer of a nonconvex problem, so the proof has to bound the objective rather than the estimator.

Formalization scope

Vectors are Fin n → ℝ and Fin p → ℝ, with indices starting at 0. The design is X : Matrix (Fin n) (Fin p) ℝ. The Euclidean norm, $\ell_1$ norm, support and $\|\cdot\|_0$ are explicit definitions, since Mathlib's norm on Fin m → ℝ is the sup norm. $\gamma_s$ is an infimum over the nonzero vectors with $\|u\|_0\le s$; this set is nonempty when $p,s\ge1$, and every ratio is $\ge0$. The noise law is the product of $n$ centred Gaussians of variance $\sigma^2$ on $\mathbb R^n$. "With probability at least $1-\eta$" means that a measurable set of noise vectors of probability at least $1-\eta$ exists on which the conclusion holds. Best subsets is an argmin predicate: Theorem 4 quantifies over every minimizer, and existence is neither assumed nor needed. Universal constants are quantified before every other parameter. "$\|\cdot\|_0\le k/2$" is a comparison of real numbers.

The model consists of $X$, $\beta^*$ (with $f^*=X\beta^*$), $\epsilon$ and its Gaussian law, the estimator (1), and the minimal sparse eigenvalue $\gamma_s$.

Two hypotheses are pinned relative to the printed theorem:

• $k\ge2$, because the statement is false for $k=1$. Take every column equal to $e_1$ and $\beta^*=0$: the error is $\epsilon_1^2$, while the bound demands order $\sigma^2\log(ep)$ with probability tending to one.
• $\|\beta^*\|_0\le k$, because the proof uses $\|\beta^*\|_1$, which the printed $\ell_2$ hypothesis controls only for sparse $\beta^*$, and §3.4 places the theorem in Corollary 1's setting $\beta^*\in B_0(k)$.

The milestones carry neither pin. Because the constants are existential, a formalization in which $c_0$, $c$ or $C$ may depend on $p$, $k$ or $X$ would be trivial, and is ruled out by quantifying them first. A version asserting the bound for some minimizer would be weaker than the theorem.

Not formalized here: the upper bounds (Theorems 2, 3, 5), the noise events of Theorem 1, Corollaries 1–6, Propositions 3–4, and the numerical experiments. The proof of the goal also uses Theorem 1's event $\mathcal G_{2k}$, which belongs to a separate mission of this series. Proved platform results that a proof of Lemma 1 can use include Sudakov minoration for separated Gaussian families (HighDimProb.RandomProcesses.sudakov_minoration_finite_separated), Gaussian Lipschitz concentration (HighDimStat.TailBounds.lipschitz_gaussian_concentration) and a lower bound on Gaussian maxima (HighDimProb.RandomProcesses.standard_gaussian_max_lower_bound). Contributions are welcome on any milestone, and on supporting lemmas: a packing of sparse sign vectors (Gilbert–Varshamov type), and the approximation of $\ell_1$-bounded vectors by sparse ones.

Selected references

• R. Mazumder, P. Radchenko, A. Dedieu, Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low, Operations Research, 2023; preprint arXiv:1708.03288v4, 2022. https://arxiv.org/abs/1708.03288v4
• D. Bertsimas, A. King, R. Mazumder, Best subset selection via a modern optimization lens, Annals of Statistics 44(2), 2016. https://doi.org/10.1214/15-AOS1388
• T. Hastie, R. Tibshirani, R. Tibshirani, Best Subset, Forward Stepwise or Lasso? Analysis and Recommendations Based on Extensive Comparisons, Statistical Science 35(4), 2020. https://doi.org/10.1214/19-STS733
• 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
• R. Vershynin, High-Dimensional Probability, Cambridge University Press, 2018. https://doi.org/10.1017/9781108231596

Why shrink a best subset?

Best subset selection fits a linear predictor using at most $k$ of $p$ available columns. Its explicit limit on the number of selected variables makes the model easy to interpret, but the search can still fit noise: among many subsets of the same size, one can align unusually well with a noisy response. Mazumder, Radchenko and Dedieu study this effect in Subset Selection with Shrinkage. They add a penalty on the size of the selected coefficients and show how this changes prediction error when the signal-to-noise ratio is low.

An $\ell_1$ penalty is familiar from the Lasso. The estimator here also keeps the subset-size constraint, so its comparison class and its tuning parameter have a different role from those in an unconstrained Lasso. The paper's Theorem 3 gives three deterministic error bounds for this estimator, each valid on a specified event of the Gaussian noise. These bounds are the target of this mission. The separate probability estimates for the events are Theorem 1 of the paper and belong to another mission in this series.

Setting

Let $X\in\mathbb R^{n\times p}$ be a fixed design matrix whose columns have Euclidean norm one. The observation is $y=f^*+\epsilon$, where $f^*\in\mathbb R^n$ is a fixed mean and the coordinates of $\epsilon$ are independent $N(0,\sigma^2)$ random variables, with $\sigma>0$. The result below fixes one realized noise vector $\epsilon$ and assumes it lies in an event stated below. No assumption that $f^*$ is itself a linear combination of columns of $X$ is required.

For $1\le k\le p$, write $B_0(k)=\{\beta\in\mathbb R^p:\|\beta\|_0\le k\}$, where $\|\beta\|_0$ counts nonzero coordinates. An $\ell_1$-regularized best subset estimator is any minimizer

$$\hat\beta_1\in\operatorname*{argmin}_{\beta\in B_0(k)}\bigl\{\|y-X\beta\|_2^2+\lambda\|\beta\|_1\bigr\}.\tag{16}$$

The objective has no factor $1/2$. The assertion applies to every minimizer, so tied solutions are covered. The sparse minimum singular value is $\gamma_s=\inf\{\|Xu\|_2/\|u\|_2:u\ne0,\ \|u\|_0\le s\}$. When $p\ge1$ and $s\ge1$ its domain is nonempty. Write $u_1^\sharp,\ldots,u_p^\sharp$ for the decreasing rearrangement of $|u_1|,\ldots,|u_p|$.

The paper defines three noise events used here. $\mathcal H$ bounds the largest coordinate of $X^\top\epsilon$ by $\sigma\sqrt{2\log(2p)}+\sigma\sqrt{2\log(1/\delta_0)}$. On $\mathcal F$, every $u\in\mathbb R^p$ satisfies

$$\epsilon^\top Xu\le(4+\sqrt2)\sigma\max\left\{\sum_{j=1}^{p}u_j^\sharp\sqrt{\log(2p/j)},\ \sqrt{\log(1/\delta_0)}\,\|Xu\|_2\right\}.$$

On $\mathcal G_s$, every $u\in B_0(s)$ satisfies $\epsilon^\top Xu\le\sigma\sqrt{5s\log(ep/s)+\log(1/\delta_0)}\,\|Xu\|_2$. Here $\delta_0\in(0,1]$ and all logarithms are natural. These definitions, including the constant in $\mathcal G_s$, are the printed deterministic events of p. 13.

Formalization targets

Exact slow rate on $\mathcal H$

At $\lambda=2\sigma\sqrt{2\log(2p)}+2\sigma\sqrt{2\log(1/\delta_0)}$, Theorem 3(A) states

$$\|f^*-X\hat\beta_1\|_2^2\le\inf_{\beta\in B_0(k)}\bigl[\|f^*-X\beta\|_2^2+2\lambda\|\beta\|_1\bigr]\qquad(\epsilon\in\mathcal H).$$

Slow rate on $\mathcal F$

For $\lambda\ge(8+2\sqrt2)\sigma\sqrt{\log(2p)}$, a positive universal constant $C_A$ gives

$$\|f^*-X\hat\beta_1\|_2^2\le C_A\left[\inf_{\beta\in B_0(k)}\bigl(\|f^*-X\beta\|_2^2+\lambda\|\beta\|_1\bigr)+\sigma^2\log(1/\delta_0)\right]\qquad(\epsilon\in\mathcal F).$$

Fast rate on $\mathcal G_{2k}$

For every $\lambda\ge0$, a positive universal constant $C_B$ gives

$$\|f^*-X\hat\beta_1\|_2^2\le C_B\left[\inf_{\beta\in B_0(k)}\|f^*-X\beta\|_2^2+\sigma^2k\log(ep/k)+\gamma_{2k}^{-2}\lambda^2 k+\sigma^2\log(1/\delta_0)\right]\qquad(\epsilon\in\mathcal G_{2k}).$$

The $k$ multiplying $\gamma_{2k}^{-2}\lambda^2$ distinguishes this rate from the $\ell_2$-penalized estimator's bound. The three claims together, with their separate tuning conditions, are Theorem 3 on p. 16. The milestones follow the displays of its proof in Supplement B.6, pp. 42–43.

What the result provides

Each inequality compares the prediction of any selected minimizer with that of every sparse competitor. The first bound has an exact leading constant and no additive noise term on $\mathcal H$. The second keeps a linear penalty term when $\lambda$ meets a fixed noise-dependent threshold. The third replaces the linear term with a quadratic $\lambda$ term controlled by the sparse minimum singular value. This distinguishes regimes in which coefficient shrinkage changes the error rate. The paper also combines deterministic bounds with event probabilities in subsequent corollaries; those probability statements are separate from this goal.

The paper proves Theorem 3. The formalization task is to verify its model definitions, event interpretation and all three inequalities in Lean, with the same constants and quantifiers. The milestone statements isolate the basic inequality, the $\mathcal H$ bound, the rearranged-coordinate bound, the $\mathcal F$ case split and the sparse $\ell_1$ step. A complete proof would also provide reusable finite-dimensional norm and matrix estimates. This mission does not include the paper's numerical experiments, data-driven model-size selection, the $\ell_2$-penalized estimator, or the event-probability theorem.

Difficulty

The constraint $\|\beta\|_0\le k$ makes the estimator a minimizer over a nonconvex set. A standard unconstrained Lasso argument does not directly supply the paper's bound for every feasible sparse comparator. The slow rates rely on two different noise controls: a coordinatewise bound on $\mathcal H$ and a maximum of a sorted-coordinate term and a prediction-norm term on $\mathcal F$. The fast rate also needs the sparse minimum singular value to relate coefficient error to prediction error. The constants in these steps matter: replacing the exact first tuning equality or dropping the factor $k$ in the fast rate would state a different theorem.

Formalization scope

Lean uses Fin n → ℝ and Fin p → ℝ for vectors and Matrix (Fin n) (Fin p) ℝ for $X$. Norms are explicit finite sums, rather than the function type's default supremum norm. The paper's one-based sorted index $j$ is j.val + 1; the sum using $u^\sharp$ is encoded as a maximum over coordinate permutations, which agrees with the decreasing rearrangement. The events are predicates on realized noise vectors. The Gaussian law explains the model but is not needed in these deterministic statements. The estimator is an argmin predicate, never a chosen minimizer.

The universal constants precede all dimensions and data in the Lean goal. The infima in the three displayed bounds are expressed as inequalities for every $\beta\in B_0(k)$, avoiding the default value of an empty or unbounded real infimum. The standing conditions are $1\le k\le p$, unit-norm columns, $\sigma>0$ and $0<\delta_0\le1$. The first slow-rate branch retains the paper's equality for $\lambda$. The fast branch additionally requires $\gamma_{2k}>0$ or $\lambda=0$: this makes the $\lambda^2/\gamma_{2k}^2$ term meaningful under Lean's total division, which returns zero at a zero denominator. The displayed events use the paper's original $\mathcal G_s$ constant; this mission makes only a deterministic claim on that event.

The sparse domain for $\gamma_{2k}$ is nonempty under these conditions. All square-root radicands and logarithm arguments in the target are in their intended ranges. The formalization must rule out a universal constant that depends on $n$, $p$, $k$, $X$ or $\lambda$, and must apply to every minimizer. Contributions to the shared norm inequalities, rearrangement identity and matrix calculations are useful beyond this theorem.

Selected references

• Rahul Mazumder, Peter Radchenko and Antoine Dedieu, Subset Selection with Shrinkage: Sparse Linear Modeling When the SNR Is Low, Operations Research 71 (2023), arXiv preprint version 4 (2022), arXiv:1708.03288v4. This mission cites the preprint's page and theorem numbering.

Why payment timing matters

A retailer can pay a supplier when it places an order or after the supplier delivers it. When production yield is uncertain, the choice changes who bears the cost of missing units. It can also change the supplier's production decision and, through the amount available for sale, the surplus received by consumers. Geng, Guo, Xiao and Yang study these effects in a decentralized supply chain and show that payment postponement can help all three parties, hurt all three, or benefit some while hurting others, depending on production cost and the retailer's pricing rule. Their Proposition 4 gives the precise cost intervals for these outcomes in the SSRN author version, pp. 19–20.

The result matters to contract design in supply chains where realized output can be below planned production. Paying for units ordered and paying for units delivered allocate that shortage differently. A comparison based only on the retailer's expected profit would miss the effects on the upstream supplier and final consumers. Proposition 4 keeps all three outcomes visible while holding the retailer's pricing policy fixed.

The supply-chain game

There is one supplier and one retailer. The supplier chooses a wholesale price $w$ and plans production $Q$ at cost $cQ$. The retailer orders $q$ and sells to a market with linear demand $d(p)=a-bp$, where $a,b>0$ and $p$ is the retail price. The yield factor $Y$ equals $1$ with probability $\theta$ and $\alpha$ with probability $1-\theta$, with $0<\alpha,\theta<1$. Thus $\mu=\mathbb E Y=\alpha(1-\theta)+\theta$. The retailer receives $\widehat q=\min\{YQ,q\}$ units; the production cost applies to planned $Q$, including units lost to yield risk §3.1–3.2.

Under pay-by-order, the retailer transfers $wq$ to the supplier and the supplier produces $Q=q$. Under pay-by-delivery, the transfer is $w\widehat q$ and the supplier can choose a larger production quantity. Under ex ante pricing, the retailer fixes $p$ before yield is known. Under responsive pricing, the retailer sets $p$ after observing delivery. Combining payment and pricing gives OA (order, ex ante), OR (order, responsive), DA (delivery, ex ante), and DR (delivery, responsive). The supplier first sets $w$, the retailer next orders and possibly fixes a price, the supplier chooses production, yield is realized, and responsive pricing occurs last Table 1, p. 9.

Both firms maximize expected profit at every stage. A subgame-perfect equilibrium is a complete plan of choices after every history in which each choice is optimal at that history. For scenario $k$, write $\pi_R^k$ and $\pi_S^k$ for equilibrium retailer and supplier profit. The consumer surplus $CS^k$ is expected surplus from sales: for delivered stock $X$ and market price $p$, the model integrates inverse demand less $p$ from zero to $\min\{d(p),X\}$. This is the paper's priority allocation convention for consumers with the highest willingness to pay p. 10.

Formalization targets

The main target is Proposition 4, which compares OA with DA and OR with DR. Let $\Delta(\pi_R,\pi_S,CS)$ mean the delivery-payment outcome minus its order-payment counterpart. A plus sign below means a strict increase, a minus sign a strict decrease, and zero equality. The admissible cost range is $0<c<a\mu/b$.

For ex ante pricing, with no restriction $\alpha\ge9/16$, the paper gives a threshold $0<\overline C<c^{DA}$ and the following pattern:

$$\begin{array}{c|c} \text{cost interval}&\operatorname{sign}\Delta(\pi_R,\pi_S,CS)\\ (\max\{0,c^{OA}_2\},\max\{\overline C,c^{OA}_2\}) &(+,+,+)\\ (\max\{\overline C,c^{OA}_2\},c^{DA}) &(+,+,-)\\ (0,\max\{0,c^{OA}_1\})\text{ or }(c^{DA},a\mu/b)&(0,0,0). \end{array}$$

For responsive pricing, assuming $\alpha\ge9/16$, the pattern is $(+,+,+)$ on $(0,\widetilde C)$, $(-,-,-)$ on $(\widetilde C,c^{DR}_1)$, $(+,-,+)$ on $(c^{DR}_1,c^{DR}_2)$, and $(0,0,0)$ on $(c^{DR}_2,a\mu/b)$. The thresholds are those specified in the paper: $\widetilde C$ is equation (6), $\overline C$ is equation (8), and the scenario cost thresholds come from Appendix B. The first ex ante interval can be empty for some parameters; its printed endpoints are retained. The milestones establish the supplier's production and responsive pricing rules, the four scenario outcomes, and the threshold ordering used in the comparison Appendices B–C.

What the result provides

The theorem separates the effect of changing the payment contract from the effect of changing the pricing rule. For advance pricing it identifies an interval where payment postponement helps both firms and consumers, then an interval where consumers lose despite both firms gaining. For responsive pricing the direction of every effect can reverse as cost passes successive thresholds. At high cost the change in payment timing leaves all three equilibrium outcomes unchanged Proposition 4, pp. 19–20.

The paper derives the equilibrium formulas in Appendix B and proves the comparisons in Appendix C. The result is therefore a known mathematical claim, while this mission asks for a machine-checked development from the sequential game through the cost-dependent equilibrium outcomes and final comparisons. The definitions of a two-point yield game and its complete contingent strategies can support other formal studies of payment or pricing postponement. There is no claim that Proposition 4 already has a machine-checked proof.

Where the formal work is difficult

The supplier's production payoff has kinks at $Q=q$ and $Q=q/\alpha$. The retailer's best order changes when those production choices change, and responsive pricing adds another kink when delivered stock crosses $a/2$. As wholesale price varies, the supplier must compare outcomes on both sides of these changes. Consequently a single first-order condition for a smooth objective does not characterize the equilibrium. The cost thresholds also depend on square roots and comparisons among several formula pieces, including the larger root chosen for $c^{OA}_2$ Appendix B, pp. 33–37.

Formalization scope

Lean represents expectation by the two weighted yield outcomes. Production cost $c$ is a separate argument, so thresholds depend only on $(a,b,\alpha,\theta)$. Parameters satisfy $a,b>0$, $0<\alpha,\theta<1$, and $0<c<a\mu/b$. Wholesale and retail prices obey the strict admissibility bounds of equation (3). Orders are nonnegative; pay-by-delivery production is nonnegative; pay-by-order production equals the order. Consumer surplus is a real interval integral. Every comparison quantifies over actual subgame-perfect equilibria, and the goal separately asserts that the compared equilibria exist at every admissible cost. Equilibrium profits are computed from strategies and transfers, rather than defined to equal the Appendix B formulas.

The paper's statements require care at ties. The model selects $Q=q$ when that is a profit-maximizing pay-by-delivery production choice, including the indifferent DR regime. The printed middle DR consumer-surplus expression combines outcomes from different production choices; the equilibrium-consistent expression is used here, and Proposition 4(R)'s comparison remains valid under either expression. Equation (2) swaps the scenario labels of committed and responsive prices, so consumer surplus uses the actual ex ante price in OA and DA and the price after delivery in OR and DR. The printed $[x]^+$ in Appendix B.1 is read as $\max\{0,x\}$, as in Lemma 1. Outcome claims use open cost intervals because uniqueness at exact thresholds fails; equilibrium existence remains part of the targets there. The threshold $c^{OA}_2$ is the larger root of the relevant quadratic factor, and $\overline C$ and $\widetilde C$ use the paper's explicit formulas. These conventions are recorded in the local moderation notes.

The development calls for real inequality reasoning, optimization of piecewise objectives, and careful handling of interval integrals. Contributions that prove the production and price best responses, establish the four equilibrium lemmas, or verify the threshold order each advance the final comparison.

Selected references

• X. Geng, X. Guo, G. Xiao and N. Yang, Supply Risk Mitigation in a Decentralized Supply Chain: Pricing Postponement or Payment Postponement?, Manufacturing & Service Operations Management 25(3), 2023. SSRN author version 3546872; DOI: 10.1287/msom.2022.0198.

Motivation

A retailer that buys from a supplier with unreliable production has two contractual levers against supply risk, and both postpone a decision until after the yield is known. Payment postponement means paying only for the units actually delivered (pay-by-delivery) instead of the units ordered (pay-by-order). This moves the yield risk upstream. Pricing postponement means setting the retail price after the delivery is observed (responsive pricing) instead of committing to it in advance (ex ante pricing). This moves the risk downstream to consumers. Both practices are common in procurement, and the natural intuition is that two ways of shedding the same risk should be substitutes: once one lever is in use, the other should be worth less.

Geng, Guo, Xiao and Yang (MSOM 25(3), 2023; author version SSRN 3546872) compute the subgame-perfect equilibria of all four combinations of the two levers in a stylized supplier–retailer game. Their Proposition 3 shows that the intuition fails at intermediate production cost. When full yield is likely and yield loss is mild, the two postponements are complements there: postponing payment is worth more when pricing is also postponed. This mission formalizes that result together with the four equilibrium characterizations it rests on.

Setting

A supplier sells one product to a retailer, who sells it in a market with linear demand $d(p)=a-bp$, $a,b>0$. The supplier plans production $Q$ at unit cost $c$ and realizes the fraction $Y$ of it, where

$$Y=1 \text{ with probability } \theta,\qquad Y=\alpha \text{ with probability } 1-\theta,\qquad 0<\alpha,\theta<1,$$

and $\mu=\alpha(1-\theta)+\theta$ is the mean yield. The retailer orders $q$ and receives $\hat q=\min\{YQ,q\}$.

The four scenarios are OA, OR, DA and DR. The first letter is the payment rule: by order (O, the transfer is $wq$) or by delivery (D, the transfer is $w\hat q$). The second letter is the pricing rule: ex ante (A, the price is fixed before the yield) or responsive (R, the price is set after $\hat q$ is observed). Each scenario is a sequential game. The supplier posts a wholesale price $w$. The retailer orders $q$, and also commits to a price $p$ in the ex ante scenarios. The supplier then chooses $Q$; under pay-by-order it produces exactly $q$. The yield realizes, and under responsive pricing the retailer then sets $p$. The retailer earns $p\min\{d(p),\hat q\}$ minus the transfer, and the supplier earns the transfer minus $cQ$. Both are risk neutral. Admissible actions follow the paper's standing ranges: $0<c<a\mu/b$, $0<p<a/b$, and $w$ between $c$ (or $c/\mu$ under pay-by-delivery) and $a/b$.

Write $\pi^k_R$ for the retailer's expected profit in a subgame-perfect equilibrium of scenario $k$. The paper's Definition 1 measures the interaction of the two postponements by

$$V=\big(\pi^{DR}_R-\pi^{OR}_R\big)-\big(\pi^{DA}_R-\pi^{OA}_R\big):$$

the value of payment postponement under responsive pricing, minus its value under ex ante pricing. The postponements are substitutes if $V<0$ and complements if $V>0$.

The parameter region of the result is $\alpha\ge 9/16$ together with $\mathcal H_3=\{\theta_2(\alpha)<\theta<1\}$, where $\theta_2(\alpha)$ is the largest real root of the cubic $-\alpha^3+\alpha^2(5+\alpha)x+(16-19\alpha-6\alpha^2)x^2-25(1-\alpha)x^3$. The cost thresholds $c^{DR}_1<c^{DR}_2$ (scenario DR) and $c^{DA}$ (scenario DA) are explicit algebraic functions of $(a,b,\alpha,\theta)$ given in the paper's Appendix B.

Formalization targets

Goal: Proposition 3

For $\alpha\ge9/16$ and $(\alpha,\theta)\in\mathcal H_3$, every scenario has an equilibrium at every cost $0<c<a\mu/b$, and there is a cost $0<\hat C<a\mu/b$ such that, at every choice of the four equilibria,

$$V<0 \text{ on } (0,c^{DR}_1)\cup(\hat C,c^{DA}),\qquad V>0 \text{ on } (c^{DR}_1,\hat C),\qquad V=0 \text{ on } (c^{DA},a\mu/b).$$

$\hat C$ is existential, as in the paper, and depends only on the parameters.

Milestones

• the supplier's production response (4) under pay-by-delivery and the ex post price (5);
• Lemmas 1–4: existence of the equilibrium of each scenario, and its outcome $(\pi_R,\pi_S,CS)$ in closed form on each cost interval;
• Lemma 1(i): on $\mathcal H_3$ the threshold $c^{OA}_2$ is nonpositive, so scenario OA has one regime;
• the threshold claims of Appendix C: $c^{OR}<0$ and $c^{DR}_1<c^{DR}_2<c^{DA}$ for $\alpha\ge9/16$.

Significance

The result separates the first-order question (which lever the retailer prefers, the subject of the paper's Proposition 2) from the second-order one (whether one lever raises the value of the other). It shows that two risk-shifting instruments can reinforce each other. On $(c^{DR}_1,\hat C)$, adopting one postponement raises the value of the other. So whenever the retailer gains from adopting either lever alone, it gains even more from adopting both. Below $c^{DR}_1$ and above $\hat C$ the reverse holds. Above $c^{DA}$, payment postponement is irrelevant, because the supplier never inflates production there.

The paper proves Lemmas 1–4 by backward induction in Appendix B and the proposition by comparing closed forms in Appendix C. None of it is machine-checked. A formal proof requires the four backward inductions with every kink and tie handled, and the polynomial inequalities between the thresholds over the parameter region. The formalization also corrects the record: the paper's explicit formula (7) for $\hat C$ does not locate the sign change of $V$ (at $(\alpha,\theta)=(0.6,0.75)$ it exceeds $c^{DA}$), while the existential statement of Proposition 3 holds at every sampled point.

Difficulty

Once Lemmas 1–4 are available, $V$ is a difference of explicit piecewise functions of $c$. The difficulty lies in those lemmas and in the thresholds. Each lemma is a three-stage optimization. The supplier's profit is piecewise linear in $Q$, with kinks at $q$ and $q/\alpha$. The retailer's profit is piecewise in $(q,p)$, with kinks where it becomes worth inflating the order. The supplier's value function in $w$ is piecewise quadratic, and its maximum can sit at a kink. In scenario DR it sits exactly at the price where the supplier is indifferent to inflating production. A naive reading of the paper's tie rule removes the equilibrium there altogether. On the middle DR interval the sign of $V$ changes inside the interval, at a root of a polynomial with nested square roots. On the other pieces, the signs of $V$ and the ordering $c^{DR}_1<c^{DR}_2<c^{DA}$ are polynomial inequalities in $(\alpha,\theta)$, with $\theta_2(\alpha)$ defined implicitly as a cubic root.

Formalization scope

• Parameters and cost. The parameters $(a,b,\alpha,\theta)$ form a structure. The cost $c$ is a separate argument, and every threshold depends on the parameters only.
• Expectation. The expectation over the yield is the explicit two-point sum $\theta f(1)+(1-\theta)f(\alpha)$.
• Equilibrium. Strategies are functions of all earlier moves, and optimality is required at every node over the full admissible action sets.
• Production ties. Under pay-by-delivery the supplier's production is a best response. When producing exactly $q$ is optimal, it produces $q$. The paper's display (4) assigns that tie to inflation, but under that rule scenario DR has no equilibrium for intermediate cost. The convention reproduces the paper's DR profits.
• Consumer surplus. It is the integral $\int_0^{\min\{d(p),\hat q\}}(p(t)-p)\,dt$. It uses the ex post price in the responsive scenarios and the committed price in the ex ante ones; the labels of the paper's display (2) are swapped.
• Closed forms. Two printed consumer-surplus values are corrected to the equilibrium values: the middle piece of OA ($8b\alpha^2$ for $8b\alpha^3$) and the middle piece of DR (one factor $\alpha^2(1-\theta)+\theta$ fewer).
• Cost intervals. Every statement is on open cost intervals, because at a threshold the outcome is not unique.
• Thresholds. $c^{OA}_2$, "the second root" of a quartic, is the larger root of the quadratic factor that defines it. $\theta_2$ is the supremum of the cubic's real roots, a finite nonempty set.

The equilibrium profits are outcomes of the equilibrium predicate. They are never defined by their closed forms, and the goal carries the existence of an equilibrium in each scenario. Without that, the comparison would be vacuous whenever the predicate is unsatisfiable.

Every object is elementary: real arithmetic, square roots, min/max, one interval integral and one sSup. The equilibrium predicate and the four lemmas are shared with the three companion missions of this paper (Propositions 2, 4 and 5). Proofs of the lemmas, of the threshold inequalities and of the goal are all welcome.

Selected references

• X. Geng, X. Guo, G. Xiao, N. Yang, Supply Risk Mitigation in a Decentralized Supply Chain: Pricing Postponement or Payment Postponement?, Manufacturing & Service Operations Management 25(3), 2023. https://doi.org/10.1287/msom.2022.0198 ; author version SSRN 3546872, https://ssrn.com/abstract=3546872

Motivation

When a supplier's production is subject to random yield, only part of a planned production run turns into usable output. A retailer sourcing from such a supplier bears the resulting shortage risk unless the contract or the selling strategy moves it elsewhere. Random yield is a classical topic in production planning (Yano and Lee, 1995), and postponing a decision until uncertainty resolves is a classical risk-mitigation tool (Van Mieghem and Dada, 1999).

Geng, Guo, Xiao and Yang study two postponements available to a retailer facing an unreliable supplier. Payment postponement replaces payment for the ordered quantity by payment for the delivered quantity, which shifts the yield risk to the supplier. Pricing postponement (responsive pricing) sets the retail price after the delivery is known, which shifts the risk to consumers. Their Proposition 2 answers which of the four combinations the retailer prefers, as a function of the production cost, when the yield loss is not too severe. This mission formalizes that proposition and the equilibrium results it rests on.

Setting

A supplier sells to a retailer, who sells to a market with linear demand $d(p)=a-bp$, $a,b>0$. The supplier's yield factor $Y$ takes the value $1$ with probability $\theta$ and $\alpha$ with probability $1-\theta$, with $\alpha,\theta\in(0,1)$, and has mean $\mu=\alpha(1-\theta)+\theta$. The supplier plans production $Q$, pays $c$ per planned unit, and delivers $\hat q=\min\{YQ,q\}$ against an order $q$. Throughout, $0<c<a\mu/b$.

There are four scenarios, written $k\in\{OA,OR,DA,DR\}$:

• O (pay-by-order): the retailer pays $wq$, and the supplier produces exactly $Q=q$;
• D (pay-by-delivery): the retailer pays $w\hat q$, and the supplier chooses $Q$ and may inflate production above $q$;
• A (ex ante pricing): the retailer commits to the retail price $p$ when it orders;
• R (responsive pricing): the retailer sets $p$ after seeing $\hat q$, maximizing $p\min\{d(p),\hat q\}$.

Each scenario is a Stackelberg game. The supplier sets the wholesale price $w$, the retailer orders (and, ex ante, prices), the supplier produces, the yield realizes, and under responsive pricing the retailer prices. Both firms are risk neutral. The solution concept is subgame-perfect equilibrium, and $\pi^k_R$ denotes the retailer's expected equilibrium profit in scenario $k$. Admissible prices are those of the paper's standing assumption (3): $0<p<a/b$, and $c<w<a/b$ under pay-by-order or $c/\mu<w<a/b$ under pay-by-delivery.

The cost thresholds of the comparison are

$$\tilde C=\frac{a\alpha\big(1-\sqrt{\alpha^2(1-\theta)+\theta}\big)}{b(1+\alpha)},\qquad c^{DR}_2=\frac{a\alpha\mu(1-\theta)}{b(\mu+\theta)},$$ $$c^{DR}_1=\frac{a\alpha(1-\theta)\big(\mu^2+\theta-2\theta\sqrt{\alpha\mu(1-\alpha)(1-\theta)}\big)}{b\big(\alpha^2(1-\theta)^3+4\alpha\theta(1-\theta)+\theta(1+\theta)^2\big)}.$$

Formalization targets

Goal: Proposition 2 (p. 16)

For $9/16\le\alpha<1$ and every $0<c<a\mu/b$, equilibria of OR, DA and DR exist, and every choice of equilibria satisfies

$$\begin{aligned} &\pi^{OR}_R<\pi^{DR}_R=\pi^{DA}_R && 0<c<\tilde C,\\ &\pi^{DA}_R=\pi^{DR}_R<\pi^{OR}_R && \tilde C<c<c^{DR}_1,\\ &\pi^{DA}_R<\pi^{OR}_R<\pi^{DR}_R && c^{DR}_1<c<c^{DR}_2,\\ &\pi^{DA}_R<\pi^{DR}_R=\pi^{OR}_R && c^{DR}_2<c<a\mu/b. \end{aligned}$$

Milestones

1. (4): the supplier's production under pay-by-delivery is $q$ below the wholesale price $c/(\alpha(1-\theta))$ and $q/\alpha$ above it.
2. (5): the responsive price is $(a-\hat q)/b$ for $\hat q<a/2$ and $a/(2b)$ otherwise.
3. Lemmas 2, 3, 4: existence of equilibria of OR, DA and DR, and their outcomes $(\pi_R,\pi_S,CS)$ in closed form on each open cost interval (Lemma 4 for $\alpha\ge 9/16$).
4. Threshold order (proof of Propositions 1–2): for $\alpha\ge 9/16$, $c^{OR}<0$ and $c^{DR}_1<c^{DR}_2<c^{DA}$.
5. Position of $\tilde C$ (proof of Proposition 4): for $\alpha\ge 9/16$, $0<\tilde C<c^{DR}_1$.

Significance

The proposition describes a preference cycle. Payment postponement (DA) is best when production is cheap, because the supplier then absorbs yield risk by inflating production. Pricing postponement (OR) is best at intermediate cost. Using both (DR) is strictly best on $(c^{DR}_1,c^{DR}_2)$, where the two postponements are worth more together than either alone. Above $c^{DR}_2$ the supplier stops inflating, DR and OR coincide, and pricing postponement suffices. These are the paper's managerial conclusions on contract and pricing choice under supply risk, and the other three missions of the series (strategic complementarity, and the effect of each postponement on the whole chain) rest on the same equilibria.

The paper derives the four equilibria in its Appendix B and proves the propositions in Appendix C as direct comparisons of closed forms. None of this has been machine-checked. The mission produces a formal model of the four games and a verified link from the game to the closed forms. Lemmas 2–4 are reusable by every statement about this model.

Difficulty

Once the closed forms are known, the comparison is polynomial algebra in $(\alpha,\theta,c)$ with square roots. The work lies upstream. Each equilibrium requires a backward induction over piecewise-linear objectives in $Q$ and $q$ and piecewise-quadratic objectives in $p$ and $w$. Optima occur at kinks such as the inflation threshold $w_0=c/(\alpha(1-\theta))$, and the supplier's value function is discontinuous there, so the maximum can sit at a boundary rather than at the center of a piece. In scenario DR the equilibrium wholesale price on $(c^{DR}_1,c^{DR}_2)$ sits exactly at $w_0$, where the supplier is indifferent among all productions in $[q,q/\alpha]$, so existence depends on how that tie is resolved. Uniqueness of outcomes, which the comparison needs, holds only on open cost intervals, because at each threshold two wholesale prices tie with different outcomes. The threshold inequalities for $\alpha\ge 9/16$ are not visible from the formulas and need careful estimates of the radicals.

Formalization scope

Parameters are a structure $(a,b,\alpha,\theta)$ with validity predicate $a,b>0$, $\alpha,\theta\in(0,1)$; the cost $c$ is a separate real argument. The expectation over $Y$ is the two-term sum $\theta f(1)+(1-\theta)f(\alpha)$, with no measure theory. A strategy profile consists of a wholesale price and rules for production $Q(w,q)$, the order $q(w)$, the ex ante price $p(w)$ and the ex post price $p^{\mathrm r}(w,q,\hat q)$. Equilibrium requires optimality at every admissible history over the admissible sets of (3). Consumer surplus is the integral $\int_0^{\min\{d(p),X\}}(p(t)-p)\,dt$, evaluated at the ex post price under responsive pricing and at the committed price under ex ante pricing.

Conventions and disclosed departures from the page:

• Tie rule. Under pay-by-delivery, when producing exactly $q$ is optimal, the supplier produces $q$. Display (4) assigns the tie at $w_0$ to inflation, under which DR has no equilibrium on $(c^{DR}_1,c^{DR}_2)$. Lemma 4's printed profits there are those of the convention.
• $CS^{DR}$ on the middle piece is stated with denominator $8b\alpha^2(1-\theta)^2(\alpha^2(1-\theta)+\theta)$; the page prints the last factor squared, which is the surplus of no single equilibrium. Proposition 2 does not involve $CS$.
• Open intervals. Lemmas are stated on open cost intervals; at the thresholds outcomes are not unique.
• $\tilde C$ is instantiated by (6), as Appendix C does; the page introduces it through Proposition 1's existential.
• Display (2) prints the scenario labels of $CS$ swapped; the Appendix B reading is used.

$\pi^k_R$ is the retailer's profit along an equilibrium of the game, never its closed form; a formalization that defines the profits by the Appendix B formulas, or an equilibrium predicate that no profile satisfies, would make the goal trivial. The goal therefore also asserts existence of equilibria of the three scenarios.

Contributions welcome: proofs of the milestones; general lemmas on maximizing piecewise-linear and piecewise-quadratic functions with kinks; the threshold inequalities. Proposition 1 (OA versus the others) is not part of this mission.

Selected references

• X. Geng, X. Guo, G. Xiao, N. Yang, Supply Risk Mitigation in a Decentralized Supply Chain: Pricing Postponement or Payment Postponement?, SSRN 3546872 (author version), 2022; published in Manufacturing & Service Operations Management 25(3), 2023. https://ssrn.com/abstract=3546872, https://doi.org/10.1287/msom.2022.0198
• C. A. Yano, H. L. Lee, Lot Sizing with Random Yields: A Review, Operations Research 43(2), 1995. https://doi.org/10.1287/opre.43.2.311
• J. A. Van Mieghem, M. Dada, Price Versus Production Postponement: Capacity and Competition, Management Science 45(12), 1999. https://doi.org/10.1287/mnsc.45.12.1631