All missions

Motivation

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

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

Setting

Observations follow the model

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

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

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

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

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

Formalization targets

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

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

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

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

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

Milestones

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

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

Significance

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

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

Difficulty

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

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

Formalization scope

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

Selected references

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

Certify $\alpha\ge2.006470828$ by specializing OpenAI's general seed theorem to $d=20$ and $M=9^{21}$.

The construction gives

$$s(f)\le A=44M^{21},\qquad bs(f,0)\ge B=M^2(2M^2+1)^{20}.$$

Here $bs(f,0)$ is block sensitivity at the all-zero input. The ratio $\log B/\log A$ is approximately $2.006470828227379\ldots$. Prove the exact inequality $A^{2.006470828}\le B$, then reuse the foundation's finite-certificate theorem.

The goal uses the campaign's shared definitions and requires arbitrarily large sensitivity. This is a stronger specialization of the existing construction, not a claim of a new construction or global parameter optimality.

Motivation

The price of anarchy (PoA) of a nonatomic congestion game is the ratio of the total cost of a Wardrop equilibrium to the minimum possible total cost. It quantifies how much selfish routing loses compared with central coordination, and it has been studied intensively since Koutsoupias and Papadimitriou (1999) and Roughgarden and Tardos (2002), mostly through worst-case bounds over classes of cost functions.

Worst-case bounds say nothing about how the PoA of one particular network behaves when its data change. In transport applications both the cost functions (capacities, tolls, travel-time models) and the demands are estimated, so the PoA is only useful if small errors in the data cause small errors in the PoA. Wu and Möhring (arXiv:2007.13979, published in Mathematics of Operations Research, 2023) study this sensitivity question in a setting where cost functions and demands change simultaneously. Earlier sensitivity results changed only the demands, with the cost functions fixed: Englert, Franke and Olbrich (2010) bounded the growth of the PoA of a single-O/D network with polynomial costs of degree at most $\beta$ by a factor $(1+\epsilon)^\beta$ when the demand grows by a factor $1+\epsilon$; Takalloo and Kwon (2020) extended this to several O/D pairs whose demands are scaled together; and Cominetti, Dose and Scarsini (arXiv:1907.10101) studied differentiability of the PoA as a function of the demand of a single O/D pair. The main theorem of the paper, Theorem 9, is the subject of this mission.

Setting

A network consists of a finite set $A$ of arcs, a finite non-empty set $\mathcal K$ of origin–destination (O/D) pairs, and for every $k \in \mathcal K$ a non-empty set $\mathcal S_k$ of paths; each path is a non-empty set of arcs. From §3.1 onward the paper also assumes every arc lies on some path and every $\mathcal S_k$ has at least two paths (Condition 1).

A game $\Gamma = (\tau, d)$ on the network consists of cost functions $\tau_a : [0,\infty) \to [0,\infty)$, one per arc, that are continuous and non-decreasing, and demands $d_k \ge 0$, one per O/D pair. The total demand is $T(d) = \sum_k d_k$. The game space $\mathcal G(G,\mathcal K,\mathcal S)$ consists of the games with $T(d) > 0$ and $\tau_a(x) > 0$ for all $x \in (0, T(d)]$.

A flow $f = (f_s)$ assigns a non-negative amount to every path, with $\sum_{s\in\mathcal S_k} f_s = d_k$. Its arc flows are $f_a = \sum_{s \ni a} f_s$, its path costs $\tau_s(f) = \sum_{a\in s}\tau_a(f_a)$, and its total cost

$$C(\Gamma, f) = \sum_{a\in A} f_a\,\tau_a(f_a).$$

A Wardrop equilibrium (WE) is a flow in which every used path of a pair is a cheapest path of that pair. The SO cost $\mathcal C^*(\Gamma)$ is the minimum total cost over all flows, the WE cost $\tilde{\mathcal C}(\Gamma)$ is the total cost of a WE flow (all WE flows have the same cost), and

$$\rho(\Gamma) = \frac{\tilde{\mathcal C}(\Gamma)}{\mathcal C^*(\Gamma)}.$$

Games are compared by the distance

$$\|\Gamma - \Gamma'\| = \max\Big\{\|d-d'\|_\infty,\ \max_{a\in A}\max_{x\in[0,\min\{T(d),T(d')\}]}|\tau_a(x) - \sigma_a(x)|,\ \|\tau(T(d)) - \sigma(T(d'))\|_\infty\Big\}$$

for $\Gamma = (\tau, d)$ and $\Gamma' = (\sigma, d')$. It compares cost functions only on the range of flow values both games can produce, plus the values at the respective total demands. A function $h$ is Lipschitz continuous on $[0,T]$ with constant $M$ if $|h(x) - h(y)| \le M|x-y|$ for all $x, y \in [0,T]$.

Formalization targets

Goal: Theorem 9 (p. 26)

Let $\Gamma = (\tau, d)$ be a game of the game space whose cost functions are Lipschitz continuous on $[0, T(d)]$. Then there are $\epsilon_\Gamma > 0$ and $\kappa_\Gamma > 0$, depending only on $\Gamma$, such that

$$|\rho(\Gamma) - \rho(\Gamma')| \le \kappa_\Gamma\,\|\Gamma - \Gamma'\|^{1/2}\quad\text{for every game } \Gamma' \text{ of the game space with } \|\Gamma - \Gamma'\| < \epsilon_\Gamma.$$

The goal fixes the exponent $1/2$ and leaves the radius and the constant existential, which is the form the paper claims.

Milestones

1. Lemma 1a)–c) (p. 13): properties of $\epsilon$-approximate WE flows, ending with

$$|C(\Gamma, f) - C(\Gamma, \tilde f)| \le |A|\sqrt{M\epsilon}\,T(d) + \epsilon$$

for an $\epsilon$-approximate WE flow $f$ and a WE flow $\tilde f$ when all costs are $M$-Lipschitz on $[0,T(d)]$. 2. Lemma 10a)–d) (p. 27): on a demand slice (games with a common demand vector $w$), $\mathcal C^*$ is Lipschitz, WE flows of one game are $|A|\,T(w)\,\|\Gamma_1-\Gamma_2\|$-approximate WE flows of the other, and $\tilde{\mathcal C}$ and $\rho$ are Hölder with exponent $1/2$ with explicit constants. 3. Lemma 11a)–c) (p. 31): on a cost slice (games with a common cost vector and $T(w') \le T(w)$), explicit Hölder bounds of exponent $1/2$ for $\tilde{\mathcal C}$ and $\rho$ and a Lipschitz bound for $\mathcal C^*$.

Significance

Theorem 9 is the first pointwise Hölder continuity result for the PoA on the whole game space, with demands and costs perturbed together. Its hypothesis is mild (Lipschitz costs on a compact interval, which covers polynomial, BPR-type and piecewise linear costs), and such games are dense in the game space. Together with Theorem 8 of the same paper, which shows that no uniform Hölder bound exists, it describes exactly what kind of stability the PoA has: local, with a constant depending on the game, and exponent $1/2$ in general. The explicit constants of Lemmas 10 and 11 give computable error bounds for the PoA of a network whose data are known only approximately.

The result is proved in the paper; no machine-checked proof exists. This mission formalizes the statement and the explicit slice estimates the proof rests on. Lemma 1 is a self-contained statement about approximate Wardrop equilibria that is useful well beyond this paper, for instance for analysing iterative traffic-assignment algorithms, which only ever produce approximate equilibria.

Difficulty

The obvious approach compares an equilibrium of $\Gamma$ with an equilibrium of $\Gamma'$ directly. This fails because the two games have different demand vectors, so their flows live in different polytopes: an equilibrium of one game is not even a flow of the other. The paper separates the perturbation into a change of costs at fixed demand and a change of demand at fixed costs, through an auxiliary game, and each half needs its own argument. On a demand slice an equilibrium of one game is only an approximate equilibrium of the other, and the passage from an approximate equilibrium to its cost loses a square root (Lemma 1c), which is tight by Example 2). On a cost slice the demand has to be removed path by path from an equilibrium while keeping it an equilibrium of a shifted game. Finally, the constants of the slice estimates depend on the auxiliary game, and they must be controlled uniformly near $\Gamma$.

Formalization scope

The Lean development fixes the following conventions.

• The network is a structure with $|A|$ arcs, $|\mathcal S|$ paths and $|\mathcal K|$ O/D pairs, a 0/1 arc–path incidence matrix and the map sending a path to its pair. Lemma 1 uses the §2 model assumptions: 0/1 incidence, non-empty paths, $\mathcal K \neq \emptyset$, and $|\mathcal S_k| \ge 1$. The later results add Condition 1 (every arc on a path, $|\mathcal S_k| \ge 2$), as assumed from §3.1. Paths are arbitrary non-empty 0/1 columns, not necessarily loop-free paths of a digraph; the results do not use loop-freeness.
• Cost functions are maps $\mathbb R \to \mathbb R$ required to be continuous, non-decreasing and non-negative on $[0,\infty)$ only.
• Arc flows, Wardrop equilibria (2.1) and the potential (2.6) come from the published definition KellyStochasticNetworks_Wardrop. $\epsilon$-approximate WE flows follow (2.7) in arc form. The total cost uses the arc form, which equals the path form for 0/1 incidence.
• $\mathcal C^*$ is the infimum of costs over flows, $\tilde{\mathcal C}$ the supremum of costs over WE flows, $\rho$ their quotient. The middle term of the distance is the supremum of the image of the compact set $A\times[0,\min\{T(d),T(d')\}]$, and $\|\cdot\|_\infty$ is the sup norm.
• Every statement about $\rho$, $\mathcal C^*$ or $\tilde{\mathcal C}$ quantifies over games of the game space, where $\rho$ is a genuine ratio of positive numbers. Off the game space Lean's division by zero would give $\rho = 0$, so quantifying over all pairs $(\tau, d)$ would trivialize the statements; this is ruled out. In the goal, $\epsilon_\Gamma$ and $\kappa_\Gamma$ are chosen before $\Gamma'$.
• Several printed strict inequalities are posed as non-strict, because they fail at $\Gamma' = \Gamma$ or are attained in the paper's own Example 2. In Lemma 11 the printed constants are corrected by a factor $|\mathcal K|$ that the paper's own argument needs; each item's Formalization Note quotes the printed form.

A complete development needs: existence of Wardrop equilibria and uniqueness of their cost on the game space, existence of social optima, the integral inequality (2.9) for monotone costs, positivity of $\mathcal C^*$ on the game space, and the path-by-path demand-reduction construction of Lemma 11. The existence and uniqueness results and Lemma 1 are reusable in any formalization of selfish routing. Proofs of any milestone are welcome, as are the supporting lemmas above.

The source is the arXiv preprint arXiv:2007.13979v3 (23 Aug 2021); all page and theorem numbers refer to it, not to the published version.

Selected references

• Z. Wu, R. H. Möhring, A sensitivity analysis of the price of anarchy in non-atomic congestion games, arXiv:2007.13979v3, 2021; Mathematics of Operations Research 48(3), 2023. https://arxiv.org/abs/2007.13979, https://doi.org/10.1287/moor.2022.1292
• T. Roughgarden, É. Tardos, How bad is selfish routing?, Journal of the ACM 49(2), 2002. https://doi.org/10.1145/506147.506153
• E. Koutsoupias, C. Papadimitriou, Worst-case equilibria, STACS 1999. https://doi.org/10.1007/3-540-49116-3_38
• J. G. Wardrop, Some theoretical aspects of road traffic research, Proceedings of the Institution of Civil Engineers 1(3), 1952. https://doi.org/10.1680/ipeds.1952.11259
• M. Englert, T. Franke, L. Olbrich, Sensitivity of Wardrop equilibria, Theory of Computing Systems 47(1):3–14, 2010.
• M. Takalloo, C. Kwon, Sensitivity of Wardrop equilibria: revisited, Optimization Letters 14(3):781–796, 2020.
• R. Cominetti, V. Dose, M. Scarsini, The price of anarchy in routing games as a function of the demand, 2020. https://arxiv.org/abs/1907.10101

Why accelerate value computation

Value iteration and its policy-evaluation special case, value computation, are the basic algorithms of dynamic programming for Markov decision processes (MDPs). Both are fixed-point iterations of a $\lambda$-contraction, so they converge at the geometric rate $\lambda$, the discount factor. When $\lambda$ is close to $1$, which is the regime of long effective horizons in reinforcement learning ($\lambda = 0.99$ or $0.999$) and in healthcare and operations applications, the number of iterations grows like $1/(1-\lambda)$.

Goyal and Grand-Clément (arXiv:1905.09963, Operations Research 2023) observe that $v \mapsto v - T(v)$ behaves like the gradient of a function with smoothness constant $1+\lambda$ and strong-convexity constant $1-\lambda$. This suggests importing the accelerated schemes of convex optimization: Nesterov's acceleration and Polyak's momentum (heavy-ball) method (Polyak 1964; Ghadimi, Feyzmahdavian, Johansson 2015). For the affine operator $T_\pi$ of a fixed policy, they prove that both schemes converge at a rate governed by $\sqrt{\kappa}$ rather than $\kappa$, with $\kappa = (1+\lambda)/(1-\lambda)$, provided the Markov chain of the policy is irreducible and reversible. This mission poses the momentum result, Theorem 5.5.

Setting

A finite MDP has a state set $S$ with $|S| = n$, a finite action set $A$, transition probabilities $P_{iaj}$ (from state $i$ to state $j$ under action $a$; each $P_{ia}$ is a probability vector), rewards $r_{ia} \in \mathbb{R}$, and a discount factor $\lambda \in (0,1)$. A policy $\pi = (\pi_{ia})$ is a matrix with nonnegative rows summing to $1$; it induces

$$r_{\pi,i} = \sum_a \pi_{ia} r_{ia}, \qquad L_{\pi,ij} = \sum_a \pi_{ia} P_{iaj}, \qquad T_\pi(v) = r_\pi + \lambda L_\pi v .$$

The value function of $\pi$ is $v^\pi = \sum_{t \ge 0} \lambda^t L_\pi^t r_\pi$, the expected discounted reward from each starting state; it is the unique fixed point of $T_\pi$.

Reversibility (Definition 2.1): the chain with transition matrix $L$ is irreducible, and it has a stationary probability distribution $\nu$ with $\nu_i L_{ij} = \nu_j L_{ji}$ for all $i,j$.

Momentum Value Computation (M-VC) starts from arbitrary $v_0, v_1 \in \mathbb{R}^n$ and iterates

$$v_{s+1} = v_s - \alpha\,(v_s - T_\pi(v_s)) + \beta\,(v_s - v_{s-1}), \qquad s \ge 1,$$

with the constant step sizes (4.2)

$$\alpha = \frac{2}{1+\sqrt{1-\lambda^2}}, \qquad \beta = \frac{1-\sqrt{1-\lambda^2}}{1+\sqrt{1-\lambda^2}} .$$

The analysis runs through the $2n \times 2n$ matrix

$$B_\pi = \begin{pmatrix} \lambda(\beta+1)L_\pi & -\beta I \\ I & 0 \end{pmatrix},$$

which propagates the error of the pair $x_s = (v_s, v_{s-1})$, and its spectral radius $\rho(B_\pi)$, the largest modulus of a complex eigenvalue.

Formalization targets

Goal: Theorem 5.5

For a valid MDP and a policy $\pi$ whose chain $L_\pi$ is irreducible and reversible, the M-VC iterates with step sizes (4.2) converge to $v^\pi$, and for every $\eta > 0$

$$v_s = v^\pi + o\!\left(\left(\frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}} + \eta\right)^{s}\right), \qquad 0 < \frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}} < \lambda .$$

The goal states the paper's three clauses as printed: convergence, the little-o rate for every $\eta > 0$, and the comparison with $\lambda$.

Milestones

1. The step-size identity $\alpha = 1 + \beta$ (proof of Lemma B.1).
2. Lemma B.1: $x_s = x^\pi + B_\pi^{s-1}(x_1 - x^\pi)$ for all $s \ge 1$, with $x^\pi = (v^\pi, v^\pi)$.
3. The eigenvalues of an irreducible, reversible transition matrix are real (§2).
4. (B.1): every eigenvalue $\omega$ of $B_\pi$ satisfies $\omega^2 - \frac{2\lambda\mu}{1+\sqrt{1-\lambda^2}}\omega + \frac{1-\sqrt{1-\lambda^2}}{1+\sqrt{1-\lambda^2}} = 0$ for an eigenvalue $\mu$ of $L_\pi$.
5. For $\mu \in [-1,1]$, the roots $\omega^\pm(\mu)$ of (B.1) have modulus $\lambda/(1+\sqrt{1-\lambda^2})$.
6. The identity $\frac{\lambda}{1+\sqrt{1-\lambda^2}} = \frac{\sqrt{1+\lambda}-\sqrt{1-\lambda}}{\sqrt{1+\lambda}+\sqrt{1-\lambda}} = \frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}}$.
7. Lemma B.2: for a reversible chain, $\rho(B_\pi) = \frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}}$.
8. $0 < \frac{1-\sqrt{1/\kappa}}{1+\sqrt{1/\kappa}} < \lambda$ for $\lambda \in (0,1)$.

Significance

The rate $(1-\sqrt{1/\kappa})/(1+\sqrt{1/\kappa})$ is the optimal rate of the heavy-ball method on strongly convex quadratics with condition number $\kappa$. Theorem 5.5 shows that policy evaluation for reversible chains enjoys the same improvement over $\lambda$, so that an $\epsilon$-approximation of $v^\pi$ needs a number of iterations scaling like $1/\sqrt{1-\lambda}$ rather than $1/(1-\lambda)$. The paper also shows that the reversibility assumption cannot simply be dropped: on a cyclic chain both accelerated schemes may diverge. Lemma B.2 is an exact spectral computation for a structured block matrix that reappears in any heavy-ball analysis driven by a matrix with real spectrum in $[-1,1]$.

The paper is a sibling series of four missions. This one poses Theorem 5.5; the others pose Theorem 5.1 (Accelerated Value Computation), Theorem 6.3 (a lower bound for first-order methods on a chain MDP) and Theorem 7.1 (Safe Accelerated Value Iteration). The results are proved on paper; none of them has a machine-checked proof. The work here is to formalize the known argument: the linear-recursion representation, the spectrum of $B_\pi$, and the passage from spectral radius to a little-o rate.

Difficulty

The obvious argument bounds $\|B_\pi\|$ in some norm and iterates. No such bound by the rate holds in general: $B_\pi$ is not normal, and for eigenvalues $\mu = \pm 1$ of $L_\pi$ the two roots of (B.1) coincide, producing Jordan blocks. The rate must come from the spectral radius, and the gap between $\rho(B_\pi)$ and $\|B_\pi^s\|^{1/s}$ is exactly what the $+\eta$ absorbs. Computing $\rho(B_\pi)$ needs two separate facts: the eigenvalues of $B_\pi$ are tied to those of $L_\pi$ through the quadratic (B.1), which needs a determinant identity for block matrices with commuting blocks; and the eigenvalues of $L_\pi$ are real and lie in $[-1,1]$, which needs reversibility together with irreducibility, used to make the stationary distribution positive. For non-real $\mu$ the modulus computation fails, which is why the hypothesis cannot be dropped.

Formalization scope

States and actions are finite types. The MDP data $(P, r, \lambda)$ is a plain structure, with validity (stochastic $P_{ia}$, $0 < \lambda < 1$) a separate hypothesis; the paper's initial distribution $p_0$ plays no role and is omitted. The value function is the Neumann series $\sum_t \lambda^t L_\pi^t r_\pi$. The norm on $\mathbb{R}^n$ is the sup norm, and $o(\cdot)$ is with respect to it as $s \to \infty$. Spectra and spectral radii are those of the complexified matrices, so that the non-real eigenvalues of $B_\pi$ are seen. Reversibility uses the published mm_basic notions: irreducibility, a stationary probability distribution, and detailed balance with respect to it; detailed balance alone would be trivially satisfied by $\nu = 0$ and is not used.

Three printed slips are corrected, and each milestone keeps the printed text verbatim. Lemma B.1 is printed with $x_0 - x^\pi$, but $x_0 = (v_0, v_{-1})$ is undefined; the statement uses $x_1 = (v_1, v_0)$. Lemma B.2 prints $\rho(B_\pi) = (1-\sqrt\kappa)/(1+\sqrt\kappa)$, a negative number; its proof computes $(1-\sqrt{1/\kappa})/(1+\sqrt{1/\kappa})$, the rate of Theorem 5.5, which is stated. On p. 22 the constant $\lambda/(1+\sqrt{1-\lambda^2})$ is printed as $\lambda/(1+\sqrt{1-\lambda})^2$. The second step size, printed $\gamma$ in (4.2), is the $\beta$ of (M-VC) and App. B.

A statement that holds only vacuously, for example one in which reversibility is replaced by detailed balance with an arbitrary vector or in which $\lambda$ is unconstrained, is ruled out by the hypotheses above. Lemma B.2 is an equality and must not be weakened to an upper bound.

A complete development needs the determinant of a $2\times 2$ block matrix with commuting blocks, the reality of the spectrum of a reversible chain (implied by the published MarkovMixing.spectral_representation once the stationary distribution is shown positive), Gelfand's formula for matrices, and the convergence of the Neumann series. The spectral facts about reversible chains and the block-matrix spectrum are reusable beyond this mission. Proofs of any milestone are welcome independently.

Selected references

• V. Goyal and J. Grand-Clément, A First-Order Approach to Accelerated Value Iteration, Operations Research, 2023; arXiv:1905.09963v7 (2021). https://arxiv.org/abs/1905.09963
• B. T. Polyak, Some methods of speeding up the convergence of iteration methods, USSR Computational Mathematics and Mathematical Physics 4(5), 1964. https://doi.org/10.1016/0041-5553(64)90137-5
• E. Ghadimi, H. R. Feyzmahdavian, M. Johansson, Global convergence of the Heavy-ball method for convex optimization, European Control Conference, 2015. https://arxiv.org/abs/1412.7457
• P. Brémaud, Markov Chains: Gibbs Fields, Monte Carlo Simulation, and Queues, Springer, 2nd ed. 2020 (cited in the paper as 2013), Chapter 6. https://doi.org/10.1007/978-3-030-45982-6
• M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 2014. https://doi.org/10.1002/9780470316887

Motivation

Quantum communication and computation often require a receiver to infer which preparation was sent after it has passed through a noisy quantum process. When possible preparations are mixed states, their overlap makes exact identification impossible. A measurement is then judged by its average probability of a correct label. The pretty good measurement gives a concrete measurement from the ensemble itself, without first solving the optimization over all measurements. Barnum and Knill related it to a general reversal operation for noisy dynamics and bounded its error through pairwise state fidelities in their preprint, §V–VI. The bound is useful when the overlaps are easier to estimate than the measurement's success probability.

The present mission addresses the preprint's second main result. The source is arXiv:quant-ph/0004088v2, not the later journal pagination. The preprint also strengthens its Theorem 3 relative to the published text, as its acknowledgment explains; this mission concerns Theorem 5 and the calculation around it.

Setting

An ensemble is a finite family of output density matrices $\hat\rho_j$ with probabilities $p_j\geq0$ satisfying $\sum_jp_j=1$. A density matrix is a positive semidefinite complex matrix with trace one. For each label $j$, fix an orthonormal eigenbasis $v_{ij}$ and nonnegative eigenvalues $\lambda_{ij}$ such that

$$\hat\rho_j=\sum_i\lambda_{ij}|v_{ij}\rangle\langle v_{ij}|, \qquad \sum_i\lambda_{ij}=1.$$

The eigenpair index $i$ runs over a finite output basis $O$; zero eigenvalues are allowed. The input labels form a finite basis $J$. A label distribution is represented by $\rho=\sum_jp_j|j\rangle\langle j|$.

The paper's classicizing channel $A$ has Kraus operators $A_{ij}=\sqrt{\lambda_{ij}}|v_{ij}\rangle\langle j|$. Acting on an input matrix $X$, its value is $A(X)=\sum_{i,j}A_{ij}X A_{ij}^{\dagger}$. In particular, its output on $\rho$ is $\rho_{\mathrm{out}}=\sum_jp_j\hat\rho_j$. The paper assumes $\rho_{\mathrm{out}}$ has full support when it writes its reversal operation. For a general Kraus family $A_a$, that operation has operators

$$(R_{A,\rho})_a=\rho^{1/2}A_a^\dagger A(\rho)^{-1/2}.$$

The inverse square root is spectral: invert nonzero eigenvalues and leave zero eigenvalues at zero. With full support, it is the usual inverse square root.

For an input label $j$, classical fidelity is the chance that the composite operation returns the same label. Averaging gives

$$F_{\mathrm{cl}}(\rho,K)= \sum_jp_j\langle j|K(|j\rangle\langle j|)|j\rangle.$$

The Bures–Uhlmann fidelity used here is the unsquared quantity $F_{\mathrm{BU}}(\sigma,\tau)=\operatorname{tr}\sqrt{\sqrt\sigma\,\tau\,\sqrt\sigma}$. For the classicizing channel, the reversal operation realizes the pretty good measurement, as shown by equation (36) and the discussion after equation (37) in the preprint, p. 10.

Formalization targets

Recovery error

The goal, in the reading established by the paper's proof, is

$$F_{\mathrm{cl}}(\rho,R_{A,\rho}A) \geq 1-\sum_{\substack{i,j\in J\\i\ne j}} \sqrt{p_ip_j}\,F_{\mathrm{BU}}(\hat\rho_i,\hat\rho_j).$$

The sum is over ordered pairs; each unordered pair of distinct labels is counted twice. The coefficient is exactly one. The goal applies to every finite ensemble with the spectral data above and a full-support output. It does not fix the number of labels or the dimension of the output.

The milestones are the reversal formula (36), the classical-fidelity identities in (38), the unit squared Frobenius norm (40), the diagonal-block expression (41), the off-diagonal trace-norm identity following (42), and the two-block estimate of Lemma 6. They record the paper's mathematical statements and keep the attack path tied to the authors' displayed results.

Significance

The result bounds a measurement's probability of error using only pairwise similarities of the possible output states and their prior probabilities. For nearly distinguishable states, the weighted fidelity sum is small, so this particular measurement succeeds with high probability. The theorem therefore gives a usable guarantee for a specified recovery procedure, rather than only asserting that some procedure exists. In the preprint, §VII, Barnum and Knill describe quantum-information applications of such recovery bounds.

The mathematical result is already proved in the paper, subject to the correction explained below. The formalization work is to make the mixed-state channel, its recovery, the finite-dimensional spectral conventions, and the block-matrix norm estimate precise in Lean. The published Prove2Me definitions for Kraus updates and trace norm supply reusable starting points. A complete proof of this mission would add a checked mixed-state pretty-good-measurement bound; the local statements here compile as open theorems, and no proof is claimed.

Difficulty

The obvious pairwise-overlap estimate does not by itself express the error of the recovery channel. The recovery's classical fidelity is initially a channel evaluation on basis states, while the bound uses trace norms of blocks of a Gram matrix. The key obstacle is controlling the off-diagonal Frobenius mass of the positive square root of that Gram matrix by the trace norms of the corresponding blocks of the Gram matrix itself. Lemma 6 states the needed two-block comparison, including rectangular blocks. The matrix dimension and block labels must remain consistent when it is applied across a larger array.

Formalization scope

All systems and index sets are finite, with matrices over $\mathbb C$ and real probabilities. A general completely positive map is represented by an unbundled finite family of Kraus matrices. The classicizing family has rectangular matrices from the input-label space to the output space; the reversal has matrices in the opposite direction. Composite Kraus families are indexed by pairs. The classical fidelity is defined from the channel action in equation (10); the goal does not define it using the desired overlap bound. The reversal is defined by equation (12) for a general family, so its specialized formula remains a theorem.

The spectral hypotheses include nonnegative probabilities and eigenvalues, unit sums, and orthonormal eigenvectors. Full support of $\rho_{\mathrm{out}}$ is an explicit hypothesis wherever the reversal appears, following page 7. Empty input or output types cannot satisfy the normalized data together with these hypotheses. The Bures–Uhlmann expression is the unsquared trace of a positive square root; using the squared fidelity would change the constant and is outside this mission. Lemma 6 is independent of the ensemble and can be reused for finite block-matrix estimates. Contributions to the spectral identities, the array equalities, and the block-norm argument are welcome.

Equation (39) prints the square of the optimal success probability on its left. The first line of (38) compares that quantity with the recovery fidelity in the opposite direction to Corollary 4. The proof on pages 12–13 concludes the displayed bound for $F_{\mathrm{cl}}(\rho,R_{A,\rho}A)$. This mission states that proved conclusion and records the printed discrepancy in its item and audit notes.

Selected references

• Howard Barnum and Emanuel Knill, Reversing quantum dynamics with near-optimal quantum and classical fidelity, arXiv:quant-ph/0004088v2, 2000/2026 version. arXiv
• Howard Barnum and Emanuel Knill, Reversing quantum dynamics with near-optimal quantum and classical fidelity, Journal of Mathematical Physics 43 (2002), 2097–2106. DOI

Payment channels and blockchain congestion

A blockchain such as Bitcoin settles a limited number of transactions per unit of time, and every on-chain transaction pays a fee that rises with congestion. The Lightning Network moves payments off the chain. Two parties lock funds in a payment channel with one on-chain transaction, and they can then pay each other any number of times by updating the channel balance privately. A new on-chain transaction is needed only when one side of the channel runs out of funds and the channel must be reset.

Guasoni, Huberman and Shikhelman (Management Science, 2023) model a channel between two nodes that pay each other at Poisson rates. They compute its cost and its optimal size, and in §3.3 they quantify how much a channel relieves the chain. The relief is the long-run number of channel transactions carried per on-chain transaction (Proposition 2). A related quantity is the probability that the payee side of the channel, not the payer side, is exhausted first (Proposition 1). This mission formalizes both results, which are statements about two finite random walks.

Setting

Node 1 commits $l_1\ge1$ units to the channel and node 2 commits $l_2\ge1$ units. Node 1 pays node 2 one unit at the jumps of a Poisson process with rate $\lambda_1$, and node 2 pays node 1 at rate $\lambda_2$, independently. Write $q=\lambda_2/\lambda_1$. The balance $X$ starts at $0$. It moves up by one when node 2 pays and down by one when node 1 pays. Node 2 has exhausted its side when $X=l_2$, and node 1 when $X=-l_1$.

Only the sequence of payments matters here, not their timing or discounting. Observed at its jumps, the balance is a random walk that steps up with probability $p=\lambda_2/(\lambda_1+\lambda_2)$ and down with probability $1-p=\lambda_1/(\lambda_1+\lambda_2)$. Two versions of this walk appear.

1. The absorbed walk on $\{-l_1,\dots,l_2\}$ stops at $-l_1$ and at $l_2$. Write $\mathbb P_0\{\tau_{l_2}<\tau_{-l_1}\}$ for the probability that, from the balance $0$, it reaches $l_2$ before $-l_1$.
2. The reset walk returns the balance to $0$ as soon as it reaches $l_2$ or $-l_1$, which models an on-chain reset of the channel. It lives on the interior balances $\{-l_1+1,\dots,l_2-1\}$. For a stationary distribution $m$ of this walk, $m(n)$ is the long-run fraction of transactions the balance spends at $n$, with $m(l_2)=m(-l_1)=0$.

The transactions that trigger an on-chain reset are the up-moves from $l_2-1$ and the down-moves from $-l_1+1$. Their stationary fraction is

$$f(m)=m(l_2-1)\,\frac{\lambda_2}{\lambda_1+\lambda_2}+m(-l_1+1)\,\frac{\lambda_1}{\lambda_1+\lambda_2},$$

and the long-term ratio of channel to on-chain transactions is $1/f(m)$.

Formalization targets

Goal: Proposition 2 (Congestion Reduction)

For $\lambda_1,\lambda_2>0$ with $\lambda_1\neq\lambda_2$ and $l_1,l_2\ge1$, the reset walk has a stationary distribution, and every stationary distribution $m$ satisfies

$$\frac1{f(m)}=\frac{(q+1)\Bigl(\bigl(l_2(q^{l_1}-1)-l_1\bigr)q^{l_2}+l_1\Bigr)}{(q-1)(q^{l_1+l_2}-1)}.$$

Milestones

• (28) and (29): $m(n)=m(0)\,\dfrac{q^{l_2}-q^n}{q^{l_2}-1}$ for $0\le n\le l_2$, and $m(n)=m(0)\,\dfrac{q^{l_1+n}-1}{q^{l_1}-1}$ for $-l_1\le n\le0$.
• (30): $m(0)=\dfrac{(q^{l_1}-1)(q^{l_2}-1)}{\bigl(l_2(q^{l_1}-1)-l_1\bigr)q^{l_2}+l_1}$.
• The on-chain fraction $f(m)$ is the reciprocal of the goal's closed form.
• Proposition 2 (i)–(ii): the closed form tends to $l_1$ as $q\downarrow0$ and to $l_1l_2$ as $q\to1$.
• Proposition 1 (i)(a),(c): $\mathbb P_0\{\tau_{l_2}<\tau_{-l_1}\}=\dfrac{1-q^{-l_1}}{1-q^{-l_1-l_2}}$ if $\lambda_2>\lambda_1>0$, and $=1$ if $\lambda_2>\lambda_1=0$.
• Proposition 1 (i)(b), corrected: for $\lambda_1=\lambda_2>0$ the probability is $l_1/(l_1+l_2)$, which is the published gambler's ruin theorem.

Significance

Proposition 2 measures how much a channel relieves the chain. A unidirectional channel of size $l_1$ carries $l_1$ payments per on-chain transaction. A symmetric bidirectional channel carries $l_1l_2$, which grows with the product of the two sizes rather than their sum. For a fixed total commitment, the relief is therefore largest when the flows are balanced. This is the paper's quantitative case that bidirectional channels reduce congestion far more than one-way ones. The probabilities of Proposition 1 tell each node how likely it is to be the one whose funds run out.

Both results are proved in the paper by elementary difference-equation arguments. Neither has a machine-checked proof. Formalizing them gives a verified closed form for the stationary law of a biased walk with resets at both ends. It also gives a biased gambler's-ruin probability on top of the platform's Markov chain library, which so far has only the fair case. The formalization also corrects case (b) of Proposition 1, which as printed claims $1/2$ for every $l_1,l_2$; the paper's own proof gives $l_1/(l_1+l_2)$.

Difficulty

The reset walk is not a birth–death chain: the balance $0$ receives the reset flow from both ends, so the walk is in general not reversible, and the detailed-balance shortcut that gives the stationary law of a reflected walk in one line fails. The balance equation (27) holds only away from $0$ and from the two reset points. In Lean, the abstract equation $mP=m$ on Fin (l₁ + l₂ - 1) must be related to recurrences indexed by integer balances, and the edge cases $l_1=1$ and $l_2=1$, where the bottom or top balance is $0$ itself, have to be handled. For Proposition 1, the hitting probability is defined as an infinite series of first-passage probabilities over trajectories, and the closed form is a statement about the value of that series.

Formalization scope

• The walks are transition matrices in the platform's MarkovMixing vocabulary (mm_basic, mm_path). Stationarity is MarkovMixing.IsStationary (nonnegative, sums to one, $mP=m$), and hitting probabilities are MarkovMixing.hitBeforeProb, a series that sums to $0$ when it is not summable. The absorbed walk is absorbed almost surely, so this convention is never triggered.
• The absorbed walk has states Fin (l₁ + l₂ + 1), with index $i$ for the balance $i-l_1$. The reset walk has states Fin (l₁ + l₂ - 1), with index $j$ for the balance $j+1-l_1$. massAt reads $m(n)$ at an integer balance and returns $0$ outside the interior, which is the paper's convention $m(l_2)=m(-l_1)=0$.
• Rates are real with $\lambda_1,\lambda_2>0$, and sizes are natural numbers $l_1,l_2\ge1$.
• The hypothesis $\lambda_1\neq\lambda_2$ ($q\neq1$) is added to Proposition 2 and to (28)–(30). The formulas divide by $q-1$, and the paper treats $q=1$ only as a limit.
• The "long-term ratio" is read as $1/f(m)$ for a stationary $m$, as in the paper's proof. Its identification with a pathwise long-run average is an ergodic theorem that the paper does not state and the mission does not ask for.
• Proposition 2 (i)–(ii) are limits of the closed form along $q\downarrow0$ and $q\to1$, $q\neq1$.
• The following would trivialize the problem and are excluded: fixing the sizes or the rates, setting $\lambda_1=\lambda_2$, defining the long-term ratio or the stationary distribution by the closed form, or quantifying over stationary distributions without proving that one exists.
• The platform has the Proved results MarkovMixing.exists_stationary_pos and MarkovMixing.stationary_unique for irreducible chains, and the fair gambler's ruin. Lemmas on stationary laws of chains with resets, and biased gambler's-ruin results on the MarkovMixing chains, would be reusable beyond this mission and are welcome.

Selected references

• P. Guasoni, G. Huberman, C. Shikhelman, Lightning Network Economics: Channels, Management Science, Articles in Advance, published online November 6, 2023, pp. 1–14. https://doi.org/10.1287/mnsc.2022.01664
• J. Poon, T. Dryja, The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments, white paper, 2016. https://lightning.network/lightning-network-paper.pdf
• D. A. Levin, Y. Peres, E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009 (§1.5, §2.1). https://doi.org/10.1090/mbk/058

Motivation

In inverse optimization one observes the decisions of an expert who solves an optimization problem and tries to recover the expert's objective. The contextual version of Besbes, Fonseca and Lobel (arXiv:2106.14015; Operations Research, 2025) asks a sharper question: not how well the cost can be estimated, but how well a decision-maker who imitates the expert performs, measured by regret against the expert. Settings of this kind arise whenever a firm wants to reproduce the routine choices of an experienced planner, for example routing, assortment or scheduling decisions, without being told the planner's cost trade-offs.

The online setting is adversarial. Nature fixes an unknown cost vector and then presents a sequence of problems; after each decision it reveals the expert's optimal action, which cuts the set of costs still consistent with the observations. A companion mission of this series shows that the natural greedy policy, which plays the center of this consistent set, can incur regret linear in the horizon. This mission formalizes the paper's first positive answer: an algorithm, EllipsoidalCones, with regret logarithmic in the horizon when the initial set of costs lies inside a pointed cone.

Setting

Costs lie on the unit sphere $S^d$ of $\mathbb R^d$, $d=m+1\ge2$. In period $t$ nature presents a feasible set $\mathcal X_t\subseteq\mathbb R^n$, compact, nonempty and of diameter at most $1$, and a $1$-Lipschitz context $f_t:\mathbb R^n\to\mathbb R^d$. The forward problem with cost $c$ has solution set $\psi(c,\mathcal X_t,f_t)=\operatorname{argmin}_{x\in\mathcal X_t}f_t(x)'c$. The decision-maker plays some $x^\pi_t$, nature reveals an expert action $x^\star_t\in\psi(c^\star,\mathcal X_t,f_t)$ for the true cost $c^\star$, and the regret over $T$ periods is

$$\mathcal R^\pi_T=\sum_{t=1}^T\big(f_t(x^\pi_t)-f_t(x^\star_t)\big)'c^\star .$$

The knowledge set $C(\mathcal I_t)$ is the set of costs in the initial set $C_0\subseteq S^d$ under which every expert action seen so far was optimal.

The angle between nonzero vectors is $\theta(c,\hat c)=\arccos(c'\hat c/\|c\|\|\hat c\|)$, and the uncertainty angle of a set $C$ is $\alpha(C)=\inf_{\hat c\in S^d}\sup_{c\in C}\theta(c,\hat c)$; a minimizing $\hat c$ is a circumcenter. The initial set is pointed when $\alpha(C_0)<\pi/2$.

For a positive diagonal $W=\operatorname{diag}(w_1,\dots,w_m)$ and an orthonormal $U$, the ellipsoidal cone is

$$E(W,U)=\{c:\ \tilde c_{[1]}\ge0,\ \tilde c_{[2:d]}'W^{-1}\tilde c_{[2:d]}\le\tilde c_{[1]}^2\},\qquad \tilde c=U^{-1}c ,$$

a cone with axis $Ue_1$ and elliptical cross-section. The effective difference of period $t$ is $\delta^\pi_t=(f_t(x^\pi_t)-f_t(x^\star_t))/\|f_t(x^\pi_t)-f_t(x^\star_t)\|$ (and $0$ if the difference vanishes).

EllipsoidalCones with parameter $\epsilon$ starts from the circular cone $W_1=\tan^2\alpha(C_0)I$, $U_1e_1$ a circumcenter of $C_0$, and plays the axis $U_te_1$ as proxy cost. With $\bar\delta=U_t^{-1}\delta^\pi_t$ it keeps the cone if

$$\bar\delta_{[2:d]}'W_t\bar\delta_{[2:d]}\le\epsilon^2 \qquad (12)$$

and otherwise replaces it by the output of ConeUpdate, which performs one central-cut step of the ellipsoid method on the cone's cross-section and re-centres the result by a spectral decomposition.

Formalization targets

Goal: Theorem 3 (p. 20)

With $\epsilon=d/T$ there is an absolute constant $K$ such that for every $d\ge2$, $T\ge1$, closed pointed $C_0$ with $\alpha(C_0)>0$, $c^\star\in C_0$, admissible instances and run,

$$\mathcal R^\pi_T\le K\,d^2\ln\big(T\tan\alpha(C_0)\big)\ \text{ if }\alpha(C_0)>\arctan(d/T),\qquad \mathcal R^\pi_T\le K\,d\ \text{ otherwise.}$$

The constant is left unfixed: the shape $d^2\ln(T\tan\alpha(C_0))$ is the claim, and the proof's explicit constant rests on a step that fails at $d=2$.

Milestones

1. Proposition 1: $\alpha(E(W,U))=\arctan\sqrt{\lambda_{\max}(W)}$.
2. Lemma 4: if $C(\mathcal I_t)\subseteq E(W_t,U_t)$ and (12) holds, the period's regret is at most $\epsilon$.
3. Lemma B-1 ($\eta=0$): ConeUpdate's output contains $E(W,U)\cap\{\delta'c\ge0\}$ and $\prod\lambda_i$ shrinks by $e^{-1/(2(d-1))}$.
4. Lemma 3: $C(\mathcal I_{t+1})\subseteq E(W_t,U_t)\cap\{\delta^{\pi\prime}_tc\ge0\}\subseteq E(W_{t+1},U_{t+1})$, and for $d\ge3$ $\prod\lambda_i$ shrinks by $e^{-1/(d-1)}$.
5. Cohen et al. (2020), Lemmas 3 and 4 (already posed on the platform, referenced): an ellipsoid-method step shrinks the smallest eigenvalue by at most $(d-1)^2/d^2$, and does not shrink it at all below the threshold $(\epsilon/(10(d-1)))^2$ when the cut is long.
6. Lemma 5: for $d\ge3$, $\lambda_{\max}(W_t)\le(10d/\epsilon)^{2(d-2)}\lambda_{\max}(W_1)^{d-1}e^{-I^\pi_t/(d-1)}$, or no update ever happens.

Significance

The theorem shows that in contextual inverse optimization the decision-maker can force nature to reveal information: a cone update happens only after a large mistake, and each such mistake shrinks the cone geometrically, so large mistakes are logarithmically rare. It is the building block of the paper's general-case algorithm, which restarts the same construction in growing subspaces, and it isolates why the greedy policy fails: it never trades instantaneous regret for information.

The paper proves the result; nothing in it is machine-checked. The mission produces a checked version of the pointed-case analysis, an ellipsoidal-cone layer on top of the platform's ellipsoid-method definitions, and corrected statements where the printed ones are imprecise: the dimension restriction $d\ge3$ for the rate of Lemma 3 and the first part of Lemma 5, the column order of the spectral decomposition in ConeUpdate, and the $\eta=0$ case of Lemma B-1.

Difficulty

Two steps resist the obvious argument. First, ConeUpdate is not the ellipsoid method: the minimum-volume ellipsoid of the cut cross-section has the right volume but its cone is no longer centred, and the new cone's axis is an eigenvector of an indefinite bordered matrix. Showing that this re-centred cone still contains the cut cone requires matching the eigenvalues of the bordered matrix with those of the ellipsoid matrix in the right order. Second, a volume decrease alone does not bound the regret: by Proposition 1 the uncertainty angle is governed by the largest eigenvalue, and the ellipsoid method can make that eigenvalue grow. The lazy test (12) and the smallest-eigenvalue lemmas of Cohen et al. are what keep the cones from becoming long and thin; without them the product of eigenvalues falls while the angle does not.

Formalization scope

Costs live in EuclideanSpace ℝ (Fin (m+1)) with $d=m+1$, actions in EuclideanSpace ℝ (Fin n), so all norms are Euclidean. $W$ is stored as its diagonal $w$, $U$ as a real orthogonal matrix, and $U^{-1}$ is written $U^\top$. Lean periods are $0$-based: Lean period $t$ is the paper's period $t+1$. This text is the arXiv v3 preprint (1 July 2023), not the published 2025 article; all numbering is the preprint's.

Standing assumptions carried by the statements: $d\ge2$, $n\ge1$, feasible sets nonempty, compact and of diameter at most $1$, contexts $1$-Lipschitz, $C_0$ a closed subset of $S^d$, $\epsilon>0$. Pinned and disclosed choices:

• ConeUpdate is a relation, not a function. The printed $U^{-1}B\delta_{[2:p]}$ is read as $(U^{-1}\delta)_{[2:p]}$. The first column of $V$ is the eigenvector of the positive eigenvalue of $M$ with positive first entry, and larger $|\mu|$ is paired with larger eigenvalues of $N$. The page leaves this order open, and Algorithm 1 and Lemma B-1 disagree on it.
• The printed "$U_1\leftarrow I_{d-1}$" is read as: $U_1$ orthonormal with a circumcenter of $C_0$ as its first column.
• $\alpha(C_0)>0$ on the goal. At $\alpha(C_0)=0$ the algorithm's $W_1=0$ is not positive definite.
• The rate of Lemma 3 and the first part of Lemma 5 are stated for $d\ge3$ only; the rest of both lemmas for every $d\ge2$. At $d=2$ ConeUpdate halves $W$, and $1/2>e^{-1}$.
• Lemma B-1 is stated only for $\eta=0$. Its $\eta>0$ inclusion is false as printed.
• The worst-case regret is stated as a bound for every true cost, every adaptive instance sequence and every run, not as a real supremum. The polynomial running-time claim is not formalized.

The run predicate is satisfiable: a circumcenter of a closed nonempty $C_0$ exists, the bordered matrix has exactly one positive eigenvalue, and a cone update is required only when the tail of $\bar\delta$ is nonzero. A formalization in which no run exists, or in which $K$ may depend on $d$ or $T$, does not state Theorem 3.

A complete development needs the angle and uncertainty-angle layer, ellipsoidal cones and their cross-sections, the published ellipsoid-method update (LinearOptimization_EllipsoidMethod) with its volume and eigenvalue facts, Cauchy–Schwarz over ellipsoids, and eigenvalue interlacing for bordered matrices. The ellipsoidal-cone layer and the cone-update lemma can be reused in the paper's general case and in other cone-based learning algorithms. Proofs of any milestone, and of the referenced Cohen et al. lemmas, are welcome.

Selected references

• O. Besbes, Y. Fonseca, I. Lobel, Contextual Inverse Optimization: Offline and Online Learning, arXiv:2106.14015v3, 2023; Operations Research, 2025. https://arxiv.org/abs/2106.14015
• M. C. Cohen, I. Lobel, R. Paes Leme, Feature-Based Dynamic Pricing, Management Science 66(11), 2020. https://doi.org/10.1287/mnsc.2019.3485
• M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, 2nd ed., Springer, 1993. https://doi.org/10.1007/978-3-642-78240-4
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 8.