Operations Research

Motivation

Martingale optimal transport asks for the cheapest way to couple two given laws $\mu$ and $\nu$ of a price at two dates under the constraint that the coupling is a martingale: the conditional mean of the later price given the earlier one equals the earlier one. It is the model-independent pricing problem of mathematical finance: given the marginal laws implied by vanilla option prices, the extreme values of $E[c(X,Y)]$ over all martingale couplings bound the price of the exotic payoff $c$ (Beiglböck, Henry-Labordère, Penkner 2013; Galichon, Henry-Labordère, Touzi 2014). In the classical (non-martingale) transport problem, the shape of the cost determines the shape of the optimal coupling: for strictly convex costs of $y-x$ on the line the optimizer is a monotone map. The question this mission addresses is the martingale analogue: how much can an optimal martingale coupling split a single starting point, as a function of the cost?

Beiglböck and Juillet (arXiv:1208.1509, Ann. Probab. 2016) introduced the variational lemma for this problem and used it to prove, among other results, that the left-curtain coupling is optimal for a family of costs and that, for costs $h(y-x)$, the number of points into which an optimal plan sends a non-atom of $\mu$ is bounded by a geometric property of $h'$ alone (their Theorem 7.1). This mission formalizes that bound.

Setting

All measures are Borel measures on $\mathbb R$ or $\mathbb R^2$. A martingale transport plan between probability measures $\mu,\nu$ on $\mathbb R$ is a measure $\pi$ on $\mathbb R\times\mathbb R$ with marginals $\mu$ and $\nu$ such that $\int\rho(x)(y-x)\,d\pi(x,y)=0$ for every bounded Borel $\rho$; equivalently, the disintegration $(\pi_x)$ of $\pi$ along its first coordinate satisfies $\int y\,d\pi_x(y)=x$ for $\mu$-almost every $x$. The set of such plans is $\Pi_M(\mu,\nu)$; it is nonempty exactly when $\mu$ and $\nu$ are in convex order, $\mu\preceq_C\nu$, meaning $\int\varphi\,d\mu\le\int\varphi\,d\nu$ for every convex $\varphi$.

A cost is a function $c:\mathbb R^2\to\mathbb R$. It satisfies the sufficient integrability condition if $c(x,y)\ge a(x)+b(y)$ for some $a\in L^1(\mu)$, $b\in L^1(\nu)$; then $E_\pi[c]=\int c\,d\pi\in(-\infty,+\infty]$ is well defined for every plan. A plan $\pi\in\Pi_M(\mu,\nu)$ is optimal if $E_\pi[c]\le E_{\pi'}[c]$ for every $\pi'\in\Pi_M(\mu,\nu)$.

A competitor of a finitely supported measure $\alpha$ on $\mathbb R^2$ is a measure $\alpha'$ with the same two marginals and the same conditional barycentres $\int y\,d\alpha_x(y)$. For a set $\Gamma\subseteq\mathbb R^2$, $\Gamma_x=\{y:(x,y)\in\Gamma\}$ is its fibre over $x$.

This mission concerns costs of the form $c(x,y)=h(y-x)$ with $h:\mathbb R\to\mathbb R$ twice continuously differentiable, and the hypothesis that affine functions meet $h'$ in at most $k$ points: for all $s,t\in\mathbb R$, $|\{x:h'(x)=sx+t\}|\le k$. For instance $h(t)=t^4$ satisfies it with $k=3$.

Formalization targets

Goal: Theorem 7.1 (p. 38)

Under the hypotheses above, with $\pi$ an optimal martingale plan of finite cost, there is a disintegration $(\pi_x)_{x\in\mathbb R}$ of $\pi$ such that for every $x\in\mathbb R$

$$\mu(\{x\})>0\qquad\text{or}\qquad\operatorname{card}(\operatorname{spt}\pi_x)\le k,$$

and if $\mu$ has no atoms, $\operatorname{card}(\operatorname{spt}\pi_x)\le k$ holds $\mu$-almost surely for every disintegration of $\pi$.

Milestones

1. Lemma 1.11 (variational lemma, p. 8): an optimal plan of finite cost is concentrated on a Borel set $\Gamma$ such that no finitely supported $\alpha$ with $\operatorname{spt}\alpha\subseteq\Gamma$ has a strictly cheaper competitor.
2. Lemma 3.2 (p. 19): if uncountably many fibres $\Gamma_a$ have at least $k$ points, some $(a,b_1<\dots<b_k)$ is a limit of such configurations from the right and from the left.
3. An interior point off the chord (proof of Theorem 7.1, p. 39): for $b_0<\dots<b_k$, some interior $b_i$ has $h'(b_i-a)$ off the chord of $h'(\cdot-a)$ through $b_0,b_k$.
4. The local sign (p. 39): near such $(a,b_i)$, the cost difference (17) − (18) of a three-point rerouting is nonzero with sign fixed by $a-a'$.
5. Countably many exceptional points (pp. 38–39): on such a $\Gamma$, only countably many continuity points $x$ of $\mu$ have $|\Gamma_x|\ge k+1$.

Significance

The result itself. Theorem 7.1 converts a one-dimensional condition on $h'$ into a sparsity statement for every optimal martingale coupling: non-atoms of $\mu$ are sent to at most $k$ points. For $h(t)=t^4$ this gives at most three points, and Section 7.3 of the paper gives an example with continuous $\mu$ where the optimizer splits into more than two points, so for this cost the bound cannot be lowered to two. For costs where $h'$ is strictly convex (so $k=2$), it gives the two-point structure also enjoyed by the left-curtain coupling, which is optimal for those costs (Theorem 1.9). Such support bounds are what make the optimizers computable and the corresponding robust price bounds explicit.

Formalizing it. The theorem is proved in the paper; to our knowledge none of it is formalized. A formal proof requires machine-checked versions of the variational lemma (itself resting on a duality theorem of Kellerer type), the countability argument of Lemma 3.2, and the real-analysis estimate behind the three-point rerouting. Each of these is reusable: Lemma 1.11 drives every structural result of the paper, and Lemma 3.2 is used again for the left-monotonicity theorems.

Difficulty

The natural first attempt is to argue pointwise: if a fibre $\Gamma_a$ has $k+1$ points, reroute mass within that fibre to lower the cost. This fails, because a competitor must preserve the barycentre of each fibre, and within a single fibre no rerouting both preserves the barycentre and the marginals. Any improvement must move mass between two different starting points $a$ and $a'$, and this requires the two fibres to be close to each other and arranged consistently, which a single fibre cannot guarantee. Producing such pairs of fibres needs uncountably many exceptional points (Lemma 3.2) and the set $\Gamma$ of the variational lemma, whose existence is the deep part (it rests on a duality theorem for measures with given marginals). A second difficulty is that the conclusion is required at every non-atom $x$, not only almost everywhere, so the exceptional set must be controlled exactly.

Formalization scope

Lean represents measures with Mathlib's Measure ℝ and Measure (ℝ × ℝ). $\Pi_M$ is encoded through the test-function characterization $\int\rho(x)(y-x)\,d\pi=0$ for bounded Borel $\rho$; costs are extended-real integrals $\int c^+-\int c^-\in[-\infty,+\infty]$ (the published ModelRiskOT.Duality.extIntegral); competitors of a finitely supported $\alpha=\sum_{s\in S}w_s\delta_s$ are encoded through the same test-function device. A disintegration is a Markov kernel $\kappa$ with $\pi=\mu\otimes\kappa$, and $\operatorname{card}(\operatorname{spt}\pi_x)\le k$ is written as "$\kappa(x)$ is concentrated on a set of at most $k$ points", which is equivalent for probability measures on $\mathbb R$. Cardinalities take values in $\mathbb N\cup\{\infty\}$; $h'$ is deriv h.

Standing and added hypotheses of the goal: $\mu,\nu$ are probability measures in convex order; "optimal transport plan" means optimal martingale plan, as throughout Section 7; and, because the proof starts from Lemma 1.11, the hypotheses of that lemma are added: the sufficient integrability condition for $c$ and finite cost of $\pi$. "Continuous $\mu$" is $\mu(\{x\})=0$ for every $x$.

The conclusion is not trivialized: the first part holds for every $x$ with a single chosen kernel, not almost everywhere, and the second part quantifies over all kernels, not one. The hypotheses are jointly satisfiable (for example $h(t)=t^4$, $k=3$, $\mu=\nu=\delta_0$).

A complete development needs disintegration of measures on $\mathbb R^2$ (available in Mathlib as condKernel), the variational lemma with its duality ingredient, and elementary real analysis. Contributions to the variational lemma are reusable across the whole series of missions on this paper.

Selected references

• M. Beiglböck, N. Juillet, On a problem of optimal transport under marginal martingale constraints, Ann. Probab. 44(1), 42–106, 2016. arXiv:1208.1509
• M. Beiglböck, P. Henry-Labordère, F. Penkner, Model-independent bounds for option prices — a mass transport approach, Finance Stoch. 17, 477–501, 2013. doi:10.1007/s00780-013-0205-8
• A. Galichon, P. Henry-Labordère, N. Touzi, A stochastic control approach to no-arbitrage bounds given marginals, with an application to lookback options, Ann. Appl. Probab. 24(1), 312–336, 2014. doi:10.1214/13-AAP925
• M. Beiglböck, M. Goldstern, G. Maresch, W. Schachermayer, Optimal and better transport plans, J. Funct. Anal. 256(6), 1907–1927, 2009. doi:10.1016/j.jfa.2009.01.013

Motivation

Minimizing a convex function $g$ on a real Hilbert space $\mathcal H$ by first-order methods has a continuous-time counterpart: second-order differential equations whose trajectories descend $g$. Su, Boyd and Candès (20) showed that Nesterov's accelerated gradient method is a discretization of $\ddot x+\frac{\alpha}{t}\dot x+\nabla g(x)=0$ with $\alpha=3$, along which $g(x(t))-\min g=O(1/t^2)$. Two modifications of this equation have been studied separately because each adds a property the plain system lacks.

• A Hessian-driven damping term $\beta\nabla^2g(x(t))\dot x(t)$ (Attouch, Peypouquet, Redont, J. Differential Equations 2016) damps oscillations and, for $\beta>0$, makes $t^2\|\nabla g(x(t))\|^2$ integrable, while keeping fast values and weak convergence of trajectories.
• A Tikhonov regularization term $\epsilon(t)x(t)$ with $\epsilon(t)\downarrow0$ (Attouch, Chbani, Riahi, J. Math. Anal. Appl. 2018) can steer trajectories to the minimum-norm minimizer.

Boţ, Csetnek and László (arXiv:1911.12845v2, 2020) combine both terms and ask which properties of the two parent systems survive. This mission covers the first of their answers: when $\epsilon$ decays fast enough, the fast rates and the weak convergence of trajectories are preserved.

Timeline. 2016 (published 2018): weak convergence of trajectories of $\ddot x+\frac\alpha t\dot x+\nabla g(x)=0$ for $\alpha>3$ (Attouch, Chbani, Peypouquet, Redont, Math. Program. 168). 2016: the same with Hessian-driven damping, $\beta>0$ (Attouch, Peypouquet, Redont). 2018: Tikhonov regularization of that system, with the $O(1/t^2)$ rate kept and strong convergence to the minimum-norm minimizer under slow decay of $\epsilon$ (Attouch, Chbani, Riahi). 2020: both terms together (Boţ, Csetnek, László, this paper).

Setting

Fix a real Hilbert space $\mathcal H$, a starting time $t_0>0$, parameters $\alpha\ge3$ and $\beta\ge0$, and initial data $u_0,v_0\in\mathcal H$. The General assumption of the paper is:

• $g:\mathcal H\to\mathbb R$ is convex and twice Fréchet differentiable, $\nabla g$ is Lipschitz continuous on bounded sets, and $\operatorname{argmin} g\ne\emptyset$; $\min g$ denotes its minimal value;
• $\epsilon:[t_0,+\infty)\to[0,+\infty)$ is nonincreasing, of class $C^1$, and $\epsilon(t)\to0$ as $t\to+\infty$.

The dynamical system is

$$\ddot x(t)+\frac{\alpha}{t}\dot x(t)+\beta\nabla^2g(x(t))\dot x(t)+\nabla g(x(t))+\epsilon(t)x(t)=0,\quad t\ge t_0,\quad x(t_0)=u_0,\ \dot x(t_0)=v_0. \tag{5}$$

A global $C^2$-solution is a twice continuously differentiable $x:[t_0,+\infty)\to\mathcal H$ satisfying (5) for every $t\ge t_0$. The decay of $\epsilon$ is controlled by $\int_{t_0}^{+\infty}t\epsilon(t)\,dt<+\infty$ together with one of two conditions:

• (a) there exist $a>1$ and $t_1\ge t_0$ with $\dot\epsilon(t)\le-\frac{a\beta}{2}\epsilon^2(t)$ for all $t\ge t_1$;
• (b) there exist $a>0$ and $t_1\ge t_0$ with $\epsilon(t)\le\frac at$ for all $t\ge t_1$.

A curve $x(t)$ converges weakly to $\bar x$ if $\langle x(t),v\rangle\to\langle\bar x,v\rangle$ for every $v\in\mathcal H$. The Lean development lives in the namespace TikhonovHDD.Weak, with IsSolution, GenAssumptionG, GenAssumptionEps, CondA, CondB, argmin, minVal and WeakTendstoAtTop for these objects.

Formalization targets

Goal: Theorem 3.5 (p. 15)

Under the General assumption, $\int_{t_0}^{+\infty}t\epsilon(t)\,dt<+\infty$ and (a) or (b), if $\alpha>3$ then every global $C^2$-solution of (5) satisfies

$$\exists\,\bar x\in\operatorname{argmin} g:\qquad x(t)\rightharpoonup\bar x\quad(t\to+\infty).$$

Milestones

In the order the argument uses them:

1. Theorem 2.1 (p. 4): existence and uniqueness of a global $C^2$-solution of (5).
2. Lemma A.2 (p. 29): a bounded-below, locally absolutely continuous $F$ with $\dot F\le G\in L^1$ a.e. has a finite limit.
3. Theorem 3.3 (p. 11), split three ways: for $\alpha\ge3$, $g(x(t))-\min g=O(1/t^2)$; for $\alpha>3$, $x$ is bounded and $t(g(x(t))-\min g)$, $t\|\dot x\|^2$, $t\epsilon\|x-x^*\|^2$, $t\epsilon\|x\|^2\in L^1$; and separately $t^2\|\nabla g(x(t))\|^2\in L^1$.
4. Lemma A.3 (p. 30): $u(t)+\frac t\alpha\dot u(t)\to\bar u$ with $\alpha>0$ implies $u(t)\to\bar u$.
5. Theorem 3.4 (p. 12): for $\alpha>3$ and every $x^*\in\operatorname{argmin} g$, $t\langle\nabla g(x),x-x^*\rangle\in L^1$, $\lim\|x(t)-x^*\|$ and $\lim t\langle\dot x+\beta\nabla g(x),x-x^*\rangle$ exist, $g(x(t))-\min g=o(1/t^2)$, $\|\dot x+\beta\nabla g(x)\|=o(1/t)$, and $t^2\epsilon(t)\|x(t)\|^2\to0$.

Significance

The result. Theorem 3.5 shows that the Tikhonov term, when it decays at least as fast as $\int t\epsilon<\infty$ requires, does not disturb the asymptotics of the Hessian-damped system: values converge at rate $o(1/t^2)$ and trajectories converge weakly to a minimizer. With $\beta=0$ it recovers the corresponding results for the regularized system without Hessian damping, and with $\epsilon\equiv0$ those for the Hessian-damped system. It is also the boundary case of the paper's second half, where slower decay of $\epsilon$ is shown to give strong convergence to the minimum-norm minimizer instead.

Formalizing it. The results are proved in the paper; none of them is machine-checked. A formal development would produce reusable pieces: a Lyapunov-energy analysis of second-order systems with time-dependent coefficients, the asymptotic Lemmas A.2 and A.3, and the bridge from "the distance to every minimizer converges and weak cluster points are minimizers" to weak convergence of a curve (the continuous Opial lemma).

Difficulty

The obvious approach, a single Lyapunov function that decreases along trajectories, fails here: the Tikhonov term makes the natural energy $\mathcal E_b$ only almost nonincreasing, with an error $\propto t\epsilon(t)\|x^*\|^2$ that must be integrated, and the Hessian term produces a cross term $-\beta\epsilon(t)t^2\langle\nabla g(x),x\rangle$ that is controlled only by condition (a) or (b). The step from $O(1/t^2)$ to $o(1/t^2)$ and to the existence of $\lim\|x(t)-x^*\|$ cannot be read off a single bounded energy: boundedness of $\mathcal E_b$ gives rates in $O$, not in $o$, and says nothing directly about $\|x(t)-x^*\|$. Weak convergence then requires Opial's lemma, which is not in Mathlib in continuous form. Existence of solutions is itself nontrivial in infinite dimension: the right-hand side involves $\nabla^2g$, so the system has to be rewritten as a first-order system before the Cauchy–Lipschitz theorem applies.

Formalization scope

• $\mathcal H$ is any real Hilbert space (InnerProductSpace ℝ H, CompleteSpace H); nothing is finite-dimensional, so weak convergence is genuinely weaker than norm convergence. It is stated through inner products with every $v\in\mathcal H$; stating it as norm convergence, or testing only some $v$, would change the theorem.
• Trajectories are maps $\mathbb R\to\mathcal H$ with velocity and acceleration maps; derivatives are one-sided at $t_0$ and values before $t_0$ play no role. Every theorem is stated for every $C^2$-solution; Theorem 2.1 shows this class is a singleton, so the hypothesis is not vacuous. A sorry-free check that the hypotheses of the goal can be met ($g=0$, $\epsilon=0$, $x=0$) accompanies the drafts.
• $\nabla^2g(x)v$ is the derivative of $\nabla g$ at $x$ applied to $v$; $\dot\epsilon$ is a derivative map tied to $\epsilon$ on $[t_0,+\infty)$; $\min g=\inf g$, attained since $\operatorname{argmin} g\ne\emptyset$; $L^1$ membership is Lebesgue integrability on $[t_0,+\infty)$ (never a comparison of a Bochner integral with a number); $O$, $o$ are Asymptotics relations at $+\infty$.
• Repair. Theorem 2.1 carries the extra hypothesis "$\beta=0$ or $g\in C^2$". As printed (only twice differentiable $g$) it is false for $\beta>0$: on $\mathbb R$, $g'(x)=2x+x^2\sin(1/x)$ gives a strongly convex $g$ with bounded but discontinuous $g''$, and the solution from $u_0=0$, $v_0=1$ is not $C^2$. The paper's own proof uses continuity of $\nabla^2 g$.
• Flagged, not repaired. The last claim of Theorem 3.3, $t^2\|\nabla g(x(t))\|^2\in L^1$, is its own item: the paper's argument for it uses a term proportional to $\beta$, so for $\beta=0$ the paper gives no proof. No counterexample is known, and the statement is drafted as printed.
• Referenced, not re-posed. Lemma A.4 (continuous Opial lemma, p. 30), the last step of the goal's proof, is the published InertialAVD.Traj.lemma_A_2 (same hypotheses: $S$ nonempty, $\lim\|x(t)-z\|$ exists for every $z\in S$, every weak sequential limit point lies in $S$; same conclusion). It is a reference milestone of this mission; its weak convergence InertialAVD.Traj.WeakTendstoAtTop has the same body as TikhonovHDD.Weak.WeakTendstoAtTop.
• The model is defined from scratch: the published HessianDamping.DINAVD.Setting concerns a different equation (no $\epsilon x$ term) and is not reused.
• Welcome contributions: a general Cauchy–Lipschitz existence theorem for locally Lipschitz first-order systems in Banach spaces on $[t_0,+\infty)$ with a blow-up alternative, the continuous Opial lemma, and Lemma A.2 for absolutely continuous functions.

Selected references

• R.I. Boţ, E.R. Csetnek, S.C. László, Tikhonov regularization of a second order dynamical system with Hessian driven damping, arXiv:1911.12845v2, 2020; published in Math. Program., https://doi.org/10.1007/s10107-020-01528-8. https://arxiv.org/abs/1911.12845v2
• H. Attouch, J. Peypouquet, P. Redont, Fast convex optimization via inertial dynamics with Hessian driven damping, J. Differential Equations 261(10), 5734–5783, 2016. https://doi.org/10.1016/j.jde.2016.08.020
• H. Attouch, Z. Chbani, H. Riahi, Combining fast inertial dynamics for convex optimization with Tikhonov regularization, J. Math. Anal. Appl. 457(2), 1065–1094, 2018. https://doi.org/10.1016/j.jmaa.2016.12.017
• H. Attouch, Z. Chbani, J. Peypouquet, P. Redont, Fast convergence of inertial dynamics and algorithms with asymptotic vanishing viscosity, Math. Program. 168, 123–175, 2018. https://doi.org/10.1007/s10107-016-0992-8
• W. Su, S. Boyd, E.J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, J. Mach. Learn. Res. 17(153), 1–43, 2016. https://jmlr.org/papers/v17/15-084.html

Motivation

Many methods for minimizing a smooth convex function $g$ on a Hilbert space can be read as discretizations of second order ordinary differential equations, and the asymptotic behaviour of the continuous trajectories predicts the behaviour of the iterates. The inertial system with vanishing damping $\ddot x+\frac{\alpha}{t}\dot x+\nabla g(x)=0$ is the continuous counterpart of Nesterov's accelerated gradient method (Su, Boyd, Candès 2016); for $\alpha>3$ its trajectories converge weakly to some minimizer of $g$ (Attouch, Chbani, Peypouquet, Redont 2018). Two modifications of this system have been studied separately. A Hessian driven damping term $\beta\nabla^2g(x)\dot x$ reduces oscillations while keeping the fast rate of the values (Attouch, Peypouquet, Redont 2016). A Tikhonov regularization term $\epsilon(t)x$ with $\epsilon(t)\to 0$ selects a particular minimizer: under suitable decay of $\epsilon$, trajectories approach the minimizer of minimum norm in the strong (norm) topology (Attouch, Chbani, Riahi 2018).

Boţ, Csetnek and László (arXiv:1911.12845v2, published in Mathematical Programming 2021) combine both terms and ask which properties of the two separate systems survive. This mission formalizes their strong convergence result, Theorem 4.4.

Setting

Let $\mathcal H$ be a real Hilbert space, $t_0>0$, $\alpha\ge 3$, $\beta\ge0$, and $u_0,v_0\in\mathcal H$. The General assumption of the paper (p. 2) is:

• $g:\mathcal H\to\mathbb R$ is convex and twice Fréchet differentiable, $\nabla g$ is Lipschitz continuous on bounded sets, and $\operatorname{argmin} g\neq\emptyset$;
• $\epsilon:[t_0,+\infty)\to[0,+\infty)$ is nonincreasing, of class $C^1$, and $\lim_{t\to+\infty}\epsilon(t)=0$.

A global $C^2$-solution of the system

$$\ddot x(t)+\frac{\alpha}{t}\dot x(t)+\beta\nabla^2g(x(t))\dot x(t)+\nabla g(x(t))+\epsilon(t)x(t)=0,\quad t\ge t_0,\qquad x(t_0)=u_0,\ \dot x(t_0)=v_0, \tag{5}$$

is a twice continuously differentiable curve $x:[t_0,+\infty)\to\mathcal H$ satisfying (5) at every $t\ge t_0$. The set $\operatorname{argmin} g$ is nonempty, closed and convex, so it has a unique element of minimum norm, denoted $x^*$. The open ball $B(0,\|x^*\|)$ is $\{y:\|y\|<\|x^*\|\}$. In the Lean development these objects are GeneralAssumption g t₀ ε ε', IsSolution g α β t₀ ε u₀ v₀ x xd xdd and IsMinNormMinimizer g xstar in the namespace TikhonovHDD.Strong, with $\min g$ written minValue g.

Formalization targets

Goal: Theorem 4.4 (p. 21)

Assume, in addition to the above,

$$\int_{t_0}^{+\infty}\frac{\epsilon(t)}{t}\,dt<+\infty,\qquad \lim_{t\to+\infty}\frac{\beta}{\epsilon(t)t^{\frac{\alpha}{3}+1}}\int_{t_0}^{t}\epsilon^2(s)s^{\frac{\alpha}{3}+1}\,ds=0,$$

that $\dot\epsilon(t)\le-\frac{a\beta}{2}\epsilon^2(t)$ for all $t\ge t_1$, for some $a>1$ and $t_1\ge t_0$, and that $\lim_{t\to+\infty}t^2\epsilon(t)=+\infty$ if $\alpha=3$, while $t^2\epsilon(t)\ge\frac23\alpha\left(\frac13\alpha-1+\beta c^2\right)$ for large $t$, for some $c>0$, if $\alpha>3$. Then

$$\liminf_{t\to+\infty}\|x(t)-x^*\|=0,$$

and

$$\lim_{t\to+\infty}\|x(t)-x^*\|=0$$

if there exists $T\ge t_0$ such that $\{x(t):t\ge T\}$ stays either in $B(0,\|x^*\|)$ or in its complement.

Milestones

1. Lemma A.1 (p. 29): for nonnegative continuous integrable $f$ on $(\delta,+\infty)$ and nondecreasing $\varphi\ge 0$ with $\varphi(t)\to+\infty$, $\frac1{\varphi(t)}\int_\delta^t\varphi(s)f(s)\,ds\to0$.
2. Theorem 3.1 (pp. 5–6): for $\alpha\ge3$, $g(x(t))\to\min g$ under either (a) $\int_{t_0}^{+\infty}\epsilon(t)/t\,dt<+\infty$ together with $\dot\epsilon\le-\frac{a\beta}{2}\epsilon^2$ eventually, or (b) $\epsilon(t)\le a/t$ eventually.
3. Case I of the proof of Theorem 4.4 (pp. 21–25): the trajectory eventually stays outside the open ball, and $x(t)\to x^*$.
4. Case II (pp. 25–26): the trajectory eventually stays inside the open ball, and $x(t)\to x^*$.
5. Case III (p. 26): the trajectory is inside and outside the ball for arbitrarily large times, and $\liminf\|x(t)-x^*\|=0$.

The three cases are exhaustive, so Cases I–III together give the goal.

Significance

Theorem 4.4 shows that adding Hessian driven damping does not destroy the selection property of Tikhonov regularization: the trajectory comes arbitrarily close to the minimum-norm minimizer, and converges to it in norm whenever it does not oscillate across the sphere $\|y\|=\|x^*\|$ forever. Since $\epsilon(t)\to 0$, the system still approaches $\operatorname{argmin} g$, but the limit is a canonical minimizer determined by $g$ alone, not by the initial data. In infinite dimensions this is the difference between weak and strong convergence, a distinction that matters for ill-posed problems and inverse problems, where the minimum-norm solution is the one usually sought. Remark 4.5 of the paper compares the hypotheses with those of Attouch, Chbani and Riahi for the system without Hessian damping: for $\beta=0$ the lower bound required of $t^2\epsilon(t)$ when $\alpha>3$ is, in the authors' words, "less tight" than theirs.

The result is proved in the paper; no part of it has a machine-checked proof. Formalizing it requires a Lyapunov-energy argument for a second order ODE in a Hilbert space, the weak lower semicontinuity of convex functions and of the norm, and the passage from weak to strong convergence via convergence of norms. Theorem 3.1 and Lemma A.1 are standalone results reusable for other Tikhonov-regularized inertial systems.

Difficulty

The weak convergence argument for the unregularized system (Opial's lemma) does not identify the limit, and it does not give strong convergence. Tikhonov regularization supplies the identification only through the Tikhonov curve $x_{\epsilon}$, the minimizer of $g+\frac{\epsilon}{2}\|\cdot\|^2$, and comparing $x(t)$ with $x_{\epsilon(t)}$ requires an energy whose derivative is controlled with weights tuned to $\alpha$. The Hessian term produces cross terms of the form $\beta\epsilon(t)t^2\langle\nabla g(x(t)),x(t)\rangle$ that are absent from the system without Hessian damping; the integral hypothesis on $\epsilon^2(s)s^{\alpha/3+1}$ and the slow-decay condition $\dot\epsilon\le-\frac{a\beta}{2}\epsilon^2$ exist to absorb them. A direct energy estimate only works when $\|x(t)\|\ge\|x^*\|$; inside the ball a different argument is required, and when the trajectory crosses the sphere infinitely often neither argument yields convergence of the whole trajectory, only a liminf statement.

Formalization scope

Conventions committed to in Lean:

• Curves are maps $\mathbb R\to\mathcal H$; only their values on $[t_0,+\infty)$ matter. Derivatives of $x$, $\dot x$ and $\epsilon$ are taken within $[t_0,+\infty)$ (one-sided at $t_0$) and passed as explicit maps xd, xdd, ε'; $\ddot x$ and $\dot\epsilon$ are continuous there.
• $\nabla g$ is gradient g; $\nabla^2g(x)v$ is the Fréchet derivative of gradient g at $x$ applied to $v$. "Lipschitz on bounded sets" means Lipschitz on every closed ball centred at $0$.
• $\min g$ is the infimum of the range of $g$, attained because $\operatorname{argmin} g\neq\emptyset$.
• $\int_{t_0}^{+\infty}\epsilon(t)/t\,dt<+\infty$ is Lebesgue integrability of $\epsilon(t)/t$ on $[t_0,+\infty)$, never a comparison of a Bochner integral with a number. $t^{\alpha/3+1}$ is the real power.
• $\liminf_{t\to+\infty}\|x(t)-x^*\|=0$ is written as: for every $\delta>0$, $\|x(t)-x^*\|<\delta$ for arbitrarily large $t$. Lean's Filter.liminf is not used, since it returns $0$ for a function tending to $+\infty$.
• The alternative "in the ball or in its complement" uses one $T$ for both branches, with the disjunction outside the universal quantifier. Placing the disjunction inside ($\forall t\ge T$, $\|x(t)\|<\|x^*\|$ or $\|x(t)\|\ge\|x^*\|$) would make the hypothesis always true and the strong convergence claim unconditional, which the paper does not prove.
• Every statement is made for every global $C^2$-solution of (5). Existence and uniqueness of that solution (Theorem 2.1 of the paper) is a separate result, formalized in the companion mission on weak convergence; the hypothesis is not vacuous.
• No positivity of $\epsilon$ is assumed: it follows from the conditions for $\alpha=3$ and $\alpha>3$.
• Cases I–III carry the full hypothesis list of Theorem 4.4, although Case II uses only part of it.

No statement of the mission has been repaired against the printed text.

A complete development needs: weak lower semicontinuity of convex continuous functions and of the norm on Hilbert spaces; weak sequential compactness of bounded sets; existence of the minimum-norm element of a closed convex set (Mathlib's projection onto closed convex sets); the strongly convex Tikhonov curve and its convergence to $x^*$; and calculus for energy functionals along $C^2$ curves on half-lines. Lemma A.1 and the Tikhonov-curve facts are reusable for every Tikhonov-regularized dynamics. Contributions of proofs of individual milestones, of supporting lemmas, and of alternative arguments are welcome.

Selected references

• R.I. Boţ, E.R. Csetnek, S.C. László, Tikhonov regularization of a second order dynamical system with Hessian driven damping, arXiv:1911.12845v2, 2020; Mathematical Programming 189, 151–186, 2021. https://arxiv.org/abs/1911.12845v2, https://doi.org/10.1007/s10107-020-01528-8
• H. Attouch, Z. Chbani, H. Riahi, Combining fast inertial dynamics for convex optimization with Tikhonov regularization, Journal of Mathematical Analysis and Applications 457, 1065–1094, 2018. https://doi.org/10.1016/j.jmaa.2016.12.017
• H. Attouch, J. Peypouquet, P. Redont, Fast convex optimization via inertial dynamics with Hessian driven damping, Journal of Differential Equations 261(10), 5734–5783, 2016. https://doi.org/10.1016/j.jde.2016.08.020
• H. Attouch, Z. Chbani, J. Peypouquet, P. Redont, Fast convergence of inertial dynamics and algorithms with asymptotic vanishing viscosity, Mathematical Programming 168, 123–175, 2018. https://doi.org/10.1007/s10107-016-0992-8
• W. Su, S. Boyd, E.J. Candès, A differential equation for modeling Nesterov's accelerated gradient method: theory and insights, Journal of Machine Learning Research 17(153), 1–43, 2016. https://jmlr.org/papers/v17/15-084.html

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