All missions

Motivation

The convex feasibility problem asks for a point in the intersection of closed convex sets. It underlies signal and image reconstruction, phase retrieval relaxations, and the constraint handling inside larger optimization methods. The workhorse algorithms are projection methods: the method of alternating projections (MAP), going back to von Neumann for subspaces, and the Douglas–Rachford and Peaceman–Rachford splitting schemes, which can be applied to the indicator, distance or squared-distance functions of the sets.

Without a regularity condition on how the sets meet, projection methods can converge arbitrarily slowly. Bounded linear regularity, an error bound saying that a point close to every set is close to their intersection, is the standard condition under which linear rates are obtained (Bauschke and Borwein, SIAM Review, 1996, doi:10.1137/S0036144593251710). Section 5 of D. Davis and W. Yin, Faster convergence rates of relaxed Peaceman–Rachford and ADMM under regularity assumptions (arXiv:1407.5210v3, Math. Oper. Res. 42(3), 2017) applies relaxed Peaceman–Rachford splitting (PRS) to the squared distance functions of two sets and proves that, under bounded linear regularity, the distance of the iterates to the intersection contracts by an explicit factor at every step, with step sizes and relaxation parameters allowed to vary between iterations. MAP is the special case of step size $1/2$ and relaxation $1$.

Setting

Let $\mathcal H$ be a real Hilbert space and $C_f, C_g \subseteq \mathcal H$ closed convex sets with $C_f\cap C_g\neq\emptyset$. For $C\subseteq\mathcal H$ the distance function is $d_C(x)=\inf_{y\in C}\|x-y\|$, and $P_C$ is the metric projection, the nearest point of $C$. The problem is modelled with

$$f(x)=d^2_{C_f}(x),\qquad g(x)=d^2_{C_g}(x).$$

For $\gamma>0$ the proximal map $\mathbf{prox}_{\gamma h}(x)$ is the minimiser of $h(y)+\frac1{2\gamma}\|y-x\|^2$, and the reflection is $\mathbf{refl}_{\gamma h}=2\,\mathbf{prox}_{\gamma h}-I$. With two step sizes, $T^{\gamma_f,\gamma_g}_{\mathrm{PRS}}=\mathbf{refl}_{\gamma_f f}\circ\mathbf{refl}_{\gamma_g g}$, and $(T)_\lambda=(1-\lambda)I+\lambda T$.

Given $z^0$, step sizes $\gamma_{f,k},\gamma_{g,k}>0$ and relaxation parameters $\lambda_k\in(0,1]$, iteration (5.1) is

$$x_g^k=\mathbf{prox}_{\gamma_{g,k}d^2_{C_g}}(z^k),\quad x_f^k=\mathbf{prox}_{\gamma_{f,k}d^2_{C_f}}(2x_g^k-z^k),\quad z^{k+1}=z^k+2\lambda_k(x_f^k-x_g^k).$$

The pair $\{C_f,C_g\}$ is boundedly linearly regular (Definition 5.1) if for every $\rho>0$ there is $\mu_\rho>0$ such that

$$d_{C_f\cap C_g}(x)\le\mu_\rho\max\{d_{C_f}(x),d_{C_g}(x)\}\qquad\text{for all }x\in B(0,\rho),$$

where $B(0,\rho)$ is the open ball. The rate function is

$$C(\gamma_f,\gamma_g,\lambda,\mu)=\left(1-\frac{4\lambda\min\{\gamma_g/(2\gamma_g+1)^2,\ \gamma_f/(2\gamma_f+1)^2\}}{\mu^2\max\{16\gamma_g^2/(2\gamma_g+1)^2,\ 1\}}\right)^{1/2}.$$

Formalization targets

Goal: Theorem 5.1

Suppose $\{C_f,C_g\}$ is boundedly linearly regular, $(z^k)$ is generated by (5.1), every $z^j$ lies in $B(0,\rho)$, and $d_{C_f\cap C_g}\le\mu_\rho\max\{d_{C_f},d_{C_g}\}$ on $B(0,\rho)$. Then for all $k\ge0$

$$d_{C_f\cap C_g}(z^{k+1})\le C(\gamma_{f,k},\gamma_{g,k},\lambda_k,\mu_\rho)\,d_{C_f\cap C_g}(z^k), \tag{5.3}$$

and if $\overline C=\sup_j C(\gamma_{f,j},\gamma_{g,j},\lambda_j,\mu_\rho)<1$, the iterates converge to a point $x\in C_f\cap C_g$ with

$$\|z^k-x\|\le 2\,d_{C_f\cap C_g}(z^0)\prod_{i=0}^{k-1}C(\gamma_{f,i},\gamma_{g,i},\lambda_i,\mu_\rho). \tag{5.4}$$

Milestones

The milestones follow the paper's own argument: Proposition 5.1 Parts 2 and 3 (the gradient of $d_C^2$ and the closed form $\mathbf{prox}_{\gamma d_C^2}=\frac1{2\gamma+1}I+\frac{2\gamma}{2\gamma+1}P_C$); Proposition 5.2, the fundamental inequality specialised to squared distances; Propositions C.1 and C.2 (the fixed-point set of $T^{\gamma_f,\gamma_g}_{\mathrm{PRS}}$ is $C_f\cap C_g$, and the iterates are Fejér monotone for $\lambda_k\in(0,1]$); and the displays (5.5)–(5.7), (5.8), (5.10) and (5.11) of the proof of Theorem 5.1, ending with the one-step contraction at a single point.

Companion: Corollary 5.1

With $\gamma_{f,k}\equiv\gamma_{g,k}\equiv\frac12$ and $\lambda_k\equiv1$, iteration (5.1) is MAP, $z^{k+1}=P_{C_f}P_{C_g}z^k$, and under the assumptions of Theorem 5.1 it contracts the distance to $C_f\cap C_g$ by $(1-1/\mu_\rho^2)^{1/2}$ from the second iterate on, converging linearly to a point of the intersection.

Significance

Theorem 5.1 gives an explicit, iteration-wise linear rate for relaxed PRS on the two-set feasibility problem with step sizes and relaxation parameters that may change from step to step. Its specialisation, Corollary 5.1, recovers linear convergence of MAP under bounded linear regularity with rate $(1-1/\mu_\rho^2)^{1/2}$, better than the $(1-1/(8\mu^2))^{1/2}$ derived in earlier work on cyclic projections. Remark 5.1 of the paper notes that Douglas–Rachford on indicator functions is a limiting case of the scheme as the step sizes grow, though the rate degenerates in that limit.

The results are proved in the paper; the proof of the convergence statement cites Bauschke–Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Theorem 5.12 (Fejér monotone sequences whose distance to a closed convex set decays converge strongly). No machine-checked proof of these statements was found on Prove2Me (search of 2026-10-07). A formalization produces a checked chain from the closed form of the prox of $d_C^2$ through the fundamental inequality to the linear rate, and with it reusable facts about squared distance functions, metric projections onto closed convex sets in Hilbert space, and Fejér monotone sequences.

Difficulty

The obvious argument would contract the distance to $C_f\cap C_g$ directly, but one PRS step measures only $d_{C_g}$ at $z$ and $d_{C_f}$ at the reflected point $\mathbf{refl}_{\gamma_g g}(z)$, never $d_{C_f}(z)$. Transferring the second distance back to $z$ costs a factor $\max\{c_1^2,1\}$ with $c_1=4\gamma_g/(2\gamma_g+1)$, and only after that does the regularity inequality turn $\max\{d_{C_f}(z),d_{C_g}(z)\}$ into $d_{C_f\cap C_g}(z)$. The fundamental inequality (5.2) itself rests on the prox-gradient calculus of the earlier sections, specialised to functions whose gradients $2(I-P_C)$ are Lipschitz. Passing from a contracting distance to convergence of the iterates to one point needs Fejér monotonicity and a completeness argument; a contracting distance alone does not give a limit.

Formalization scope

Everything lives in a real Hilbert space (InnerProductSpace ℝ H with CompleteSpace H); $d_C$ is Mathlib's Metric.infDist. The squared distance is viewed as an extended-real function so that the published proximal predicate ThreeOpSplitting.ConvexRates.IsProx applies, and prox maps are arbitrary maps satisfying it (unique here). Metric projections are maps satisfying the published RandomGradFree.Nonsmooth.IsMetricProjection. Step sizes and prox maps are indexed by the iteration. The hypotheses of the goal are: $C_f,C_g$ closed and convex with nonempty intersection; bounded linear regularity of the pair; $\gamma_{f,k},\gamma_{g,k}>0$; $\lambda_k\in(0,1]$; iterates in an open ball $B(0,\rho)$ on which the regularity inequality holds with $\mu_\rho>0$. The range $\lambda_k\in(0,1]$ is Algorithm 1's standing assumption, used in the proof but not restated in (5.1). The condition $\overline C<1$ is stated as a uniform bound $c<1$ on all rate factors. The product in (5.4) runs over $i=0,\dots,k-1$; the page prints the upper index $k$, which claims an extra factor that the proof does not give. In the proof's (5.9)–(5.10) the page swaps $\gamma_f$ and $\gamma_g$ relative to (5.2); the milestone states the pairing that (5.2) produces. Corollary 5.1's improved rate is stated for $k\ge1$, since it uses $z^k\in C_f$.

A trivializing formalization is ruled out: the goal mentions none of the proof's intermediate quantities, takes the prox maps as genuine minimisers of the squared-distance objective rather than chosen points, and measures distances to a nonempty intersection, so the junk value of infDist on the empty set never arises.

A complete development needs the closed form of $\mathbf{prox}_{\gamma d^2_C}$, differentiability of $d_C^2$, the fundamental inequality of the paper's §1 specialised to these functions, and the convergence theorem for Fejér monotone sequences. The last three are reusable well beyond this mission. Proofs of any milestone, and of Mathlib-level lemmas on metric projections, are welcome.

Selected references

• D. Davis, W. Yin, Faster convergence rates of relaxed Peaceman–Rachford and ADMM under regularity assumptions, Mathematics of Operations Research 42(3), 2017; arXiv version used here: arXiv:1407.5210v3.
• H. H. Bauschke, J. M. Borwein, On projection algorithms for solving convex feasibility problems, SIAM Review 38(3), 1996. doi:10.1137/S0036144593251710
• H. H. Bauschke, P. L. Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Springer, 2011. doi:10.1007/978-1-4419-9467-7
• P.-L. Lions, B. Mercier, Splitting algorithms for the sum of two nonlinear operators, SIAM Journal on Numerical Analysis 16(6), 1979. doi:10.1137/0716071

Motivation

An assignment problem pairs each of $n$ sources with exactly one of $n$ destinations while minimizing a specified cost. A permutation records those pairings. The number of permutations grows as $n!$, so a direct search quickly becomes impractical. In discrete optimal transport, the same data can be placed in a linear optimization problem over nonnegative matrices: a matrix entry records how much mass moves from one source to one destination. That formulation permits a source's mass to be split, which gives it many more feasible solutions than the assignment problem. The question for this mission is whether the added flexibility can improve the optimum when every source and destination carries the same mass. The setting and answer are given in Peyré and Cuturi, Computational Optimal Transport, §2.2–2.3.

This capstone is the first in a series based on the textbook. It links a finite combinatorial optimization problem to the matrix model used throughout later chapters. The general transport model is needed again when marginals are unequal, when cost matrices come from distances, and when entropy is added to the objective. The uniform matching case isolates a useful boundary: relaxing an assignment to allow fractional flows expands the feasible set, yet it does not change the best objective value.

Setting

Fix an integer $n>0$ and a real $n\times n$ cost matrix $C$. The entry $C_{ij}$ is the cost of sending a unit of mass from source $i$ to destination $j$. No sign or metric assumption is imposed on $C$. A permutation $\sigma$ assigns source $i$ to destination $\sigma(i)$, with every destination used once. The assignment objective of equation (2.2) is

$$A_C(\sigma)=\frac1n\sum_{i=1}^{n}C_{i,\sigma(i)}.$$

The factor $1/n$ matters: it treats each source as having mass $1/n$, so the assignment and transport objectives use the same total mass.

A histogram is a vector of masses. The uniform histogram $u$ has $u_i=1/n$ at each of the $n$ indices. A coupling of histograms $a$ and $b$ is a nonnegative matrix $P$ with row sums $a$ and column sums $b$. The set of such matrices is

$$U(a,b)=\left\{P\in\mathbb R_+^{n\times m}:\sum_jP_{ij}=a_i\ \text{for each }i,\quad\sum_iP_{ij}=b_j\ \text{for each }j\right\}.$$

Its linear cost is $\langle C,P\rangle=\sum_{i,j}C_{ij}P_{ij}$, and $L_C(a,b)$ denotes the minimum cost over $P\in U(a,b)$, as in equations (2.10)–(2.11). For a permutation $\sigma$, the scaled permutation matrix $P_\sigma$ has entry $1/n$ in column $\sigma(i)$ of row $i$ and zero elsewhere. Consequently $P_\sigma$ is a coupling of $u$ with itself, and its transport cost equals $A_C(\sigma)$. A general member of $U(u,u)$ may distribute a row's mass across several columns.

Formalization targets

Relaxation bound

Because every scaled permutation matrix is feasible for the transport problem, the unrestricted minimum cannot exceed the assignment minimum:

$$L_C(u,u)\le \min_{\sigma\in\operatorname{Perm}(n)}A_C(\sigma).$$

This is the weaker claim in the milestone list. The symmetry of couplings under transposition and the identity $\langle C,P_\sigma\rangle=A_C(\sigma)$ supply reusable statements about the model. The list also states the book's scaled form of Birkhoff's extreme point characterization.

Proposition 2.1: tightness for uniform marginals

The goal is the stronger statement: there is an assignment that also minimizes over the full coupling polytope,

$$\exists\sigma^\star\in\operatorname{Perm}(n):\quad P_{\sigma^\star}\in U(u,u),\quad \langle C,P_{\sigma^\star}\rangle=L_C(u,u),\quad A_C(\sigma^\star)=\min_{\tau\in\operatorname{Perm}(n)}A_C(\tau).$$

This is Proposition 2.1, pp. 372–373. It quantifies over every real cost matrix of the given size. The equality of optimal values follows from the stated common optimizer; the proposition does not claim that every optimal transport plan is a permutation matrix.

Significance

The result gives an exact linear relaxation for uniform assignment. One can optimize over a convex set of matrices without paying an optimal value penalty for allowing fractional mass. The conclusion has a precise limit: it guarantees at least one integral, scaled permutation optimizer, while other optimal couplings can coexist when the cost matrix has ties. When source and destination weights are unequal, the assignment formulation may not even be feasible; the broader coupling model then carries information that a permutation cannot represent.

For formalization, the result fixes a finite transport interface that later missions can compare with their own conventions: nonnegative matrix entries, prescribed row and column sums, and a cost that is linear in the matrix. Mathlib already contains Birkhoff's theorem for doubly stochastic matrices with row sums equal to $1$. This mission's formal target uses the probability normalization $1/n$, so the scaling is part of the mathematical statement. The textbook result is known; the goal here is a machine checked Lean proof of this precise version and its cited supporting claims. The listed Lean declarations are currently open statements with sorry placeholders.

Difficulty

The evident inequality points in the easy direction: enlarging a feasible set can only reduce a minimum. It gives no reason why a minimizer over the larger set should happen to be a permutation matrix. A generic feasible coupling can split mass between several destinations, and even a unique assignment need not be the only point under consideration in the relaxed problem. The central issue is the geometry of the uniform coupling polytope and its relation to permutation matrices. Its normalization differs from the usual doubly stochastic convention, so a proof using a standard library theorem must retain the factor $1/n$ at every point where a matrix or objective is converted.

Formalization scope

The Lean index types are Fin n and Fin m; they have $n$ and $m$ elements but are numbered from zero. Histograms are real valued functions on those types, and couplings are real matrices constrained to be nonnegative with exact finite row and column sums. The pairing is a finite double sum. The goal assumes $n>0$ so that the displayed $1/n$ is meaningful and the assignment problem has an index to assign. There is no additional positivity requirement on $C$. The minimum values are represented by real infima only in statements where the uniform coupling polytope and permutation set are nonempty and their finite dimensional objectives are bounded below.

An optimal coupling in the goal is compared with all matrices in $U(u,u)$, including fractional ones. Restricting that comparison to permutation matrices would erase the proposition's content. The definitions of coupling feasibility, scaled permutation matrices, and the assignment cost are reusable beyond this chapter. Contributions that establish the scaling relation to Mathlib's doubly stochastic matrices, the extreme point characterization in this normalization, or the goal from these components fit the mission. The optional strict inclusion claim on p. 372 is excluded from the milestones because its printed formulation fails at $n=1$; it would require a separate $n\ge2$ statement. The page also prints row and column sums of $P_\sigma$ as $\mathbf1_n$ despite defining entries $1/n$; the Lean statement uses $\mathbf1_n/n$.

Selected references

• G. Peyré and M. Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019, DOI: 10.1561/2200000073.
• D. Bertsimas and J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Theorem 2.7, publisher record. Cited in the proof of Proposition 2.1.

Motivation

A manufacturer that sells through an independent retailer may also open its own direct channel, an online store or a factory outlet. This is called supply chain encroachment. The operations literature has asked whether encroachment helps or hurts the two firms. The usual approach compares the double-marginalization cost of a pure retail channel with the competition the direct channel creates. With quality exogenous and uniform across channels, Arya, Mittendorf and Sappington (2007) showed that encroachment can lead to a win–win outcome when the manufacturer's direct selling cost is large, because it pushes the wholesale price down.

Ha, Long and Nasiry (Quality in Supply Chain Encroachment, MSOM 18(2), 2016; authors' manuscript SSRN 3970373) make product quality a decision of the manufacturer. Their main model lets her commit to the qualities of both channels before the retailer orders. In that model quality differentiation is not always optimal: for some parameters she sells the same quality in both channels (their Proposition 4).

Commitment is a modelling assumption. When design lead times are short, the manufacturer can redesign the direct-channel product after seeing the retailer's order, so she cannot credibly announce its quality in advance. Section 6.3 of the paper studies this fast-design case. Its only analytical result is Proposition 7: without commitment, quality differentiation across channels is always optimal. This mission formalizes that proposition and the three steps of its proof.

Setting

Consumers. A consumer has quality sensitivity $\theta$, uniform on $[0,1]$, and obtains surplus $\theta u - p$ from one unit of quality $u>0$ at price $p$. The manufacturer sells $q_M$ units of quality $u_M$ directly and the retailer sells $q_R$ units of quality $u_R$. Each consumer buys at most one unit, and the market-clearing prices depend on which product has the higher quality:

• if $u_R\le u_M$: $\;p_M = u_M(1-q_M)-u_Rq_R,\quad p_R = u_R(1-q_M-q_R)$;
• if $u_M<u_R$: $\;p_M = u_M(1-q_M-q_R),\quad p_R = u_R(1-q_R)-u_Mq_M$.

At $u_M=u_R=u$ both channels clear at $u(1-q_M-q_R)$.

Costs. One unit of quality $v$ costs the manufacturer $kv^2$, with $k>0$. She pays a selling cost $c\ge0$ for each unit sold directly; the retailer's selling cost is $0$.

Profits. For a wholesale price $w$,

$$\Pi_R = (p_R-w)\,q_R,\qquad \Pi_M = (w-ku_R^2)\,q_R + (p_M-c-ku_M^2)\,q_M .$$

Timing without commitment.

1. The manufacturer announces the retailer's quality $u_R$ and the wholesale price $w$.
2. The retailer chooses its order $q_R$.
3. The manufacturer chooses the direct-channel quality $u_M$ and quantity $q_M$.

The game has perfect information and is solved by backward induction. A strategy profile $\sigma$ has three parts: a stage-1 choice $(w,u_R)$, a retailer rule $(w,u_R)\mapsto q_R$, and a stage-3 rule $(w,u_R,q_R)\mapsto(u_M,q_M)$. The profile is a subgame perfect equilibrium (SPE) when, at every history on or off the path, the mover's action is feasible and no feasible alternative gives the mover more. The manufacturer encroaches when $q_M>0$ on the equilibrium path.

Formalization targets

Goal: Proposition 7 (p. 21)

For every $k>0$, $c\ge0$ and every SPE $\sigma$ whose equilibrium path has $q_M>0$ and $q_R>0$,

$$u_M \neq u_R \quad\text{on the equilibrium path.}$$

Milestones (proof of Proposition 7, p. 37)

Write $u_M=\tau u_R$ with $\tau>0$.

1. Stage-3 value functions. For $\tau\ge1$ the optimal direct quantity is $q_M(\tau,q_R,u_R)=\big((-c-q_Ru_R-k\tau^2u_R^2+\tau u_R)/(2\tau u_R)\big)^+$. When it is positive the optimal profit is

$$\Pi^{HF}_M=\frac{(c+u_R(q_R+\tau(k\tau u_R-1)))^2}{4\tau u_R}+q_R(w-ku_R^2).$$

The case $\tau\le1$ gives $\Pi^{LF}_M$ in the same way, and the two agree at $\tau=1$. 2. Derivatives (31)–(32). The $\tau$-derivatives of $\Pi^{HF}_M$ and $\Pi^{LF}_M$, their values at $\tau=1$, and the equivalence

$$q_M(1,q_R,u_R)>0\iff c+u_R(q_R+ku_R-1)<0.$$

3. Stage-3 contradiction. At any history with $u_R>0$ and $q_R>0$, no optimal stage-3 choice has both $u_M=u_R$ and $q_M>0$.

Milestone 3 is stronger than the goal: it holds at every stage-3 history, not only on the equilibrium path.

Significance

The result. Proposition 7 shows that the structure of the optimal product line depends on the timing of design decisions. With commitment, the manufacturer sometimes keeps a single quality. A lower-quality direct product would draw a larger retail order but forgo market segmentation, and with some parameter values she accepts that trade. Without commitment, the direct-channel quality can no longer influence the retailer's order. She then always differentiates, so whenever both channels sell, consumers face a two-product line. The paper's numerical work (Figure 6) compares the two regimes. The analytical statement that differentiation is universal without commitment is this proposition.

Formalizing it. The proposition has a short, informal proof in the e-Companion. That proof argues through first-order conditions, "given that $\tau=1$ is optimal". It uses the strict signs printed in (31) and (32), although optimality gives only weak inequalities. Its contradiction relies on the retailer's order being positive, which the statement leaves implicit. A machine-checked proof pins down exactly which hypotheses the result needs. It also contributes reusable facts about Cournot-type stage games with vertically differentiated products. No part of this paper has been formalized before.

Difficulty

The stage-3 problem is a joint choice of quality $u_M$ and quantity $q_M$, and the demand system changes form at $u_M=u_R$, so the manufacturer's profit is not differentiable in $u_M$ there. The value function after optimizing $q_M$ is a piecewise expression: $\Pi^{HF}_M$ to the right of $\tau=1$, $\Pi^{LF}_M$ to the left, and the linear profit $q_R(w-ku_R^2)$ wherever the optimal $q_M$ is zero. An argument that $\tau=1$ is not optimal has to work with one-sided derivatives of this function at a kink. It must also check that the optimal quantity stays positive on both sides near $\tau=1$.

An obvious shortcut is to argue that differentiation is optimal because segmentation always pays. That argument fails at $q_R=0$. There the manufacturer is a one-product monopolist, and $u_M=u_R$ is optimal whenever $u_R$ happens to equal her monopoly quality. The positive retail order is therefore essential.

Formalization scope

All definitions live in the namespace QualityEncroach.NoCommit. They are real-valued throughout, and the formalization fixes the following conventions:

• the wholesale price $w$ ranges over $\mathbb R$, since the paper states no sign restriction;
• qualities satisfy $u_R,u_M>0$, and quantities satisfy $q_R,q_M\ge0$;
• the inverse demand is the formula above for all nonnegative quantities, as in the paper;
• the paper derives the case $u_M<u_R$ "similarly" (p. 15), and its explicit form is the one stated above;
• $\tau$ is not named in the paper's text; its formulas read $u_M=\tau u_R$;
• subgame perfection is stated in one-shot-deviation form at every history, which in this three-stage game is equivalent to subgame perfection;
• the goal adds the hypothesis $q_R>0$ on the path, reading "across channels" as both channels selling (see Difficulty).

A trivializing formalization is ruled out: the stage-3 rule maps $(w,u_R,q_R)$ to $(u_M,q_M)$, so $u_M$ is chosen after the order. Putting $u_M$ at stage 1 would give the committed game, where the proposition is false. The goal is conditional on an SPE existing, which the paper does not prove. A verification file checks the price formulas on hand instances in both branches. At $k=1$, $c=0.05$, $u_R=0.3$, $q_R=0.1$ and $w=0.15$, it checks that the basic parameter conditions hold and a uniform stage-3 choice is strictly beaten by $u_M=0.33$. The numerical check does not establish the existence of an optimal stage-3 choice or an SPE.

A complete development needs elementary real analysis only: maximization of concave quadratics, one-variable derivatives, and one-sided optimality conditions at a kink. Proofs of any milestone, and proofs of the goal from milestone 3, are welcome.

Selected references

• A. Y. Ha, X. Long, J. Nasiry, Quality in Supply Chain Encroachment, Manufacturing & Service Operations Management 18(2), 2016. https://doi.org/10.1287/msom.2015.0562 (authors' manuscript: https://ssrn.com/abstract=3970373)
• A. Arya, B. Mittendorf, D. E. M. Sappington, The Bright Side of Supplier Encroachment, Marketing Science 26(5), 651–659, 2007. https://doi.org/10.1287/mksc.1070.0280
• M. Mussa, S. Rosen, Monopoly and Product Quality, Journal of Economic Theory 18(2), 301–317, 1978. https://doi.org/10.1016/0022-0531(78)90085-6

Motivation

Best subset selection with ridge shrinkage asks for a coefficient vector $\beta\in\mathbb R^p$ that fits a response $y\in\mathbb R^n$ through a design matrix $X\in\mathbb R^{n\times p}$ while using few nonzero coefficients:

$$\min_{\beta\in\mathbb R^p}\ \tfrac12\|y-X\beta\|_2^2 + \lambda_0\|\beta\|_0 + \lambda_2\|\beta\|_2^2 .$$

This $\ell_0\ell_2$-regularized least squares problem is NP-hard, and exact methods solve it as a mixed integer program by branch-and-bound (BnB). The speed of BnB is governed by the strength of the continuous relaxation solved at every node: a larger relaxation value prunes more nodes. Hazimeh, Mazumder and Saab (arXiv:2004.06152, Mathematical Programming 2022) build the solver L0BnB on a perspective formulation and compare its relaxation with two standard alternatives. Their Proposition 1 quantifies that comparison, and their experiments (Section 4.2.1 of the paper) report speed-ups of more than 90× from using the perspective formulation with a tight bound $M$ instead of the bound-free formulation.

The mission formalizes Proposition 1 together with the three steps of its proof in the paper's Appendix A.

Setting

Fix $X$, $y$, regularization parameters $\lambda_0,\lambda_2>0$ and a bound $M>0$ on $\|\beta\|_\infty$; write $[p]=\{1,\dots,p\}$.

The Big-M formulation $B(M)$ introduces indicators $z_i$ and minimizes $\tfrac12\|y-X\beta\|_2^2+\lambda_0\sum_i z_i+\lambda_2\|\beta\|_2^2$ subject to $-Mz_i\le\beta_i\le Mz_i$, $z_i\in\{0,1\}$. Its interval relaxation lets $z_i\in[0,1]$; its optimal value is $V_{B(M)}$.

The reverse Huber penalty is $\mathcal B(t)=|t|$ for $|t|\le1$ and $(t^2+1)/2$ for $|t|\ge1$. Put

$$\psi_1(b;\lambda_0,\lambda_2)=2\lambda_0\,\mathcal B\big(b\sqrt{\lambda_2/\lambda_0}\big),\qquad \psi_2(b;\lambda_0,\lambda_2,M)=\Big(\frac{\lambda_0}{M}+\lambda_2M\Big)|b|,$$

and let $\psi=\psi_1$ if $\sqrt{\lambda_0/\lambda_2}\le M$ and $\psi=\psi_2$ if $\sqrt{\lambda_0/\lambda_2}>M$. The paper's Theorem 1 shows that the interval relaxation of the perspective formulation $\mathrm{PR}(M)$ is equivalent to

$$\min_{\|\beta\|_\infty\le M} F(\beta),\qquad F(\beta)=\tfrac12\|y-X\beta\|_2^2+\sum_{i\in[p]}\psi(\beta_i;\lambda_0,\lambda_2,M), \tag{5}$$

and $V_{PR(M)}$ denotes the optimal value of (5). Without a bound, the relaxation value of $\mathrm{PR}(\infty)$ is

$$V_{PR(\infty)}=\min_{\beta\in\mathbb R^p}G(\beta),\qquad G(\beta)=\tfrac12\|y-X\beta\|_2^2+\sum_{i\in[p]}\psi_1(\beta_i;\lambda_0,\lambda_2). \tag{6}$$

Finally $h(\lambda_0,\lambda_2,M)=\lambda_0/M+\lambda_2M-2\sqrt{\lambda_0\lambda_2}$, and $\beta^*$ denotes an optimal solution of (5).

Formalization targets

Goal: Proposition 1

For $\sqrt{\lambda_0/\lambda_2}>M$,

$$V_{PR(M)}\ \ge\ V_{B(M)}+\lambda_2\big(M\|\beta^*\|_1-\|\beta^*\|_2^2\big), \tag{7}$$ $$V_{PR(M)}\ \ge\ V_{PR(\infty)}+h(\lambda_0,\lambda_2,M)\,\|\beta^*\|_1. \tag{8}$$

Milestones

1. (37): $V_{B(M)}=\min_{\|\beta\|_\infty\le M}H(\beta)$ with $H(\beta)=\tfrac12\|y-X\beta\|_2^2+\sum_i\big(\tfrac{\lambda_0}{M}|\beta_i|+\lambda_2\beta_i^2\big)$; the Big-M relaxation expressed in $\beta$ alone. It holds for every $M>0$.
2. (7) alone.
3. The linear case of $\psi_1$: if $|b|\le M<\sqrt{\lambda_0/\lambda_2}$ then $\psi_1(b;\lambda_0,\lambda_2)=2|b|\sqrt{\lambda_0\lambda_2}$.
4. (8) alone (the paper's (38)).

The goal is the conjunction of milestones 2 and 4.

Significance

In the regime $\sqrt{\lambda_0/\lambda_2}>M$ both added terms are nonnegative: $M\|\beta^*\|_1\ge\|\beta^*\|_2^2$ because $\|\beta^*\|_\infty\le M$, and $h>0$ because $\lambda_0/M+\lambda_2M>2\sqrt{\lambda_0\lambda_2}$ whenever $M\ne\sqrt{\lambda_0/\lambda_2}$. So the perspective relaxation is at least as strong as both the Big-M relaxation and $\mathrm{PR}(\infty)$, strictly so as soon as one coordinate of $\beta^*$ lies strictly inside $(0,M)$ in absolute value (for (7)) or $\beta^*\ne0$ (for (8)). The bounds are explicit in the relaxation's own solution, so they can be evaluated at a BnB node. This is the theoretical justification for the paper's design choice of building its solver on $\mathrm{PR}(M)$ with a valid, tight $M$; the regime $\sqrt{\lambda_0/\lambda_2}\le M$, where (5) is (6) with the additional box constraint $\|\beta\|_\infty\le M$, is complementary.

Proposition 1 is proved in the paper; it has no machine-checked proof. The mission produces one, together with reusable Lean definitions of the three relaxation values and of the reverse Huber penalty that other statements about perspective relaxations of sparse regression can be stated against.

Difficulty

The arithmetic of the coordinate-wise penalties is short. The substance is in comparing optimal values that are defined as infima over different feasible sets. The obvious argument "$V_{PR(M)}-V_{B(M)}\ge F(\beta^*)-H(\beta^*)$" requires that the Big-M relaxation, which is posed over pairs $(\beta,z)$, have value at most $H(\beta^*)$; that is the content of (37), a statement about a different feasible set in more variables. Likewise (8) needs $V_{PR(\infty)}\le G(\beta^*)$, i.e. that the infimum in (6) is a genuine lower bound of a set bounded below, and both inequalities use the regime $\sqrt{\lambda_0/\lambda_2}>M$, in which $\psi=\psi_2$. Dropping the regime hypothesis makes (8) false in general: for $\sqrt{\lambda_0/\lambda_2}\le M$ one has $\psi=\psi_1$ and $h\ge0$, and the right side can exceed $V_{PR(M)}=V_{PR(\infty)}$.

Formalization scope

All objects live in the namespace L0BnB.Strength. Data are X : Matrix (Fin n) (Fin p) ℝ, y : Fin n → ℝ, reals lam0 lam2 M with 0 < lam0, 0 < lam2, 0 < M as hypotheses; $[p]$ is Fin p. Norms are explicit sums: $\|v\|_2^2$ is ∑ i, v i ^ 2, $\|\beta\|_1$ is ∑ i, |β i|, and $\|\beta\|_\infty\le M$ is ∀ i, |β i| ≤ M. The regime is written M < Real.sqrt (lam0 / lam2).

Optimal values are sInf of the image of the feasible set in ℝ. Each set is nonempty ($\beta=0$, $z=0$) and bounded below by $0$ under the positivity hypotheses, so sInf is the true infimum and never a junk value. $V_{B(M)}$ is defined over pairs $(\beta,z)$ with $z_i\in[0,1]$, not through $H$; (37) is a theorem. $V_{PR(\infty)}$ is (6) as printed: the paper attributes to its reference [21] the identification of (6) with the interval relaxation of $\mathrm{PR}(\infty)$ in $(\beta,z,s)$ variables, and that identification is not part of the mission. $V_{PR(M)}$ is the value of (5), which is the paper's definition; Theorem 1 (the equivalence of (5) with the $(\beta,z,s)$ relaxation) belongs to a sibling mission.

The optimal solution $\beta^*$ is a binder with the hypotheses $\|\beta^*\|_\infty\le M$ and $F(\beta^*)\le F(\beta)$ for every $\beta$ in the box. A formalization in which $\beta^*$ is an arbitrary feasible point, or in which $V_{B(M)}$ or $V_{PR(\infty)}$ is defined through a chosen minimizer, would change the statement and is ruled out. The paper uses no $O(\cdot)$ in this result, so no constant is instantiated.

Needed infrastructure is light: continuity of $H$ and compactness of the box for the attainment in (37), and csInf lemmas on ℝ. Contributions of proofs of any milestone, and of the attainment of the infimum in (5), are welcome.

Selected references

• H. Hazimeh, R. Mazumder, A. Saab, Sparse Regression at Scale: Branch-and-Bound rooted in First-Order Optimization, arXiv:2004.06152v2, 2021; Mathematical Programming (2022). https://arxiv.org/abs/2004.06152
• H. Hazimeh, R. Mazumder, Fast Best Subset Selection: Coordinate Descent and Local Combinatorial Optimization Algorithms, Operations Research 68(5), 1517–1537, 2020. https://doi.org/10.1287/opre.2019.1919
• H. Dong, K. Chen, J. Linderoth, Regularization vs. Relaxation: A conic optimization perspective of statistical variable selection, arXiv e-prints, 2015 (the paper's reference [21], source of (6) for $\mathrm{PR}(\infty)$). https://arxiv.org/abs/1510.06083

Motivation

Online retailers, search engines and streaming services show products on a sequence of pages, and most consumers look at only the first few. Which products are seen therefore depends on where they are placed. Gallego, Li, Truong and Wang (Operations Research, 2020) call the problem of placing products on pages to maximize expected revenue product framing. They show that it is NP-hard even with two pages and the multinomial logit model, and they give simple algorithms with constant-factor guarantees.

This mission concerns their second guarantee. In their basic model every consumer chooses with the same choice model, whatever the number of pages she views. In practice the number of pages viewed is itself informative: consumers who browse many pages may be keener buyers. Section 6 of the paper lets the choice model depend on the number of pages viewed and proposes the TRUNC algorithm for this setting. The guarantee is that TRUNC earns at least one third of the optimal expected revenue.

Setting

There are $n$ products with revenues $r_i\ge 0$ and $m$ virtual pages, each holding at most $p$ products; write $[k]=\{1,\dots,k\}$. A framing places each product on at most one page, with at most $p$ products per page. A consumer views a random number $X\in[m]$ of pages, with law $\lambda(x)=\mathbb P[X=x]$, tail $\Lambda(x)=\mathbb P[X\ge x]$ and failure rate $h(x)=\lambda(x)/\Lambda(x)$. Her consideration set is the set of products on pages $1,\dots,X$.

A consumer who views $x$ pages is of type $x$ and buys product $i$ from consideration set $S$ with probability $P_x(i,S)$, where $P_x(i,S)\ge 0$, $P_x(i,S)=0$ for $i\notin S$, and $\sum_{i\in S}P_x(i,S)\le 1$. The revenue of $S$ for type $x$ and the best capacitated revenue are

$$R_x(S)=\sum_{i\in S}r_iP_x(i,S),\qquad U(x)=\max_{S\subseteq[n],\ |S|\le xp}R_x(S).$$

A framing $f$ earns $\sum_{x\in[m]}\lambda(x)R_x(C_f(x))$, where $C_f(x)$ is the set of products on pages $1,\dots,x$. Its maximum over all framings is $V^{OPT}$. The assumptions are:

• B1: $R_x(S)\le R_y(S)$ whenever $x\le y$ and $|S|\le xp$;
• B2: $U(x)/x$ is nonincreasing in $x$;
• B3: problem (9) defining $U$ can be solved, here exactly;
• B4: $X$ has an increasing failure rate (IFR), i.e. $h$ is nondecreasing (Shaked and Shanthikumar 2007).

TRUNC($y$), for $y\in[m]$, picks an optimal assortment $S(y)$ for $U(y)$ and places it, in any arrangement, on pages $1,\dots,y$, leaving the remaining pages blank. TRUNC takes the best of these $m$ framings; its revenue is $V^{TRUNC}$.

The analysis passes through the bound-revealing program (10): minimize $\max_{x\in[m]}U(x)\Lambda(x)$ over nondecreasing $U\ge 0$ with $U(x)/x$ nonincreasing and over tails $1=\Lambda(1)\ge\cdots\ge\Lambda(m)\ge 0$ with $\Lambda(x+1)\Lambda(x-1)\le\Lambda(x)^2$, subject to $\sum_x\lambda(x)U(x)=1$.

Formalization targets

Goal: Theorem 4

Under Assumptions B1–B4, for every choice of optimal assortments and every arrangement on the pages,

$$V^{TRUNC}\;\ge\;\frac13\,V^{OPT}.$$

Milestones

In the order the proof uses them:

1. Upper bound (§6, p. 13): $V^{OPT}\le\mathbf E[U(X)]=\sum_x\lambda(x)U(x)$.
2. Lower bound (§6.1, p. 14): every run of TRUNC($y$) earns at least $U(y)\Lambda(y)$.
3. Lemma 8: for an IFR tail with $\Lambda>0$, $g(x)=x\Lambda(x)$ is weakly unimodal, and its largest maximizer is $\min\{x: h(x)>1/(x+1)\}$.
4. Proposition 5, Lemma 9, Proposition 6, Proposition 7: the structure of every optimal solution of (10) with $\Lambda>0$. With $y$ the largest maximizer of $U(x)\Lambda(x)$:
   • $U(x)/x$ is constant for $x\ge y$;
   • $y$ also maximizes $x\Lambda(x)$;
   • $U(x)\Lambda(x)$ is constant for $x\le y$;
   • $h$ is constant on $[y,m-1]$.
5. Value of (10) (A.4, p. 42): every feasible point of (10) has $\max_xU(x)\Lambda(x)\ge 1/3$.

Significance

The theorem shows that framing under type-dependent choice admits a constant-factor approximation using only $m$ calls to an assortment oracle, although the framing problem itself is NP-hard. The constant does not depend on the number of products, pages or page capacity. The bound-revealing program (10) is a self-contained extremal problem about log-concave tails and is reusable wherever a revenue curve with decreasing average returns meets an IFR horizon. The numerical value of (10) decreases with $m$ ($2/3$ at $m=2$, about $0.36$ at $m=40$), so the constant $1/3$ is approached only as the number of pages grows.

The result is proved in the paper. No part of it has a machine-checked proof: the platform has no item on product framing, discrete failure rates or program (10). A complete development would give a machine-checked proof of the approximation ratio. It would also give a checked treatment of the perturbation arguments of Appendix A.4, which the paper presents briefly.

Difficulty

Two steps are elementary: the upper bound (a consumer of type $x$ never sees more than $xp$ products) and the lower bound (every consumer of type $x\ge y$ sees all of $S(y)$).

The difficulty lies in the extremal problem (10). It is not convex: the IFR constraint is a log-concavity condition, and the objective is a maximum of products $U(x)\Lambda(x)$. A direct bound such as $\max_xU(x)\Lambda(x)\ge\sum_x\lambda(x)U(x)/m$ gives a constant that decays with $m$. The uniform constant comes from showing that the extremal tail is geometric beyond the maximizing page and that the extremal $U$ is pinned down on both sides of it. The paper reaches this structure through optimality conditions, so a formal proof must also establish that (10) attains its minimum, or must avoid that step.

Formalization scope

Products are Fin n. Pages are the natural numbers $1,\dots,m$, as in the paper, with $m\ge 1$ and $p\ge 1$. A framing is f : Fin n → ℕ: product $i$ is on page f i when $1\le f(i)\le m$, and f i = 0 means it is not displayed. The law $\lambda$ and the functions of (10) are functions on $\mathbb N$ of which only the values on $[m]$ are used, and $\Lambda(m+1)=0$.

$V^{OPT}$ and $U$ are maxima over finite nonempty families, and $V^{TRUNC}$ is a Finset.sup' over $y\in[m]$. TRUNC is a predicate on its outputs, not a function, and the goal is quantified over every family of runs. Assumption B3 is used with $\epsilon=0$, as everywhere in the paper. IFR is required only where the failure rate is defined ($\Lambda>0$), so laws whose support ends before page $m$ are allowed. Nonnegative revenues $r_i\ge 0$ are assumed; the lower bound of milestone 2 needs them.

No trivializing reading. The goal is not stated for one particular filling heuristic, or for some run only, and $V^{TRUNC}$ is the revenue of the framings themselves, not the lower bound $U(y)\Lambda(y)$.

Page numbers refer to the authors' accepted manuscript of the Operations Research article, which differ from the journal typesetting. The development needs only Mathlib (finite sums and maxima over Finset). Program (10) and Lemma 8 are independent of the framing model. Contributions are welcome at every milestone: Lemma 8 and the bound for (10) are the most self-contained.

Selected references

• G. Gallego, A. Li, V.-A. Truong, X. Wang, Approximation Algorithms for Product Framing and Pricing, Operations Research, 2020. https://doi.org/10.1287/opre.2019.1875
• M. Shaked, J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

Motivation

Best subset selection with ridge shrinkage asks for a sparse linear model: given a design matrix $X\in\mathbb R^{n\times p}$ and responses $y\in\mathbb R^n$, minimize

$$\tfrac12\|y-X\beta\|_2^2+\lambda_0\|\beta\|_0+\lambda_2\|\beta\|_2^2 ,$$

where $\|\beta\|_0$ counts nonzero coefficients. The problem is NP-hard, and exact methods solve it as a mixed integer program by branch-and-bound (Bertsimas, King, Mazumder 2016). The speed of branch-and-bound is governed by two things: how tight the continuous relaxation at each node is, and how cheaply that relaxation can be solved.

Hazimeh, Mazumder and Saab (arXiv:2004.06152v2; Mathematical Programming 2022) build a branch-and-bound solver whose node relaxations are solved by first-order methods rather than by a conic interior-point solver. Their starting point is the perspective formulation, a standard device for strengthening relaxations of mixed integer programs with indicator variables (Frangioni, Gentile 2006; Günlük, Linderoth 2010). Theorem 1 of the paper shows that the interval relaxation of this formulation is a box-constrained least squares problem with a separable penalty in $\beta$ alone. This mission formalizes Theorem 1.

Timeline. Owen (2007) introduced the reverse Huber penalty as a hybrid of lasso and ridge. Dong, Chen, Linderoth (2015) showed that the interval relaxation of the perspective formulation without a Big-M bound reduces to least squares with a reverse Huber penalty. Hazimeh, Mazumder and Saab (2020–2021) added the Big-M constraint and obtained Theorem 1, with a second regime in which the penalty becomes $\ell_1$.

Setting

Fix $X\in\mathbb R^{n\times p}$, $y\in\mathbb R^n$, $\lambda_0>0$, $\lambda_2>0$ and $M>0$, and write $[p]=\{1,\dots,p\}$. The perspective formulation $\mathrm{PR}(M)$ is problem (3) of the paper:

$$\min_{\beta,z,s}\ \tfrac12\|y-X\beta\|_2^2+\lambda_0\sum_{i\in[p]}z_i+\lambda_2\sum_{i\in[p]}s_i \quad\text{s.t.}\quad \beta_i^2\le s_iz_i,\ \ -Mz_i\le\beta_i\le Mz_i,\ \ z_i\in\{0,1\},\ \ s_i\ge0 .$$

Here $z_i$ indicates whether $\beta_i$ may be nonzero, $s_i$ stands in for $\beta_i^2$ through the rotated second-order cone constraint $\beta_i^2\le s_iz_i$, and $M$ bounds $|\beta_i|$. The interval relaxation replaces $z_i\in\{0,1\}$ with $z_i\in[0,1]$.

The reverse Huber penalty (4) is $\mathcal B(t)=|t|$ for $|t|\le1$ and $\mathcal B(t)=(t^2+1)/2$ for $|t|\ge1$. Put

$$\psi_1(b;\lambda_0,\lambda_2)=2\lambda_0\,\mathcal B\big(b\sqrt{\lambda_2/\lambda_0}\big),\qquad \psi_2(b;\lambda_0,\lambda_2,M)=\Big(\frac{\lambda_0}{M}+\lambda_2M\Big)|b|,$$

and let $\psi=\psi_1$ if $\sqrt{\lambda_0/\lambda_2}\le M$ and $\psi=\psi_2$ if $\sqrt{\lambda_0/\lambda_2}>M$. The reduced relaxation (5) is

$$\min_{\beta\in\mathbb R^p}\ F(\beta):=\tfrac12\|y-X\beta\|_2^2+\sum_{i\in[p]}\psi(\beta_i;\lambda_0,\lambda_2,M)\quad\text{s.t.}\quad\|\beta\|_\infty\le M ,$$

with optimal value $V_{\mathrm{PR}(M)}$. For one coordinate $b$, $\omega(b;\lambda_0,\lambda_2,M)$ is the minimum of $\lambda_0z+\lambda_2s$ over $b^2\le sz$, $-Mz\le b\le Mz$, $z\in[0,1]$, $s\ge0$.

Formalization targets

Goal: Theorem 1 (Reduced Relaxation), p. 6

The interval relaxation of (3) is equivalent to (5):

$$\exists\,(z,s):\ (\beta,z,s)\ \text{feasible}\iff\|\beta\|_\infty\le M,\qquad \min_{z,s}\Big\{\tfrac12\|y-X\beta\|_2^2+\lambda_0\textstyle\sum_i z_i+\lambda_2\sum_i s_i\Big\}=F(\beta)\ \ (\|\beta\|_\infty\le M),$$

and both problems attain the common optimal value $V_{\mathrm{PR}(M)}$.

Milestones (proof of Theorem 1, p. 28)

1. Reduction to (36). For $|b|\le M$, the smallest feasible $z$ is $\hat z=\max\{b^2/s,|b|/M\}$, so

$$\omega(b;\lambda_0,\lambda_2,M)=\min_{s\ge b^2}\max\Big\{\lambda_0\tfrac{b^2}{s}+\lambda_2s,\ \lambda_0\tfrac{|b|}{M}+\lambda_2s\Big\}.$$

2. Case I. If $\sqrt{\lambda_0/\lambda_2}\le M$ and $|b|\le M$, then $\omega(b;\lambda_0,\lambda_2,M)=2\lambda_0\mathcal B(b\sqrt{\lambda_2/\lambda_0})$.
3. Case II. If $\sqrt{\lambda_0/\lambda_2}>M$ and $|b|\le M$, then $\omega(b;\lambda_0,\lambda_2,M)=(\lambda_0/M+\lambda_2M)|b|$.

Significance

The result. Theorem 1 removes the $2p$ auxiliary variables $z,s$ and all conic constraints from the node relaxation. What remains is a composite problem, a smooth least squares loss plus a separable, convex penalty under a box constraint, to which coordinate descent and proximal methods apply directly. The paper's solver, its active-set strategy, and the dual bounds of its Section 3 are all built on (5). The theorem also exposes a regime change: when $\sqrt{\lambda_0/\lambda_2}>M$, the ridge term of the perspective formulation disappears from the relaxation and the penalty is pure $\ell_1$. Propositions 1 and 2 of the paper, which compare the strengths of the perspective, Big-M and $\mathrm{PR}(\infty)$ relaxations, use this reduced form.

Formalizing it. The result is proved in the paper (Appendix A) by a coordinatewise argument. To our knowledge it has no machine-checked proof. Formalizing it gives a verified bridge from the conic mixed integer formulation to the penalized form that later results of the paper use, and a checked case analysis at the regime boundary $\sqrt{\lambda_0/\lambda_2}=M$, where the two formulas must agree with the stated tie-breaking.

Difficulty

The obvious approach, "minimize over $z$ and $s$ coordinate by coordinate", is correct in outline, but each step hides a boundary case. The rotated cone constraint $\beta_i^2\le s_iz_i$ degenerates at $s_i=0$ or $z_i=0$, where $\beta_i^2/s_i$ is undefined, and the paper's convention for $\beta_i=s_i=0$ must be handled. The one-variable problem (36) is a minimum of a pointwise maximum of two functions of $s$, one convex and decreasing then increasing, the other increasing. Its minimizer lies either in the interior of the region where the first term dominates or on the crossover $s=|b|M$, depending on the regime. The paper's proof describes the cases loosely: it optimizes the Case I term without imposing the side condition that Case I attains the maximum. A complete argument must prove the lower bound over all feasible $s$, not just evaluate at a candidate. Finally, the minimum over $(z,s)\in\mathbb R^{2p}$ must be shown to split into a sum of coordinate minima, each attained.

Formalization scope

Data are X : Matrix (Fin n) (Fin p) ℝ, y : Fin n → ℝ, and reals lam0 lam2 M with 0 < lam0, 0 < lam2, 0 < M; the paper's $[p]$ is Fin p. The squared norm $\|y-X\beta\|_2^2$ is the explicit sum $\sum_r(y_r-(X\beta)_r)^2$, and $\|\beta\|_\infty\le M$ is $|\beta_i|\le M$ for all $i$. The cone constraint is kept in product form $\beta_i^2\le s_iz_i$. In $\hat z$ and (36), Lean's $b^2/0=0$ coincides with the paper's convention $\beta_i^2/s_i=0$ for $\beta_i=s_i=0$. Every "min" is stated with IsLeast (membership plus lower bound), so attainment is part of each statement. $V_{\mathrm{PR}(M)}$ is defined as a real infimum over the box, and Theorem 1 asserts that this infimum is attained by both problems. No normalization of $X$ or $y$ is assumed; the paper's unit-norm assumption starts in Section 3. The paper writes no $O(\cdot)$ in these results, so there are no constants to instantiate.

A goal stating only one inequality (that $F(\beta)$ is achieved by some $(z,s)$, or that it bounds the relaxation from below), or a goal over $z_i\in\{0,1\}$, would not be Theorem 1. The IsLeast form rules out both. The goal uses $\psi$ with both regimes.

A complete development needs: a two-variable convexity argument for $\lambda_0b^2/s+\lambda_2s$ on $s>0$; a lemma that the infimum of a separable objective over a product of feasible sets is the sum of the coordinate infima; and continuity of $F$ with compactness of the box to obtain an optimal $\beta$. The coordinate lemmas and the definition of the reverse Huber penalty are reusable in the companion missions on relaxation strength and Lagrangian duality. Contributions to any milestone, or an alternative proof of the goal, are welcome.

Selected references

• H. Hazimeh, R. Mazumder, A. Saab, Sparse Regression at Scale: Branch-and-Bound rooted in First-Order Optimization, arXiv:2004.06152v2 (2021); Mathematical Programming (2022). https://arxiv.org/abs/2004.06152v2
• A. Frangioni, C. Gentile, Perspective cuts for a class of convex 0–1 mixed integer programs, Mathematical Programming 106(2), 225–236, 2006. https://doi.org/10.1007/s10107-005-0594-3
• O. Günlük, J. Linderoth, Perspective reformulations of mixed integer nonlinear programs with indicator variables, Mathematical Programming 124(1–2), 183–205, 2010. https://doi.org/10.1007/s10107-010-0360-z
• H. Dong, K. Chen, J. Linderoth, Regularization vs. Relaxation: A conic optimization perspective of statistical variable selection, arXiv:1510.06083, 2015. https://arxiv.org/abs/1510.06083
• A. B. Owen, A robust hybrid of lasso and ridge regression, Contemporary Mathematics 443, 59–72, 2007. https://doi.org/10.1090/conm/443/08555
• D. Bertsimas, A. King, R. Mazumder, Best subset selection via a modern optimization lens, Annals of Statistics 44(2), 813–852, 2016. https://doi.org/10.1214/15-AOS1388