All missions

Two quadratic functions can be compared losslessly. The S-procedure says that, when the constraint is strictly feasible, the implication

holds if and only if a single nonnegative multiplier certifies it as a matrix inequality, $\lambda \begin{bmatrix} F_1 & g_1 \\ g_1^{T} & h_1\end{bmatrix} \succeq \begin{bmatrix} F_2 & g_2 \\ g_2^{T} & h_2\end{bmatrix}$ for some $\lambda \ge 0$. It is a cornerstone of control theory, trust-region methods and robust optimization, and a rare case in which a nonconvex problem has zero duality gap. The route runs through the theory this mission builds from Boyd & Vandenberghe §5.8–5.9 and Appendix B: strong alternatives for convex inequality systems, cone-program strong duality under a generalized Slater condition, semidefinite programming duality, the LMI theorems of alternatives, and the hidden convexity of the joint range of two quadratic forms.

Log-concave functions are the meeting point of convex analysis and probability: densities of Gaussian, exponential, uniform and Wishart distributions are all log-concave, and countless facts of applied probability flow from one structural theorem — integrating out variables preserves log-concavity. This mission builds the convex-analysis spine of Boyd & Vandenberghe's Convex Optimization (Chapters 2–3) — separation and supporting hyperplanes, dual cones, the first- and second-order differential characterizations of convexity, Fenchel conjugacy — and climbs to Prékopa's theorem via the Prékopa–Leindler inequality, a landmark of Brunn–Minkowski theory absent from Mathlib.

Value decomposition — approximating the value of a joint state by a sum of per-agent local values — is a staple of multi-agent dynamic programming and reinforcement learning, from index policies for restless bandits to modern MARL architectures, yet it is normally used without justification. Chen and Peng (arXiv:2506.02385) supply one. They show a multi-agent MDP admits an exact value decomposition precisely when its transition matrix is not entangled — a notion built in direct analogy with quantum entanglement — and then turn that qualitative characterisation into a quantitative one: a measure of Markov entanglement bounds the decomposition error in general. This mission formalizes that core theory. The goal is Theorem 6, the general N-agent bound in the occupancy-weighted norm; the milestones are the equivalence between separability and exact decomposition, the perturbation machinery that carries a one-step transition error into a value-function error, and the extensions to shared global state and shared rewards. The paper's restless-bandit application, which needs mean-field machinery of its own, is left to a second mission in the series.

The Monge optimal transport problem on the real line with the classical distance cost $|x-y|$ famously fails to have a unique solution. Juillet (2019) restored uniqueness by considering the strictly concave power costs $|x-y|^p$ with $p<1$ and letting $p\to 1^-$: the limit selects a distinguished optimal plan, the excursion coupling, built from the level sets of the difference $F_\sigma=F_\mu-F_\nu$ of the cumulative distribution functions. This mission formalizes the completed-graph construction, the generalized Banach indicatrix identities of Bertoin-Yor, the alternating crossing structure of almost every level, and the marginal identities for the crossing counting measures. It culminates in Propositions 3.5-3.6: every monotone transport plan is concentrated on the paired routes, and the marginals uniquely determine the coupling carried by those routes, including in the presence of atoms.

This mission formalizes the key implication 3=>4 in Juillet's Main Theorem.

How much flow can be sent from a source $s$ to a sink $t$ through a network with arc capacities $u_{ij}\in(0,\infty]$ — and what certifies that no more is possible? This mission formalizes §7.4-7.5 of Bertsimas & Tsitsiklis. The circulation calculus of §7.4 supplies the two structural tools: the flow decomposition theorem (Lemma 7.1 — every nonzero nonnegative circulation is a positive combination $\mathbf{f}=\sum_i a_i\mathbf{f}^i$ of simple circulations with only forward arcs, with integer $a_i$ when $\mathbf{f}$ is integer) and the optimality criterion for the minimum cost network flow problem (Theorem 7.6 — a feasible flow is optimal if and only if there is no unsaturated cycle with negative cost). Section 7.5 then formulates the maximum flow problem ($\max b_s$ s.t. $\mathbf{A}\mathbf{f}=\mathbf{b}$, $b_t=-b_s$, $b_i=0$ for $i\ne s,t$, $0\le\mathbf{f}\le\mathbf{u}$), defines augmenting paths (Definition 7.2: $f_{ij}<u_{ij}$ on forward arcs, $f_{ij}>0$ on backward arcs) and the Ford–Fulkerson algorithm, and proves integer invariance and finite termination for integer capacities (Theorem 7.8). The goal is Theorem 7.10:

(a) if the Ford–Fulkerson algorithm terminates because no augmenting path can be found, the current flow is optimal;

(b) the value of the maximum flow equals the minimum cut capacity

— the archetypal combinatorial min-max theorem, which the book notes can also be read as LP duality (pp. 311-312).

Sometimes reward during learning is irrelevant — a pharmaceutical company running phase-II trials only cares about identifying the best treatment, as quickly and as reliably as possible. Chapter 33 of Lattimore–Szepesvári formalizes fixed-confidence best-arm identification: a policy together with a stopping time $\tau$ and a recommendation must be sound (wrong with probability at most $\delta$) while minimizing $\mathbb{E}[\tau]$. The information-theoretic complexity is $c^*(\nu)^{-1} = \sup_{\alpha\in\mathcal{P}_{k-1}} \inf_{\nu'\in\mathcal{E}_{alt}(\nu)} \sum_i \alpha_i D(\nu_i, \nu_i')$: every sound strategy needs $\mathbb{E}[\tau] \ge c^*(\nu)\log\frac{1}{4\delta}$, and the Track-and-Stop algorithm — the goal theorem — achieves $\lim_{\delta\to 0} \mathbb{E}[\tau]/\log(1/\delta) = c^*(\nu)$ exactly. The mission also covers the fixed-budget counterpart, sequential halving.

When rewards are binary — a click or no click, a cure or no cure — the subgaussian machinery of Missions I–III is not tight: the variance of a Bernoulli arm degrades near the boundary of $[0,1]$, and the correct exponential rate is governed by the binary relative entropy $d(p,q) = p\log\frac{p}{q} + (1-p)\log\frac{1-p}{1-q}$ rather than a squared distance. Chapter 10 of Lattimore–Szepesvári develops Chernoff's tail bound in its information-theoretic form and the KL-UCB algorithm, whose upper confidence bounds are level sets of $d$. The goal theorem shows KL-UCB attains

— asymptotic optimality with exactly the constant demanded by the lower bound of Mission VII, strictly improving subgaussian UCB on every Bernoulli instance.

Every lower bound in bandit theory rests on one question: how hard is it to tell two probability measures apart from a sample? The answer is quantified by the relative entropy $D(P,Q)$, and the sharpest elementary tool is the Bretagnolle–Huber inequality: for any event $A$, $P(A) + Q(A^c) \ge \frac{1}{2}\exp(-D(P,Q))$ — no test can distinguish $P$ from $Q$ with total error probability below $\frac{1}{2}e^{-D(P,Q)}$. This mission formalizes Chapter 14 of Lattimore–Szepesvári: the Bretagnolle–Huber inequality (the goal theorem, proved via Le Cam's inequality $\int p \wedge q \ge \frac{1}{2}(\int\sqrt{pq})^2$), Pinsker's inequality $\delta(P,Q) \le \sqrt{D(P,Q)/2}$, and the closed-form divergences between Gaussians and Bernoullis. These half-page inequalities power every impossibility result in Missions VII, XI and beyond.

Motivation

Large language models are now deployed as decision aids next to human decision-makers, and a basic empirical question is whether the pair does better than either party alone. Baek, Fu, Ma and Peng (arXiv:2602.12631v2) study this question for inventory control: they build a benchmark of multi-period inventory problems, compare operations-research policies, LLM agents and their hybrids, and run a classroom experiment in which students manage inventory with and without an AI assistant.

The experiment raises a statistical issue that is independent of inventory control. Average gains at the population level do not show that any individual benefits: if weak decision-makers simply adopt the AI's recommendation and strong ones ignore it, the average collaborative performance can exceed both stand-alone averages while no single person improves on the better of their own and the AI's performance. The quantity of interest is therefore the fraction of individuals who benefit, and it is not identified: each person is observed in only one condition (alone or with the AI), so the joint law of the two outcomes is unknown and only their marginal laws can be estimated.

Section 6.1 of the paper answers this with a distribution-free lower bound on the fraction of individuals whose gain exceeds a threshold, computed from the two marginal distributions alone, and shows that the bound cannot be improved. The bound is an instance of the classical bounds on the distribution of a difference of two random variables with given marginals (Makarov, 1981; Rüschendorf, 1982; Frank, Nelsen and Schweizer, 1987), applied to the identification problem of a human–AI experiment.

Setting

A person $i$ is drawn from a population. Write $y_H^{(i)}$ for their performance alone, $y_{AI}$ for the AI's performance, and $y_{H+AI}^{(i)}$ for their performance with the AI. The individual complementarity effect is

Set $a(i) = \max(y_H^{(i)}, y_{AI})$ and $b(i) = y_{H+AI}^{(i)}$, so that $\mathrm{CE}_i = b(i) - a(i)$. In the formal development the population is a probability space $(\Omega, P)$ and $a, b : \Omega \to \mathbb R$ are measurable functions.

The cumulative distribution function of a probability law $\mu$ on $\mathbb R$ is the right-continuous function $F(t) = \mu((-\infty, t])$; $F_a$ and $F_b$ denote those of $a$ and $b$. A joint law (coupling) of $(a, b)$ with marginals $\mu_a, \mu_b$ is a probability measure $\pi$ on $\mathbb R^2$ whose first and second marginals are $\mu_a$ and $\mu_b$. For a threshold $\delta \ge 0$ the bound is

called makarovBound δ μa μb in Lean.

Formalization targets

Goal: Theorem 1 (p. 17)

For every $\delta \ge 0$:

1. for every population law of $(a, b)$,

2. for any two marginal laws $\mu_a, \mu_b$ on $\mathbb R$ there is a joint law $\pi$ with these marginals under which $\pi[b - a > \delta] = \varepsilon(\delta)$.

Both clauses are part of the goal. The first says the bound is valid; the second says it is the best bound obtainable from the marginals.

Milestones (Appendix K, p. 46)

• (5): $\mathbb P[\mathrm{CE}_i > \delta] \ge \mathbb P[b > t + \delta,\ a \le t]$ for every $t$.
• (6): $\mathbb P[b > t + \delta,\ a \le t] \ge (1 - F_b(t + \delta)) + F_a(t) - 1 = F_a(t) - F_b(t + \delta)$.
• $\varepsilon(\delta) \ge 0$.
• If $\varepsilon = 1$, then $b - a > \delta$ almost surely under every coupling.
• For $\varepsilon < 1$: the retained sub-distributions $F_{a^+} = \max\{F_a - \varepsilon, 0\}$ and $F_{b^-} = \min\{F_b, 1 - \varepsilon\}$ are distribution functions of sub-measures of mass $1 - \varepsilon$, and $F_{a^+}(t) \le F_{b^-}(t + \delta)$.
• Retained masses ordered in this way can be coupled with $b - a \le \delta$ almost surely.
• Adding an arbitrary coupling of the remaining $\varepsilon$-mass gives a joint law with $\Pr(b - a > \delta) \le \varepsilon$.

Significance

The result. The bound converts two marginal distributions, each estimable from a separate experimental arm, into a guaranteed lower bound on the share of individuals who gain more than $\delta$ from collaboration. Tightness shows that no other function of the marginals gives a better guarantee: any improvement needs information about the joint law. At $\delta = 0$ (Corollary 1, p. 18) the bound is a one-sided Kolmogorov–Smirnov distance between the two marginals, which the paper estimates from its classroom data in §6.2.

Formalizing it. The result is proved in the paper, with one gap: the degenerate case $\varepsilon = 1$ of the tightness proof asserts a threshold $t^*$ that need not exist (see below). The mission targets a machine-checked proof of both clauses for arbitrary laws on $\mathbb R$, atoms included. Along the way it needs two reusable pieces: the decomposition of a law on $\mathbb R$ into its lower $\varepsilon$-mass and the rest, and the monotone coupling of two finite measures ordered in the first-order stochastic sense. No machine-checked statement of the Makarov bound or of its sharpness was found on the platform or in Mathlib.

Difficulty

The lower bound is a two-line argument. The content is tightness, and three points are delicate. First, the supremum need not be attained, so the case $\varepsilon = 1$ cannot be handled by choosing a threshold as the printed proof does; for $\delta = 1/2$, $a \sim \mathrm{Uniform}(-1, 0)$ and $b \equiv 1/2$, one has $\varepsilon = 1$ but no such threshold. Second, when $\varepsilon < 1$ the split of a law at its $\varepsilon$-quantile must cut through atoms: a retained sub-measure is not, in general, the restriction of the law to a set. Third, the event $\{b - a > \delta\}$ is strict and the CDFs are right-continuous, so atoms of $a$ at $t$ and of $b$ at $t + \delta$ must be accounted for exactly; changing either convention changes the value of the bound.

Formalization scope

All objects live in the namespace HumanAIComp.Bound. Laws on $\mathbb R$ are Measure ℝ with IsProbabilityMeasure; distribution functions are Mathlib's ProbabilityTheory.cdf; probabilities are Measure.real. The population is an arbitrary probability space and $a, b$ are arbitrary measurable real functions: the theorem and its proof never use the form $a = \max(y_H, y_{AI})$, which is one instance. Couplings are the published MongeKantorovichYao.transferencePlans μa μb. The bound is a real supremum over $t \in \mathbb R$ of a family bounded above by $1$, so it is the true supremum. The hypothesis $\delta \ge 0$ of the paper is kept.

A formalization that fixed example marginals, or let the coupling's marginals vary, would make the tightness clause trivial; the goal quantifies over all pairs of probability laws on $\mathbb R$ and requires a coupling with exactly those marginals. The milestones on the case $\varepsilon = 1$ state only the conclusion, not the printed threshold claim.

The monotone coupling theorem for probability measures is on the platform as StochasticOrders.Usual.usual_order_coupling_iff_v2 (Proved), and is included as a reference. Contributions of general lemmas about sub-measures with prescribed distribution functions, and about couplings of finite measures, are welcome.

Selected references

• J. Baek, Y. Fu, W. Ma, T. Peng, AI Agents for Inventory Control: Human-LLM-OR Complementarity, arXiv:2602.12631v2, 2026. https://arxiv.org/abs/2602.12631
• G. D. Makarov, Estimates for the distribution function of a sum of two random variables when the marginal distributions are fixed, Theory of Probability and its Applications 26 (1981) 803–806. https://doi.org/10.1137/1126086
• L. Rüschendorf, Random variables with maximum sums, Advances in Applied Probability 14 (1982) 623–632. https://doi.org/10.2307/1426677
• M. J. Frank, R. B. Nelsen, B. Schweizer, Best-possible bounds for the distribution of a sum — a problem of Kolmogorov, Probability Theory and Related Fields 74 (1987) 199–211. https://doi.org/10.1007/BF00569989
• M. Shaked, J. G. Shanthikumar, Stochastic Orders, Springer, 2007. https://doi.org/10.1007/978-0-387-34675-5

Motivation

Many problems in statistics and signal processing ask for a vector that is both small in some norm and sparse, with at most $K$ nonzero entries. The best-known example is sparse principal component analysis (sparse PCA), whose feasible set is the set of unit vectors in the Euclidean norm with at most $K$ nonzero entries (d'Aspremont et al. 2007). Cardinality constraints make such sets nonconvex, and convex relaxations of the problem need a description of their convex hull.

Kim, Tawarmalani and Richard (arXiv:1910.02573v2, Mathematics of Operations Research, 2022) describe convex hulls of sets that are invariant under permutations and sign changes of coordinates through majorization inequalities. Their §3 applies this to cardinality-constrained norm balls: for every symmetric gauge function $\|\cdot\|_s$ (a norm invariant under permutations and sign changes) it gives the convex hull of $\{x : \|x\|_s \le 1, \operatorname{card}(x) \le K\}$ as the unit ball of an explicit norm, and the Sparsity Theorem gives a closed-form optimal solution of the associated majorization program. For the Euclidean norm, the norm obtained is the $K$-support norm of Argyriou, Foygel and Srebro (2012), used as a regularizer in sparse prediction.

Setting

Vectors live in $\mathbb R^n$. For $x \in \mathbb R^n$, $|x| = (|x_1|, \dots, |x_n|)$, $x_{[i]}$ is the $i$-th largest entry of $x$, and $|x|_{[i]}$ is the $i$-th largest entry of $|x|$. $\operatorname{card}(x)$ is the number of nonzero entries.

Majorization. $x$ majorizes $y$, written $x \ge_m y$, if $\sum_{i \le j} x_{[i]} \ge \sum_{i \le j} y_{[i]}$ for $j = 1, \dots, n-1$, with equality of the full sums. $y$ is weakly submajorized by $x$, written $x \ge_{wm} y$, if the partial-sum inequalities hold for $j = 1, \dots, n$ and no equality is required.

Fix a symmetric gauge function $\|\cdot\|_s$ and an integer $K$ with $1 < K < n$ (for $K = 1$ the hull is an $\ell_1$ ball, and for $K = n$ the constraint is void). Set

Its convex hull is a compact convex set, symmetric about $0$, with $0$ in its interior. Its gauge

is therefore a norm. For $x \in \mathbb R^n$ and $i = 1, \dots, K$ put

let $i_x$ be the smallest index minimizing $s(x)_i$ over $1 \le i \le K$, and $\delta(x) = s(x)_{i_x}$. The vector $u(x)$ of (15) has entries $|x|_{[i]}$ for $i < i_x$, $\delta(x)$ for $i_x \le i \le K$, and $0$ beyond $K$.

Formalization targets

Goal: the Sparsity Theorem (Theorem 3.2, p. 9)

For every $x \in \mathbb R^n$, $u(x)$ is an optimal solution of

and, as the paper reads the theorem on p. 6,

Milestones

In attack order:

• Lemma 2.1: a linear map that maps $S$ into itself maps $\operatorname{conv}(S)$ into itself.
• Lemma 2.2: $x \ge_m y$ iff $y$ is a convex combination of permutations of $x$. This is already proved on the platform.
• Lemma 3.1: permutation-invariant norms are monotone under $\ge_m$.
• Proposition 3.1: $\operatorname{conv}(N^K)$ is a convex body.
• Proposition 3.2: $\operatorname{conv}(N^K)$ is the unit ball of the sign- and permutation-invariant norm $\|\cdot\|_c$.
• Proposition 3.3: $\|x\|_c = \|x\|_s$ when $\operatorname{card}(x) \le K$.
• Proposition 3.4: the recursion and unimodality of $s(x)$, $u(x) \ge_m |x|$, and $u(x)_1 = \max\{|x|_{[1]}, s(x)_1\}$.
• Theorem 3.1: $\|x\|_c = \|u(x)\|_s$.
• The weak-majorization fact 5.A.9 of Marshall–Olkin–Arnold, which the proof of Theorem 3.2 cites: $u \ge_{wm} y$ implies that some $u'$ satisfies $u \ge_m u'$ and $u' \ge y$.

Significance

The result. The theorem reduces membership in the convex hull of a cardinality-constrained norm ball to one sort of $|x|$, a scan over $K$ averages and one evaluation of $\|\cdot\|_s$. It also gives an explicit extended formulation and a separating hyperplane (Corollary 3.1). The paper uses these to build relaxations for sparse PCA whose valid inequalities rest on this hull description. Specialized to $\ell_2$ it recovers the closed form of the $K$-support norm, and specialized to $\ell_\infty$ the norm of Proposition 3.5. The result holds for every symmetric gauge, so it covers all $\ell_p$ norms at once.

Formalizing it. The result is proved in the paper; none of it is machine-checked. The mission would supply a formal theory of majorization and weak majorization through sums of largest entries, Schur-convexity of symmetric norms, and the gauge of a convex hull of a symmetric nonconvex set. The platform already has Lemma 2.2 (the Hardy–Littlewood–Pólya/Birkhoff characterization) as a proved theorem, and the mission builds on it.

Difficulty

The inequality $\|x\|_c \le \|u(x)\|_s$ follows from $u(x) \ge_m |x|$ and the monotonicity of symmetric norms under majorization. The reverse inequality $\|x\|_c \ge \|u(x)\|_s$ is the hard part. An upper bound on a gauge needs a single convex combination, but a lower bound needs a linear inequality that holds on the whole nonconvex set $N^K_{\|\cdot\|_s}$, for an arbitrary symmetric gauge whose dual norm is not known in closed form. Bounding by $\|x\|_s$ itself does not work: the two norms agree only on $K$-sparse vectors. The particular index $i_x$, the first minimizer of $s(x)$, is what makes the closed form exact, and replacing it by any other index breaks the identity. The paper treats sorted order statistics as notation; a formal proof has to carry them explicitly.

Formalization scope

Vectors are Fin n → ℝ, and Lean index $i$ is the paper's $i+1$. A norm $\|\cdot\|_s$ is a plain function (Fin n → ℝ) → ℝ that satisfies the axioms in the structures IsPermInvNorm (definite, subadditive, absolutely homogeneous, permutation-invariant) and IsSymmetricGauge (also sign-invariant). Lean's built-in norm on Fin n → ℝ is the sup norm, so stating the theorems for it would prove only the $\ell_\infty$ case; every statement here instead quantifies over all symmetric gauges. The standing assumption $1 < K < n$ (p. 6) is a hypothesis of every §3 item.

Sums of the $j$ largest entries are the published ModernConvex.Spectral.sumLargest (from ModernConvex_Spectral_SDR), used only for $1 \le j \le n$. With it, $\ge_m$ is the right-hand side of the published majorization_principle. Weak majorization runs over $j = 1, \dots, n$. $|x|_{[\cdot]}$ is built from Mathlib's Tuple.sort. $s(x)$ and $i_x$ keep the paper's 1-based indices and are used only on $1, \dots, K$. The convention $s(x)_0 = s(x)_{K+1} = \infty$ only excludes those indices from the minimization. The norm $\|\cdot\|_c$ is Mathlib's gauge of convexHull ℝ (NK ns K): (14) writes a minimum, which is an infimum at $x = 0$. A convex body is a compact convex set with nonempty interior.

In the goal, the minimizer is the specific closed-form $u(x)$, and minimality is over every feasible point of (11). The equivalence in part 2 is with membership in the actual convex hull, not with a set chosen to make it true. Contributions are welcome at every milestone; Lemma 3.1, 5.A.9 and Propositions 3.1–3.2 are reusable beyond this mission.

Selected references

• J. Kim, M. Tawarmalani, J.-P. P. Richard, Convexification of Permutation-Invariant Sets and an Application to Sparse Principal Component Analysis, Mathematics of Operations Research, 2022; arXiv:1910.02573v2. https://arxiv.org/abs/1910.02573v2
• A. W. Marshall, I. Olkin, B. C. Arnold, Inequalities: Theory of Majorization and Its Applications, 2nd ed., Springer, 2011. https://doi.org/10.1007/978-0-387-68276-1
• A. Argyriou, R. Foygel, N. Srebro, Sparse Prediction with the k-Support Norm, NeurIPS 2012. https://arxiv.org/abs/1204.5043
• A. d'Aspremont, L. El Ghaoui, M. I. Jordan, G. R. G. Lanckriet, A Direct Formulation for Sparse PCA Using Semidefinite Programming, SIAM Review 49(3), 2007. https://doi.org/10.1137/050645506

Motivation

Coding theorems and (strong) converses for memoryless quantum communication channels and quantum sources are proved: for the quantum source the coding theorem is reviewed, and the strong converse proven. For classical information transmission via quantum channels we give a new proof of the coding theorem, and prove the strong converse, even under the extended model of nonstationary channels. As a by-product we obtain a new proof of the famous Holevo bound. Then multi-user systems are investigated, and the capacity region for the quantum multiple access channel is determined. The last chapter contains a preliminary discussion of some models of compression of correlated quantum sources, and a proposal for a program to obtain operational meaning for quantum conditional entropy. An appendix features the introduction of a notation and calculus of entropy in quantum systems.

This mission is the statement-level formalization of Coding Theorems of Quantum Information Theory (arXiv:quant-ph/9907077v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

76 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem I.1: Dbar²≤1−Fbar≤Dbar; for quantum encoders also 1−Fbar≤1−Fe. (Theorem I.1, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

9 results of the paper are not stated yet, because the library lacks an interface they need:

• I.3-subnormalized: A valid complete statement of I.3-subnormalized under its printed hypotheses (source-ambiguity)
• Lemma II.8: A valid complete statement of Lemma II.8 under its printed hypotheses (source-ambiguity)
• Lemma II.12: A valid complete statement of Lemma II.12 under its printed hypotheses (source-ambiguity)
• Lemma II.15: A valid complete statement of Lemma II.15 under its printed hypotheses (source-ambiguity)
• Remark II.22: A valid complete statement of Remark II.22 under its printed hypotheses (source-ambiguity)
• Lemma II.24: A valid complete statement of Lemma II.24 under its printed hypotheses (source-ambiguity)
• Theorem IV.14: A valid complete statement of Theorem IV.14 under its printed hypotheses (source-ambiguity)
• Theorem A.3: A valid complete statement of Theorem A.3 under its printed hypotheses (source-ambiguity)
• Corollary A.25: A valid complete statement of Corollary A.25 under its printed hypotheses (source-ambiguity)

Selected references

• Coding Theorems of Quantum Information Theory, arXiv:quant-ph/9907077v1, https://arxiv.org/abs/quant-ph/9907077v1

Online learning with an approximation algorithm

Many sequential decision problems have a combinatorial action set: each round a decision maker picks a route, a schedule or a cut, and only afterwards learns its cost. When the offline problem — minimize a known linear cost over the action set — is NP-hard, the best available tool is an approximation algorithm, which returns a feasible action whose cost is within a factor $\alpha$ of optimal. The natural benchmark online is then the $\alpha$-regret: the learner's average cost minus $\alpha$ times the average cost of the best fixed action in hindsight.

Kakade, Kalai and Ligett (SIAM J. Comput. 2009) showed that any $\alpha$-approximation oracle can be converted into an online algorithm with vanishing $\alpha$-regret, but their conversion may call the oracle $O(T)$ times per round. Garber (arXiv:1709.03093, Mathematics of Operations Research 2021) gave the first conversion whose expected $\alpha$-regret is $O(T^{-1/3})$ while the number of oracle calls per round is polylogarithmic in $T$, in both the full-information and the bandit settings. This mission formalizes the full-information regret bound, Theorem 1 of that paper.

Setting

Vectors live in $\mathbb R^d$ with the Euclidean norm $\|\cdot\|$ and dot product $x\cdot f$; $\mathbb R^d_+$ is the non-negative orthant. An instance consists of compact sets $\mathcal K,\mathcal F\subset\mathbb R^d_+$, with $\mathcal K$ nonempty, and constants $R,F,C>0$ such that $\|x\|\le R$ on $\mathcal K$, $\|f\|\le F$ on $\mathcal F$, and $0\le x\cdot f\le C$ for $x\in\mathcal K$, $f\in\mathcal F$. Here $\mathcal K$ is the set of actions and $\mathcal F$ the set of loss (or payoff) vectors.

An $\alpha$-approximation oracle ($\alpha>0$) is a map $\mathcal O_{\mathcal K}$ that, for every $c\in\mathbb R^d_+$, returns $\mathcal O_{\mathcal K}(c)\in\mathcal K$ with $\mathcal O_{\mathcal K}(c)\cdot c\le\alpha\min_{x\in\mathcal K}x\cdot c$ when $\alpha\ge1$ (loss minimization), or $\mathcal O_{\mathcal K}(c)\cdot c\ge\alpha\max_{x\in\mathcal K}x\cdot c$ when $\alpha<1$ (payoff maximization).

Over $T$ rounds an oblivious adversary fixes $f_1,\dots,f_T\in\mathcal F$ in advance, and the learner plays $x_1,\dots,x_T\in\mathcal K$. The $\alpha$-regret is

The algorithm (Algorithm 3) is online gradient descent over $\mathrm{CH}(\alpha\mathcal K)$, the convex hull of $\alpha\mathcal K=\{\alpha x:x\in\mathcal K\}$, with exact projections replaced by infeasible projections: a point $\tilde y$ with $\|\tilde y-z\|^2\le\|y-z\|^2$ for all $z\in\mathrm{CH}(\alpha\mathcal K)$. They are computed by Algorithm 2, which repeatedly runs an Ellipsoid-method separation-or-decomposition procedure (Lemma 5) driven by an extended oracle $\hat{\mathcal O}_{\mathcal K}$ (Lemma 1) that accepts every direction in $\mathbb R^d$. When no separating direction is found, the procedure returns a probability vector $(a_1,\dots,a_N)$ over feasible points $s_1,\dots,s_N\in\mathcal K$, and the learner samples its next action from it.

Formalization targets

Goal: Theorem 1 (regret bound)

For $\eta>0$, $\varepsilon\in(0,(\alpha+2)R]$ and $T\ge1$, the points $s_1,\dots,s_T$ played by Algorithm 3 satisfy

The statement covers both $\alpha\ge1$ and $\alpha<1$ and every dimension $d\ge2$.

Milestones

1. Lemma 1 (p. 6): the extended oracle $\hat{\mathcal O}_{\mathcal K}(c)=(v,s)$ satisfies $v\cdot c\le\min_{x\in\alpha\mathcal K}x\cdot c$, $s$ dominates $v$ on $\mathcal F$, and $\|v\|\le(\alpha+2)R$.
2. Lemma 2 (p. 7): online gradient descent with infeasible projections keeps the regret bound $\frac1{2T\eta}\|x_1-x\|^2+\frac\eta{2T}\sum_t\|f_t\|^2$ against every $x$ in the feasible set.
3. Lemma 6 (p. 11): if $\min_i(x-v_i)\cdot w\le\varepsilon$ for every unit vector $w$, the minimum-norm convex combination $p$ of the $v_i$ satisfies $\|p-x\|\le\varepsilon$.
4. Lemma 5 (pp. 9–10): with $N\ge c\,d^2\ln\frac{(\alpha+1)R+\|x\|}{\varepsilon}$ Ellipsoid iterations, the procedure either finds $w$ with $(x-z)\cdot w\ge\varepsilon$ on $\alpha\mathcal K$ and $\|w\|\le1$, or a convex combination $p$ of oracle outputs with $\|x-p\|\le3\varepsilon$.
5. Lemma 7 (p. 12): Algorithm 2 terminates and returns an infeasible projection $\tilde y$ of its input onto $\mathrm{CH}(\alpha\mathcal K)$ with $\|p-\tilde y\|\le3\varepsilon$.

Significance

Theorem 1 shows that low $\alpha$-regret needs nothing beyond black-box access to an offline approximation algorithm, with an oracle cost per round that grows only logarithmically in the accuracy. It applies to any combinatorial problem with a linear objective and a known approximation algorithm, and it is the base of the paper's bandit result (Theorem 2), whose analysis reuses the same infeasible-projection argument.

The result is proved in the paper; none of it has been machine-checked. The mission adds a formal account of the model and the algorithms, including the conventions the paper leaves implicit (which Ellipsoid method, what the expectation ranges over). It also records two printed claims that are not stated here because they are incorrect as written: Lemma 7's iteration count $\lceil\alpha^2R^2/\varepsilon^2\rceil$, replaced by termination, and the bound $2\alpha^2R^2$ in Lemma 7's "Moreover" clause. A formal proof would confirm the regret bound independently of these slips.

Difficulty

The obvious approach, online gradient descent over $\mathrm{CH}(\alpha\mathcal K)$, needs Euclidean projections onto a set that can only be accessed by approximate linear optimization over $\mathcal K$, and only for directions in $\mathbb R^d_+$. Such an oracle cannot certify membership in $\mathrm{CH}(\alpha\mathcal K)$ and cannot optimize over it exactly, so exact projection is out of reach. Simulating the projection by an Ellipsoid run on $\mathrm{CH}(\alpha\mathcal K)$ itself also fails: the oracle answers only non-negative directions, and its answers are off by the factor $\alpha$. The regret analysis must therefore survive projections that are infeasible, decompositions that are only approximately correct, and points that are not even in $\mathcal K$.

For a formal proof the hardest part is Lemma 5. It is an Ellipsoid-method volume argument whose cut rule queries the oracle at every iterate, whose iteration constant is universal, and whose logarithm can be negative.

Formalization scope

All work is in the namespace ApproxOLO.FullInfo, in one definitions module. Vectors are Fin d → ℝ, and every norm is the Euclidean euclNorm x = √(x·x); Mathlib's ‖·‖ on this type (the sup norm) is not used anywhere. The two regimes $\alpha\ge1$ and $\alpha<1$ are kept everywhere, in the oracle, the regret, the extended oracle and the update $y_{t+1}=\tilde y_t\mp\eta f_t$. The oracle guarantee is stated for every $x\in\mathcal K$, which is equivalent to the min/max form. In the regret, the min and max are sInf/sSup of the image of the compact nonempty $\mathcal K$.

The Ellipsoid method, which the paper does not specify, is fixed as follows: it starts at the unit ball, and its update is the standard central cut from the published LinearOptimization_EllipsoidMethod module, with cut vectors $x-v$ and $-w$ in that module's sign convention. That update has the factor $d^2/(d^2-1)$, so Lemma 5, Lemma 7 and Theorem 1 assume $d\ge2$. $T\ge1$ is assumed wherever the factor $1/T$ appears. The universal constant $c$ of Lemma 5 is quantified once, before the dimension and the instance. Each call of the procedure uses a positive integer number of iterations $N$ satisfying that lower bound, and the number may differ from call to call.

Algorithms 2 and 3 are run predicates. The choices the paper leaves open ($s_1$, the iteration budgets, the optimal solution of Problem (5)) are quantified universally. The expected $\alpha$-regret is Eq. (1) evaluated at the per-round expected losses $\sum_ia_i\,s_i\cdot f_t$. This equals the expectation by linearity, because the iterates never depend on the samples and the adversary is oblivious.

A statement with $N=0$ allowed, an infeasible oracle hypothesis, a fixed $\alpha\ge1$, or a sup-norm in place of the Euclidean norm would be a different and partly trivial theorem; the statements exclude each of these. The sanity file exhibits an instance, an oracle and a one-round run satisfying all hypotheses.

Not formalized: the oracle-complexity bound $K(\eta,\varepsilon)$ and the "In particular" rates of Theorem 1 (big-$O$ statements with hidden constants), Lemma 7's iteration count and "Moreover" clause, the bandit setting (Definition 1, Algorithm 4, Theorem 2), and the comparison scheme of Lemmas 3–4. Reusable beyond this mission: the extended oracle, infeasible projections and Lemma 2, Lemma 6 on minimum-norm points of convex hulls, and the separation-or-decomposition procedure. Proofs of any milestone are welcome, as is a formal version of the oracle-complexity bound with explicit constants.

Selected references

• D. Garber, Efficient Online Linear Optimization with Approximation Algorithms, Mathematics of Operations Research 46(1), 2021; preprint arXiv:1709.03093v1, 2017. https://arxiv.org/abs/1709.03093
• S. M. Kakade, A. T. Kalai, K. Ligett, Playing Games with Approximation Algorithms, SIAM Journal on Computing 39(3), 2009. https://doi.org/10.1137/070701704
• M. Zinkevich, Online Convex Programming and Generalized Infinitesimal Gradient Ascent, Proceedings of ICML, 2003 (the origin of online gradient descent, reference [17] of the paper).
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, Chapter 8 (the Ellipsoid method).
• M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1988. https://doi.org/10.1007/978-3-642-97881-4

Motivation

The data processing inequality (DPI) for the conditional von Neumann entropy says that discarding part of the side information cannot make a quantum system less uncertain: for every tripartite state $\rho_{ABC}$,

It is equivalent to strong subadditivity of the von Neumann entropy, proved by Lieb and Ruskai in 1973 (Lieb–Ruskai), and it underlies most of quantum Shannon theory: the converse bounds of channel coding, the monotonicity of mutual information under local operations, and the security analysis of quantum key distribution all reduce to it. The known proofs rest on operator convexity (Lieb's concavity theorem) or on other non-elementary matrix analysis.

Beaudry and Renner (arXiv:1107.0740v2, Quantum Inf. Comput. 12 (2012) 432) give a proof that avoids operator convexity entirely. It first proves the DPI for a one-shot quantity, the smooth min-entropy, where it follows almost directly from the definition, and then recovers the von Neumann statement through the quantum asymptotic equipartition property (QAEP) of Tomamichel, Colbeck and Renner (arXiv:0811.1221), for which the paper supplies a short self-contained proof.

Timeline. 1973: Lieb–Ruskai prove strong subadditivity. 2009: Tomamichel–Colbeck–Renner prove the QAEP with explicit convergence rates. 2010: Tomamichel–Colbeck–Renner establish the duality and data processing of smooth entropies (arXiv:0907.5238). 2011–2012: Beaudry–Renner assemble these into the route formalized here.

Setting

All Hilbert spaces are finite-dimensional, and all logarithms are base 2. A density matrix is a positive semidefinite matrix of trace one; $S_=(\mathcal H)$ is their set and $S_\le(\mathcal H)$ is the set of subnormalized states (positive semidefinite, trace at most one). A state on $\mathcal H_A\otimes\mathcal H_B$ is written $\rho_{AB}$, and its marginal $\rho_B=\operatorname{Tr}_A\rho_{AB}$. The von Neumann entropy is $H(A)_\rho=-\operatorname{Tr}\rho_A\log\rho_A$ and the conditional entropy $H(A|B)_\rho=H(AB)_\rho-H(B)_\rho$.

The min-entropy of $A$ conditioned on $B$ is

The purified distance between subnormalized states is $P(\rho,\sigma)=\sqrt{1-\bar F(\rho,\sigma)^2}$, where $\bar F(\rho,\sigma)=\|\sqrt\rho\sqrt\sigma\|_1+\sqrt{(1-\operatorname{Tr}\rho)(1-\operatorname{Tr}\sigma)}$ is the generalized fidelity. The smooth min-entropy maximizes the min-entropy over the ball $\mathcal B^\varepsilon(\rho)=\{\rho'\in S_\le : P(\rho,\rho')\le\varepsilon\}$:

For $n$ independent copies, $\rho^{\otimes n}$ is a state on $A^n\otimes B^n$. The non-conditional entropies $H_{\min}(A)_\rho=-\log\|\rho\|_\infty$, $H_0(A)_\rho=\log\operatorname{rank}\rho$ and $H_\alpha(A)_\rho=\frac{1}{1-\alpha}\log\operatorname{Tr}\rho^\alpha$, and their smoothings over the same ball, appear in the intermediate lemmas.

Formalization targets

Goal: the von Neumann entropy DPI (Theorem 3)

The goal is the existing Open platform theorem QAlgorithms.Papers.Independent.Gap48.P20.strongSubadditivity, which states $0\le H(CB)+H(RB)-H(B)-H(CRB)$ for every density matrix on $C\otimes R\otimes B$; with $A\mapsto C$, $C\mapsto R$ this is exactly $H(ABC)+H(B)\le H(AB)+H(BC)$, the expanded form of the inequality above. It is referenced, not restated.

The smooth min-entropy DPI (Theorem 1)

The QAEP (Theorem 2)

split into the lower bound (Lemma 4.1) and the upper bound (Lemma 4.2). The milestones below them are the paper's own lemmas: monotonicity of the purified distance (Lemma A.1), Uhlmann's theorem (Theorem A.1, an existing Open platform theorem), the chain rule (Lemma 5.1), the Rényi lower bound (Lemma 5.2), the limit $\alpha\to1$ of Rényi entropies (Lemma B.2), the non-conditional QAEP for $H^\varepsilon_{\min}$ and $H^\varepsilon_0$ (Lemmas 5.4, 5.5), the bound by a nearby conditional entropy (Lemma 5.6), the eigenvalue-alignment bound (Lemma A.2) and the almost-i.i.d. limit (Lemma B.1).

Significance

The DPI for the von Neumann entropy is the single most used inequality in quantum information theory, and strong subadditivity is the structural fact behind it. A machine-checked proof of it is a prerequisite for formalizing essentially any converse theorem of quantum Shannon theory. The QAEP, a milestone here, is independently the bridge between one-shot and asymptotic information theory: it is what makes smooth entropies the right finite-blocklength replacements for the von Neumann entropy.

Both strong subadditivity and the QAEP are proved results; nothing in this mission is open mathematics. What the mission adds is a machine-checked route through one-shot entropies. The goal theorem is Open on the platform: it is posed but has no accepted proof. The milestones of this route, from the smooth min-entropy DPI to the QAEP, are not formalized anywhere on the platform. A completed development would also leave reusable pieces: monotonicity of the purified distance, the chain rule for smooth entropies, and the i.i.d. limits of smooth entropies.

Difficulty

Theorem 1 is short once the purified distance is known to be monotone under trace non-increasing completely positive maps, and that monotonicity (Lemma A.1) is itself the first real obstacle, since it is a statement about the generalized fidelity of subnormalized states. The bulk of the work is the QAEP. Its lower half needs a chain rule that trades conditional for non-conditional entropies at the cost of tripling the smoothing parameter, then precise i.i.d. limits of the non-conditional smooth entropies. The upper half needs a continuity statement for the conditional entropy of states that are only close to $\rho^{\otimes n}$, uniform in $n$ after division by $n$. The tempting reading of the double limit as a single limit in $n$ at fixed $\varepsilon$ is stronger than what the paper proves; the inner limit's existence is not established there.

Formalization scope

States are complex matrices indexed by finite types; a bipartite state is a matrix on A × B, a tripartite one on A × (B × C) with B × C the conditioning system of $H(A|BC)$. The smooth conditional min-entropy, the purified distance, the generalized fidelity, the conditional entropy $H(A|B)$ and the grouped tensor power $\rho^{\otimes n}$ on $A^nB^n$ are the published definitions QAlgorithms_Papers_Independent_Information100_P67; the Rényi entropy and $\operatorname{Tr}_C$ come from QAlgorithms_Papers_Independent_Dependency50_P35. Smooth entropies take values in the extended reals, so an empty ball gives $-\infty$ and a ball containing $0$ gives $+\infty$.

A local definitions module adds the non-conditional entropies $H_{\min}$, $H^\varepsilon_{\min}$, $H_0$, $H^\varepsilon_0$, trace non-increasing Kraus families, and the conditional entropy (36) of a subnormalized state $\tilde\rho$, $\frac{1}{\operatorname{Tr}\tilde\rho}\max_{\sigma_B}\operatorname{Tr}\tilde\rho(\log(\mathbb 1\otimes\sigma_B)-\log\tilde\rho)$, with the maximum taken over positive definite $\sigma_B$ so that Lean's convention $\log0=0$ cannot enter. The double limit $\lim_{\varepsilon\to0}\lim_{n\to\infty}$ is read through two predicates: "$L\le\lim\lim f$" means that for every $\delta>0$ there is $\varepsilon_0>0$ with $L-\delta\le f(\varepsilon,n)$ for all $\varepsilon\in(0,\varepsilon_0)$ and all large $n$, and "$\lim\lim f\le L$" is the mirror statement.

Trivializing encodings are ruled out: the smooth entropies are the published sup over the full subnormalized purified-distance ball, not free reals and not the ball $\{\rho\}$; $\varepsilon$ is quantified universally below $\varepsilon_0$ and is never allowed to depend on $n$; and the entropy of the nearby state in Lemma 5.6 is (36), not $H(AB)-H(B)$.

The paper's Lemma 5.3, (30), is false as printed and is not posed: at $\varepsilon=0$ it states $H_0\le H_\alpha$ for $\alpha<1$, the reverse of Rényi monotonicity, and $\rho=\operatorname{diag}(0.9,0.1)$, $\alpha=3/4$, $\varepsilon=0.1$ gives $1>0.8637$. Lemma 5.5, which its proof serves, is true and is a milestone. Uhlmann's theorem (Theorem A.1) is the existing Open platform theorem Claimed50.P12.lemmaB_3.

Contributions of any milestone are welcome. The purified-distance monotonicity and the Rényi-limit lemmas are reusable well beyond this paper.

Selected references

• N. J. Beaudry and R. Renner, An intuitive proof of the data processing inequality, Quantum Inf. Comput. 12 (2012) 432–441. https://arxiv.org/abs/1107.0740v2
• E. H. Lieb and M. B. Ruskai, Proof of the strong subadditivity of quantum-mechanical entropy, J. Math. Phys. 14 (1973) 1938–1941. https://doi.org/10.1063/1.1666274
• M. Tomamichel, R. Colbeck and R. Renner, A fully quantum asymptotic equipartition property, IEEE Trans. Inf. Theory 55 (2009) 5840–5847. https://arxiv.org/abs/0811.1221
• M. Tomamichel, R. Colbeck and R. Renner, Duality between smooth min- and max-entropies, IEEE Trans. Inf. Theory 56 (2010) 4674–4681. https://arxiv.org/abs/0907.5238
• B. Schumacher, Quantum coding, Phys. Rev. A 51 (1995) 2738–2747. https://doi.org/10.1103/PhysRevA.51.2738