Missions · Prove2Me

Mathematical Physics Quantum Information·Captain: mikedeng1

Entangling operations and their implementation using a small amount of entanglement: The Gate exp(−i(π/2^N)σx⊗σx) Is Implemented with Unit Probability Using α_N f_N < 5.97932·α_N Ebits on AverageResearch Paper

Motivation

A two-qubit gate whose qubits sit in different laboratories cannot be applied by local operations and classical communication (LOCC) alone: it can create entanglement, so it must consume some. The basic question of distributed quantum computation is how much. The textbook answer, teleporting one qubit to the other side, applying the gate and teleporting back, costs two ebits (maximally entangled pairs) whatever the gate. For gates close to the identity this is wasteful: a gate that can only create a small amount of entanglement should not need two ebits to implement.

J. I. Cirac, W. Dür, B. Kraus and M. Lewenstein (arXiv:quant-ph/0007057v1, published as Phys. Rev. Lett. 86, 544 (2001)) answered this for the family of phase gates $U(\alpha)=e^{-i\alpha\,\sigma_x\otimes\sigma_x}$ with binary phases $\alpha_N=\pi/2^N$ , the gates of the quantum Fourier transform. Their protocol implements $U(\alpha_N)$ exactly, with probability one, using on average an amount of entanglement proportional to $\alpha_N$ and about two classical bits in each direction. Shortly before, Eisert, Jacobs, Papadopoulos and Plenio had shown that one ebit and two classical bits suffice for a controlled-NOT (arXiv:quant-ph/0005101); Cirac et al. showed that the cost can go to zero with the gate's phase.

Setting

Six quantum systems are involved: $A_1,A_2,A_3$ on Alice's side and $B_1,B_2,B_3$ on Bob's, each of dimension $d$ with computational basis $\{|i\rangle\}$ . Let $|\Phi\rangle=d^{-1/2}\sum_i|i\rangle|i\rangle$ and $P=|\Phi\rangle\langle\Phi|$ . A completely positive map $\mathcal E(\rho)=\sum_kO_k\rho O_k^\dagger$ on $A_1B_1$ has the operator

E_{A_1A_2,B_1B_2}=\mathcal E(P_{A_1A_2}\otimes P_{B_1B_2}),

$\mathcal E$ acting as the identity on $A_2B_2$ . The map is recovered from $E$ by a joint projection of $A_2A_3$ and $B_2B_3$ onto $|\Phi\rangle$ : $\mathcal E(\rho)=d^4\operatorname{tr}_{A_2A_3B_2B_3}(E\,\rho_{A_3B_3}P_{A_2A_3}P_{B_2B_3})$ .

From now on $d=2$ . Let $\sigma_x,\sigma_y,\sigma_z$ be the Pauli matrices, $\alpha_N=\pi/2^N$ and $U(\alpha)=e^{-i\alpha\,\sigma_x^{A_1}\otimes\sigma_x^{B_1}}$ . The resource state is

|\psi_\beta\rangle=\cos\beta\,|\Phi^+\rangle_{A_1A_2}|\Phi^+\rangle_{B_1B_2}-i\sin\beta\,|\Psi^+\rangle_{A_1A_2}|\Psi^+\rangle_{B_1B_2},

One step with resource $|\psi_\beta\rangle$ : Alice measures $A_2A_3$ and Bob measures $B_2B_3$ in the Bell basis $|\Psi_{i_1,i_2}\rangle=(\mathbb 1\otimes\sigma_{i_1,i_2})|\Phi\rangle$ , with $\sigma_{1,1}=\mathbb 1$ , $\sigma_{1,2}=\sigma_x$ , $\sigma_{2,1}=\sigma_y$ , $\sigma_{2,2}=\sigma_z$ , and each applies the Pauli operator of the outcome to $A_1$ or $B_1$ . The step succeeds when $i_1=j_1$ . The protocol for $U(\alpha_N)$ acts on an input on $A_3B_3$ and leaves the output on $A_1B_1$ : step $k$ uses $|\psi_{2^{k-1}\alpha_N}\rangle$ , and the protocol stops at the first success or after step $N$ . With $p_k$ the probability that step $k$ is performed, the average entanglement consumed is $\bar E[U(\alpha_N)]=\sum_kp_k\,E(\psi_{2^{k-1}\alpha_N})$ .

Formalization targets

Goal: unit probability at cost $\alpha_Nf_N$

For every $N\ge1$ :

every terminal branch of the protocol applies $U(\alpha_N)$ up to a scalar, and the branch operators $K_l$ satisfy $\sum_lK_l^\dagger K_l=\mathbb 1$ ;
on every input state, step $k$ is performed with probability $(1/2)^{k-1}$ , and

\bar E[U(\alpha_N)]=\alpha_Nf_N,\qquad f_N=\frac1\pi\sum_{k=1}^N2^kE(\psi_{\alpha_k});

the average classical communication in each direction is $2-(1/2)^{N-2}$ bits;
$f_N<f_\infty=\frac1\pi\sum_{k\ge1}2^kE(\psi_{\alpha_k})$ , the series converges, and

5.97931<f_\infty<5.97932.

Milestones

In the order of the paper: the transpose identity (7) and the reconstruction (6)/(8) for general $d$ ; the operator of $U(\alpha)$ (10); the step-outcome rule (each outcome has probability $1/16$ ; the step applies $U(\beta)$ if $i_1=j_1$ and $U(-\beta)$ otherwise); the accumulation of failures, $U(-\alpha_N)^{2^N-1}=-U(\alpha_N)$ ; the entropy formula $E(\psi_\alpha)=h(\cos^2\alpha)$ (11); the cost identity (12); and the bounds (13).

Significance

The result shows that the entanglement needed to implement a nonlocal gate is not a fixed quantum of two ebits but can scale with the gate: $\bar E<5.97932\,\alpha_N$ ebits for $U(\alpha_N)$ . Through composition of binary phases it bounds the cost of an arbitrary phase gate by $f_\infty\alpha$ , and through the paper's infinitesimal argument it relates the cost of any two-qubit unitary to its nonlocal parameters; these extensions are not part of this mission. The operator–map correspondence (6)–(8), a bipartite form of the Jamiołkowski isomorphism, is the general mechanism for implementing a map from a resource state, and it is reusable well beyond this protocol.

The paper's arguments are short calculations, presented as "one can readily see". The mission makes every one of them explicit: the Bell-basis contraction, the Pauli corrections, the phase bookkeeping across $N$ steps, the probability of each branch, and the numerical value of $f_\infty$ . In checking the statements, two points needed repair. The printed value $f_\infty=5.97932$ is not the value: $f_\infty=5.9793137\ldots$ , so the goal poses $5.97931<f_\infty<5.97932$ , which keeps the paper's usable bound. And footnote [20]'s step count is off by one: the local step $U(\pi/2)$ is step $N$ , and the printed communication $2-(1/2)^{N-2}$ is the sum of $p_k$ over steps $1,\dots,N-1$ . No machine-checked proof of any of these statements is known to exist.

Difficulty

Each step is a contraction of a 64-dimensional state with two Bell vectors and two Pauli corrections; the claimed rule ( $U(\beta)$ if $i_1=j_1$ , $U(-\beta)$ otherwise, always with amplitude of modulus $1/4$ ) must be verified on all 16 outcomes, and it holds only for the right reading of the Bell basis. The multi-step statement needs an invariant over histories of arbitrary length: after $k$ failures the applied operator is a scalar multiple of $U(-\alpha_N)^{2^k-1}$ , and the step- $(k+1)$ resource $U(2^k\alpha_N)$ exactly undoes it on success. The cost identity (12) is a reindexing of a finite sum, but the bound (13) is not: it needs the convergence of $\sum2^kh(\cos^2(\pi/2^k))$ (the terms behave like $2^k\cdot(\pi/2^k)^2\log(2^k)$ ) and a certified numerical enclosure of the sum to within $10^{-5}$ , including a bound on the tail. A floating-point evaluation is not a proof.

Formalization scope

Systems are indexed from $0$ : Pauli labels are Fin 2 × Fin 2 with $(0,0),(0,1),(1,0),(1,1)$ for $\mathbb 1,\sigma_x,\sigma_y,\sigma_z$ , and the paper's step $k$ is list position $k-1$ . Operators on several systems are matrices over product index types in Mathlib's Kronecker convention; the resource is indexed $((a_1,a_2),(b_1,b_2))$ , so the published partial trace WildeQIT.partialTraceRight takes the cut $(A_1A_2)|(B_1B_2)$ . The gate is Mathlib's matrix exponential. Entropies are QAlgorithms.vnEntropy, in bits, and the binary entropy is WildeQIT.binaryEntropy. A protocol branch is a Kraus operator from $A_3B_3$ to $A_1B_1$ ; probabilities are $\operatorname{Re}\operatorname{Tr}(K\rho K^\dagger)$ on density matrices. $f_\infty$ is a tsum, and every statement about it asserts summability. The undefined $|\Psi\rangle$ of the Bell basis is read as $|\Phi\rangle$ of Eq. (5), the only reading under which the step rule holds.

The protocol is not defined through its conclusion: the step operators are the literal contractions of the resource with the Bell vectors, success is the label condition $i_1=j_1$ , the resource is the printed formula (10) rather than $U\otimes\mathbb 1$ applied to $|\Phi^+\rangle|\Phi^+\rangle$ , the entropy is computed from the reduced state, and the step probabilities are computed from the operators rather than set to $(1/2)^{k-1}$ . A formalization that defines any of these by the property to be proved, or drops the summability of $f_\infty$ , trivializes the mission.

A complete development needs Pauli and Kronecker-product algebra, the closed form $U(\alpha)=\cos\alpha\,\mathbb 1-i\sin\alpha\,\sigma_x\otimes\sigma_x$ of the exponential, the spectrum of a rank-two reduced state, induction over protocol histories, and certified bounds on $\cos$ and $\log_2$ for the numerical clause. The operator–map identities (6)–(8) and a verified evaluation of $f_\infty$ are reusable independently. Contributions to any milestone are welcome.

Selected references

J. I. Cirac, W. Dür, B. Kraus, M. Lewenstein, Entangling operations and their implementation using a small amount of entanglement, arXiv:quant-ph/0007057v1, 2000; Phys. Rev. Lett. 86, 544 (2001). https://arxiv.org/abs/quant-ph/0007057v1
J. Eisert, K. Jacobs, P. Papadopoulos, M. B. Plenio, Optimal local implementation of nonlocal quantum gates, Phys. Rev. A 62, 052317 (2000). https://arxiv.org/abs/quant-ph/0005101
A. Jamiołkowski, Linear transformations which preserve trace and positive semidefiniteness of operators, Rep. Math. Phys. 3, 275 (1972). https://doi.org/10.1016/0034-4877(72)90011-0

13 thms3 active usersReviewed

Completed

Markov Chain Operations Research Optimization+1·Captain: mikedeng1

Pricing and Optimization in Shared Vehicle Systems: An Approximation Framework: Elevated-Flow-Relaxation Prices Earn an m/(m+n−1) Fraction of the Optimal State-Dependent ObjectiveResearch Paper

Motivation

Bike-sharing and car-sharing systems, and ride-hailing platforms, all move a fixed fleet of units between stations. Every ride takes a unit away from its origin and leaves it at its destination, so demand that is unbalanced across stations drains some stations and floods others. Pricing is the main lever an operator has: raising the price of rides out of a depleted station throttles the outflow. Choosing such prices optimally is hard, because the optimal policy may react to the full system state, a placement of $m$ units over $n$ stations, of which there are $\binom{m+n-1}{n-1}$ .

Banerjee, Freund and Lykouris (arXiv:1608.06819v4, Operations Research 2022) give an approximation framework for this control problem. Their first result, Theorem 15, shows that one convex program yields state-independent prices whose steady-state performance is within a factor $m/(m+n-1)$ of the best state-dependent policy. The guarantee holds simultaneously for throughput, social welfare and revenue under regular demand.

Timeline. Gordon and Newell (1967) gave the product-form stationary law of closed queueing networks. Whitt (1984) observed that balanced closed networks give every node availability $m/(m+n-1)$ . George and Xia (2011) studied availability in vehicle-rental networks via closed queueing networks. Waserhole and Jost (2014) proved the $m/(m+n-1)$ guarantee for throughput. Banerjee, Freund and Lykouris extended it to concave reward curves, and to travel times and other controls.

Setting

There are $n$ nodes and $m$ units. A state is $x\in S_{n,m}=\{x\in\mathbb N_0^n:\sum_ix_i=m\}$ . Customers wishing to travel from $i$ to $j$ arrive at node $i$ at rate $\varphi_{ij}\ge0$ . A quantile $q_{ij}\in[0,1]$ is the fraction of them willing to pay the quoted price. A customer who accepts engages a unit at $i$ if one is present, moving the system from $x$ to $x-e_i+e_j$ .

A state-dependent policy chooses quantiles $q_{ij}(x)\in[0,1]$ at every state, with $q_{ij}(x)=0$ when $x_i=0$ . A stationary law $\pi$ is a probability vector on $S_{n,m}$ satisfying the balance equation (1):

\pi(x)\sum_{i,j}\varphi_{ij}q_{ij}(x)=\sum_{i,j}\pi(x+e_i-e_j)\varphi_{ij}q_{ij}(x+e_i-e_j).

Rewards are given by per-ride rewards $I_{ij}$ , functions of the quantile, with reward curves $R_{ij}(q)=q\,I_{ij}(q)$ . The steady-state objective (2) is

\mathrm{Obj}_m(q)=\sum_{x\in S_{n,m}}\pi(x)\sum_{i,j}\varphi_{ij}R_{ij}(q_{ij}(x)),

and $\mathrm{Opt}_m$ is its best value over all state-dependent policies and their stationary laws.

The elevated flow relaxation (Algorithm 1) drops availability from the objective and adds a flow-conservation constraint:

\max_q\ \widehat{\mathrm{Obj}}(q)=\sum_{i,j}\varphi_{ij}R_{ij}(q_{ij})\quad\text{s.t.}\quad\sum_k\varphi_{ki}q_{ki}=\sum_j\varphi_{ij}q_{ij}\ \forall i,\qquad q\in[0,1]^{n\times n}.

A feasible $q$ has balanced demand. Its optimum $\tilde q$ is then quoted as a fixed price at every non-empty station.

Formalization targets

Goal: Theorem 15

If every $R_{ij}$ is concave on $[0,1]$ , $\tilde q$ is an optimal solution of Algorithm 1 whose support graph $\{(a,b):a\ne b,\ \varphi_{ab}\tilde q_{ab}>0\}$ is strongly connected, and $\tilde\pi$ is a stationary law of $\tilde q$ , then for every state-dependent policy $q$ and every stationary law $\pi$ of it,

\mathrm{Obj}_m(\tilde q)\ \ge\ \frac{m}{m+n-1}\,\mathrm{Obj}_m(q),\qquad\text{i.e.}\qquad \mathrm{Obj}_m(\tilde q)\ge\frac{m}{m+n-1}\mathrm{Opt}_m.

The connectivity hypothesis is the paper's standing irreducibility assumption, and the printed statement is false without it.

Milestones

These follow the paper's own sequence:

Propositions 7 and 8 (demand bounding, supply circulation);
Lemma 9, $\widehat{\mathrm{Obj}}(\tilde q)\ge\mathrm{Opt}_m$ ;
the reduction of a state-independent policy to a Gordon–Newell network (§2.3) and the Gordon–Newell theorem (Theorem 2, an already proved platform theorem);
Lemma 3, availability in product-form networks;
Lemma 13, a weighted bipartite graph between $S_{n,m}$ and $S_{n,m-1}$ ;
Lemma 14, $A_m=r_{\max}G_{m-1}/G_m\ge m/(m+n-1)$ ;
Proposition 6, infinite-unit availabilities $r_i/\max_jr_j$ ;
Lemma 10, equal availabilities under balanced demand;
Lemma 11, $\mathrm{Obj}_\infty=\widehat{\mathrm{Obj}}$ ;
Lemma 12, $\mathrm{Obj}_m=A_m\,\mathrm{Obj}_\infty$ .

Significance

The result. Theorem 15 turns an exponentially large control problem into a convex program with $n^2$ variables and a guarantee that does not depend on the arrival rates. The factor $m/(m+n-1)$ tends to $1$ as the fleet grows relative to the number of stations. The same framework gives the paper's later results on travel times, rebalancing and constrained pricing. In those settings the balanced-demand shortcut is unavailable and the infinite-unit comparison (Lemmas 12 and 14) carries the argument.

Formalizing it. The theorem is proved in the paper; nothing here is open. The mission produces a machine-checked version and a reusable layer: stationarity of finite-state rate-based chains via balance equations, the identification of state-independent pricing with Gordon–Newell networks, and availability identities for product-form laws. The Gordon–Newell product form itself is already proved on the platform and is referenced, not restated. No result of this paper had a machine-checked proof on the platform when the mission was drafted.

Difficulty

The comparison is against state-dependent policies, which can be reducible and have many stationary laws. Lemma 9 must hold for every one of them, so no product form is available on that side: only the balance equations are.

On the other side, the availability of a state-independent policy depends on the traffic intensities in a way that has no closed form for finite $m$ , and the bound $m/(m+n-1)$ must hold uniformly over all of them.

A natural first idea is to compare $\tilde q$ directly with the averaged quantiles of the optimal policy. That idea fails: averaging ignores availability, which is exactly the loss being bounded.

Finally, identifying the stationary law of $\tilde q$ with the uniform law uses irreducibility, which must be derived from the connectivity hypothesis.

Formalization scope

Nodes are Fin n, so the paper's node $i$ is index $i-1$ . States reuse the closed-network vocabulary of the platform (states, moveState, productForm, normConst, tailMarginal). Laws are real functions on $\mathbb N^n$ that vanish off $S_{n,m}$ .

Decisions and rewards.

Decision variables are quantiles. Value distributions and prices do not appear, and $I_{ij}$ is any real function of the quantile.
$R_{ij}(q):=q\,I_{ij}(q)$ , so $R_{ij}(0)=0$ . Concavity is required on $[0,1]$ only.
A state-independent $q$ enters the $m$ -unit system as the policy $x\mapsto q_{ij}\mathbf 1\{x_i>0\}$ .

Stationarity and the optimum.

Stationarity is the balance equation (1) plus nonnegativity, vanishing off $S_{n,m}$ and total mass $1$ . Without the total mass, the zero function would satisfy (1).
$\mathrm{Opt}_m$ is never a supremum: the goal quantifies over every policy and every stationary law, so no junk value of sSup can enter.
Policies must vanish at empty stations, so no ride is counted from a station without units.

Ratios and traffic.

Ratios are stated as products, e.g. $\mathrm{Obj}_m=A_m\,\mathrm{Obj}_\infty$ , so there is no division by an objective.
Traffic intensities are solutions of $\sum_jr_j\varphi_{ji}q_{ji}=r_i\sum_k\varphi_{ik}q_{ik}$ .

The milestones that depend on connectivity (Proposition 6, Lemmas 10 and 11) state it as a hypothesis, as the goal does.

The needed infrastructure is finite sums over $S_{n,m}$ , Jensen's inequality for concave functions on $[0,1]$ , and the bridge from the balance equation to the closed-network steady state. Proofs of any milestone, and alternative proofs of the bridge, are welcome.

Selected references

S. Banerjee, D. Freund, T. Lykouris, Pricing and Optimization in Shared Vehicle Systems: An Approximation Framework, Operations Research 70(3), 2022; arXiv:1608.06819v4. https://arxiv.org/abs/1608.06819
W. J. Gordon, G. F. Newell, Closed Queuing Systems with Exponential Servers, Operations Research 15(2), 1967. https://doi.org/10.1287/opre.15.2.254
D. K. George, C. H. Xia, Fleet-sizing and service availability for a vehicle rental system via closed queueing networks, European Journal of Operational Research 211(1), 2011. https://doi.org/10.1016/j.ejor.2010.12.015
A. Waserhole, V. Jost, Pricing in vehicle sharing systems: optimization in queuing networks with product forms, EURO Journal on Transportation and Logistics 5(3), 2016. https://doi.org/10.1007/s13676-014-0054-4
R. Serfozo, Introduction to Stochastic Networks, Springer, 1999. https://doi.org/10.1007/978-1-4612-1482-3

15 thms3 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: mikedeng1

M-Convex Function Minimization Under L1-Distance Constraint and Its Application to Dock Reallocation in Bike-Sharing System: Steepest Descent from the Center Is Optimal at Every L1 RadiusResearch Paper

Motivation

Bike-sharing operators periodically move docks between stations: a station that often runs out of bikes or of open docks frustrates users, but every moved dock costs money. Freund, Henderson and Shmoys modelled this dock re-allocation problem as a separable nonlinear integer program with a budget on the number of moved docks (Freund–Henderson–Shmoys, IPCO 2017). Shioura observed that, after a change of variables, the objective is an M-convex function and the budget is an $\ell_1$ -ball around the current allocation, and studied the resulting problem in general (Shioura, arXiv:1809.03126).

M-convex functions are the discrete analogue of convex functions on the integer points of a hyperplane, introduced by Murota (Murota, Adv. Math. 1996; Murota, Discrete Convex Analysis, SIAM 2003). Their unconstrained minimization is well understood: a local minimum with respect to single exchanges $x \mapsto x + \chi_i - \chi_j$ is global, and steepest descent converges. Adding an $\ell_1$ -distance constraint breaks the M-convex structure of the feasible region, and whether the exchange method survives such a constraint is the question this mission formalizes.

Setting

Let $V$ be a finite set (the stations), and write $x(V) = \sum_{v \in V} x(v)$ for $x \in \mathbb Z^V$ , $\chi_i$ for the $i$ -th unit vector, $\chi_0 = \mathbf 0$ , $\mathrm{supp}^+(z) = \{v \mid z(v) > 0\}$ , $\mathrm{supp}^-(z) = \{v \mid z(v) < 0\}$ and $\|z\|_1 = \sum_v |z(v)|$ . For $f : \mathbb Z^V \to \mathbb R \cup \{+\infty\}$ , the effective domain is $\operatorname{dom} f = \{x \mid f(x) < +\infty\}$ . The function $f$ is M $^\natural$ -convex if

\forall x, y \in \operatorname{dom} f,\ \forall i \in \mathrm{supp}^+(x - y),\ \exists j \in \mathrm{supp}^-(x - y) \cup \{0\}:\ f(x) + f(y) \ge f(x - \chi_i + \chi_j) + f(y + \chi_i - \chi_j),

and M-convex if, in addition, $\operatorname{dom} f \subseteq \{x \mid x(V) = \theta\}$ for some $\theta \in \mathbb Z$ .

Fix an M-convex $f$ with bounded $\operatorname{dom} f$ and a center $x_c$ with $x_c(V) = \theta$ ; the center need not lie in $\operatorname{dom} f$ . For $k \in \mathbb Z_+$ the problem

(\mathrm{MML1}(k))\qquad \min\{ f(x) \mid x \in \operatorname{dom} f,\ \|x - x_c\|_1 \le 2k \}

has optimal set $M_k$ . Put $2\sigma = \min\{\|x - x_c\|_1 \mid x \in \operatorname{dom} f\}$ (the radius at which the problem becomes feasible) and $2\tau = \min\{\|x - x_c\|_1 \mid x \in \arg\min f\}$ (the radius at which the constraint stops binding). For a budget $\gamma \ge \sigma$ , the problem (MML1) is (MML1( $\gamma$ )).

Algorithm SteepestDescentMML1 (p. 8): choose $x_\sigma \in M_\sigma$ ; for $k = \sigma + 1, \dots, \gamma$ set $x_k = x_{k-1} + \chi_{i_k} - \chi_{j_k}$ , where $(i_k, j_k) \in V \times V$ minimizes $f(x_{k-1} + \chi_i - \chi_j)$ over all pairs; output $x_\gamma$ .

Formalization targets

Goal: Theorem 4.2

Every run of SteepestDescentMML1, with any choice in Step 0 and any tie-breaking, satisfies

x_k \in M_k \quad (\sigma \le k \le \gamma), \qquad\text{in particular } x_\gamma \in M_\gamma .

The goal fixes no constant and covers every M-convex $f$ with bounded domain, every center on the hyperplane, and every budget $\gamma \ge \sigma$ .

Milestones

(M-EXC) (§2.1, p. 4): $f$ is M-convex if and only if $\forall x, y \in \operatorname{dom} f,\ \forall i \in \mathrm{supp}^+(x - y),\ \exists j \in \mathrm{supp}^-(x - y)$ with the exchange inequality.
Lemma A.1 (p. 16): if $y \ne \tilde y$ , $y(V) = \tilde y(V)$ and $\|y - x_c\|_1 \le \|\tilde y - x_c\|_1$ , then $\tilde y$ exceeds $x_c$ somewhere on $\mathrm{supp}^+(\tilde y - y)$ or falls below it somewhere on $\mathrm{supp}^-(\tilde y - y)$ .
Lemma A.2 (p. 16): $\|x - z\|_1 + \|y - z\|_1 \ge \|(x - \chi_i + \chi_j) - z\|_1 + \|(y + \chi_i - \chi_j) - z\|_1$ for $i \in \mathrm{supp}^+(x - y)$ , $j \in \mathrm{supp}^-(x - y)$ .
Lemma A.3 (p. 17): from $y \in \operatorname{dom} f$ with $\|y - x_c\|_1 < 2\tau$ there is a monotone sequence with strictly decreasing values to the point of $M_\tau$ nearest to $y$ .
Theorem 4.1 (p. 8): (i) $\mu_\sigma > \mu_{\sigma+1} > \cdots > \mu_\tau$ and $M_k \subseteq \{\|x - x_c\|_1 = 2k\}$ for $k \in [\sigma, \tau]$ ; (ii) every $y \in M_k$ has a neighbour $y + \chi_i - \chi_j \in M_{k+1}$ with $i \notin \mathrm{supp}^-(y - x_c)$ , $j \notin \mathrm{supp}^+(y - x_c)$ ; (iii) every $y \in M_{k+1}$ has a neighbour $y - \chi_i + \chi_j \in M_k$ with $i \in \mathrm{supp}^+(y - x_c)$ , $j \in \mathrm{supp}^-(y - x_c)$ , for $k \in [\sigma, \tau - 1]$ .

Significance

Theorem 4.2 gives a pseudo-polynomial algorithm for (MML1): after the initial point, it needs $\gamma - \sigma$ rounds of $|V|^2$ function evaluations. It is also a structural statement: the greedy path from the center passes through an optimum at every radius simultaneously, so a single run answers the whole family of budget questions $k = \sigma, \dots, \gamma$ , which is what an operator comparing budgets needs. Theorem 4.1 underlies the paper's polynomial-time proximity and scaling algorithms (§5) and its fast algorithm for dock re-allocation (§6).

The result is proved in the paper; nothing here is open mathematics. No part of it is formalized: the platform has M-convex vocabulary and unconstrained steepest descent bounds from Murota's book, but nothing about $\ell_1$ -constrained minimization, the sets $M_k$ , or steepest descent under a distance constraint. The mission produces a machine-checked proof of the algorithm's correctness, including the case of an infeasible center and budgets beyond $\tau$ , which the printed theorem sets aside.

Difficulty

The feasible region of (MML1( $k$ )) is not M-convex, so the classical optimality criterion for M-convex functions does not apply to it directly, and a local optimum of the constrained problem need not be global. The obvious induction, "a steepest step from an optimum at radius $2k$ lands at an optimum at radius $2(k+1)$ ", requires knowing that some optimum at radius $2(k+1)$ is a single exchange away and that its exchange moves away from the center; that is Theorem 4.1 (ii), whose proof rests on the strict monotonicity of the optimal values and on the tightness of the constraint (Theorem 4.1 (i)), which in turn rests on constructing strictly decreasing exchange paths towards a nearest minimizer (Lemma A.3). The bookkeeping of $\ell_1$ distances along such paths, which change by $-2$ , $0$ or $+2$ per step, is the delicate part.

Formalization scope

Vectors are V → ℤ over a finite type V with decidable equality (no lower bound on $|V|$ ); values are WithTop ℝ, with $+\infty = \top$ ; $\|x - y\|_1$ is the natural number L1Dist x y. M-convexity is the paper's definition, (M $^\natural$ -EXC) plus the hyperplane condition, using the published MNatExchangeAxiom; it is not defined through (M-EXC), whose equivalence is a milestone. The hyperplane condition through the center is the hypothesis $\forall x \in \operatorname{dom} f,\ x(V) = x_c(V)$ ; $x_c \in \operatorname{dom} f$ is not assumed. $\sigma$ and $\tau$ are natural numbers given by IsLeast hypotheses on the doubled minima. $M_k$ is a set defined from $f$ , $x_c$ and $k$ , and the optimal value $\mu_k$ is never a separate real number: Theorem 4.1 (i) asserts $M_k \ne \emptyset$ and compares values of $f$ on consecutive sets. A run is a sequence x : ℕ → V → ℤ satisfying Step 0 and Steps 2–3, with all pairs $(i, j)$ , $i = j$ included, admissible in Step 2.

The goal is not vacuous: the run hypothesis is satisfiable whenever $\operatorname{dom} f \ne \emptyset$ (the minima over the finite sets $V \times V$ exist and $M_\sigma \ne \emptyset$ ), and a sanity file exhibits an instance with an explicit run. The paper's standing assumption $\tau > \gamma$ is dropped; the goal therefore also covers budgets past the nearest minimizer.

A complete development needs the M-convex exchange calculus (the (M-EXC) equivalence and its use with $\ell_1$ distances), which is reusable for any M-convex problem with a distance or budget constraint. Proofs of the milestones in any order are welcome, as are alternative proofs of Theorem 4.1.

Selected references

A. Shioura, M-convex Function Minimization Under L1-Distance Constraint (published as M-Convex Function Minimization Under L1-Distance Constraint and Its Application to Dock Reallocation in Bike-Sharing System, Mathematics of Operations Research, 2022), arXiv:1809.03126v3, 2018. https://arxiv.org/abs/1809.03126
D. Freund, S. G. Henderson, D. B. Shmoys, Minimizing multimodular functions and allocating capacity in bike-sharing systems, Proc. 19th IPCO, LNCS 10328, 2017. https://arxiv.org/abs/1611.09304
K. Murota, Discrete Convex Analysis, SIAM, 2003. https://doi.org/10.1137/1.9780898718508
K. Murota, Convexity and Steinitz's exchange property, Advances in Mathematics 124:272–311, 1996. https://doi.org/10.1006/aima.1996.0084
K. Murota, On steepest descent algorithms for discrete convex functions, SIAM Journal on Optimization 14:699–707, 2003. https://doi.org/10.1137/S1052623402419005

17 thms3 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics Linear Optimization+1·Captain: mikedeng1

On the Set of Balanced Games: The Polytope of Nonnegative Balanced Games Is Combinatorial and Its Adjacency Graph Is Hamilton-ConnectedResearch Paper

Motivation

A cooperative game with transferable utility (a TU-game) assigns to every coalition of players a number, the worth that coalition can secure on its own. The central allocation concept is the core, introduced by Gillies (1953): the payment vectors that distribute exactly the worth of the grand coalition while giving every coalition at least its worth. The core may be empty. Bondareva (1963) and Shapley (1967) characterized the games with a nonempty core as the balanced games, through a finite family of linear inequalities indexed by minimal balanced collections. The set of balanced games is therefore a polyhedron, and Garcia-Segador, Grabisch and Miranda (arXiv:2501.14341) study its geometry: its lineality space, extremal rays and facets, and those of two of its sections.

The motivation given in the paper is a projection problem: finding the balanced game closest to a non-balanced one would give a new solution concept for games with an empty core, and an orthogonal projection onto a polyhedron needs a detailed description of that polyhedron. Games are set functions vanishing on the empty set, so the same objects appear in decision theory (capacities), voting theory (simple games) and combinatorial optimization (polymatroid rank functions).

This mission concerns the third section studied in the paper: the nonnegative balanced games normalized by $v(N)=1$ . This set is a polytope, and the paper shows that it is a combinatorial polytope in the sense of Naddef and Pulleyblank (1981) and that its graph is Hamilton-connected.

Setting

Let $N=\{1,\dots,n\}$ be the set of players. A coalition is a subset $S\subseteq N$ , and a game is a function $v:2^N\to\mathbb R$ with $v(\varnothing)=0$ . Write $x(S)=\sum_{i\in S}x_i$ for $x\in\mathbb R^n$ . The core of $v$ is

C(v)=\{x\in\mathbb R^n : x(S)\ge v(S)\ \text{for all } S\subseteq N,\ x(N)=v(N)\},

and $v$ is balanced when $C(v)\ne\varnothing$ .

$\mathcal G_+(n)$ is the set of games with $v(S)\ge 0$ for every $S$ and $v(N)=1$ , and

\mathcal{BG}_+(n)=\{v\in\mathcal G_+(n) : v \text{ balanced}\}.

A vertex of $\mathcal{BG}_+(n)$ is an extreme point. Two distinct vertices are adjacent when the segment between them is an edge (a one-dimensional face). The adjacency graph has the vertices as nodes and the adjacent pairs as edges. For a vertex $v$ , its family is $\mathcal D(v)=\{S\ne\varnothing,N : v(S)=1\}$ ; conversely a family $\mathcal D$ of proper nonempty coalitions defines the game $v_{\mathcal D}$ equal to $1$ on $\mathcal D\cup\{N\}$ and $0$ elsewhere.

A polytope $P\subseteq\mathbb R^d$ is combinatorial (Definition 1) when all its vertices are 0-1-valued and, for any two distinct non-adjacent vertices $v_1,v_2$ , there are two other different vertices $v_3,v_4$ with $v_1+v_2=v_3+v_4$ . A graph is Hamilton-connected when every two distinct nodes are joined by a Hamiltonian path, and the hypercube $Q_d$ is the graph on $\{0,1\}^d$ whose edges join vectors at Hamming distance one.

Formalization targets

Goal: Theorem 12

\mathcal{BG}_+(n)\ \text{is a combinatorial polytope, and its adjacency graph is Hamilton-connected.}

Both clauses are part of the goal; the first includes that $\mathcal{BG}_+(n)$ is a polytope, since Definition 1 applies to polytopes. Hamilton-connectedness (a Hamiltonian path between every pair of distinct vertices) is stronger than having a Hamiltonian cycle.

Milestones

Theorem 1 (Bondareva–Shapley): $C(v)\ne\varnothing$ iff $v$ is balanced. Already proved on the platform.
Proposition 1: $\mathcal{BG}_+(n)$ is a $(2^n-2)$ -dimensional polytope.
Theorem 8: $v\in\mathcal G_+(n)$ is a vertex of $\mathcal{BG}_+(n)$ iff $v$ is balanced and 0-1-valued.
Theorem 9: for a family $\mathcal D\subseteq 2^N\setminus\{\varnothing,N\}$ , $v_{\mathcal D}$ is a vertex iff $\mathcal D=\varnothing$ or $\bigcap\mathcal D\ne\varnothing$ .
Lemma 5: distinct vertices $v_1,v_2$ are non-adjacent iff $v_1+v_2=v_3+v_4$ for vertices $v_3,v_4\notin\{v_1,v_2\}$ ; then $\mathcal D_3\cup\mathcal D_4=\mathcal D_1\cup\mathcal D_2$ and $\mathcal D_3\cap\mathcal D_4=\mathcal D_1\cap\mathcal D_2$ .
Theorem 11 (Naddef–Pulleyblank): the adjacency graph of a combinatorial polytope is a hypercube or Hamilton-connected.
Proof of Theorem 12: for $n\ge 2$ the adjacency graph of $\mathcal{BG}_+(n)$ is not a hypercube.

Significance

The result. The vertices of $\mathcal{BG}_+(n)$ are the balanced 0-1-valued games, and their number grows doubly exponentially in $n$ (Proposition 3 of the paper). Theorem 12 places this polytope in the class of combinatorial polytopes studied by Naddef and Pulleyblank, in which non-adjacency of two vertices is witnessed by a pairwise exchange $v_1+v_2=v_3+v_4$ . Hamilton-connectedness gives, between any two prescribed vertices, an ordering of all vertices in which consecutive vertices share an edge of the polytope, that is, a traversal of the whole vertex set by edge moves.

Formalizing it. The theorem is proved in the paper; no machine-checked proof exists. The mission produces formal definitions of the core-based balanced-game polytope, of the adjacency graph of a convex set, of hypercube graphs, of Hamilton-connectedness and of combinatorial polytopes. The Naddef–Pulleyblank theorem (Theorem 11) is cited in the paper without proof and is itself a substantial formalization target, reusable for every combinatorial polytope.

Difficulty

Three steps carry the weight. Theorem 11 is a graph-theoretic result about all combinatorial polytopes; its proof is not in this paper. Lemma 5 requires showing that non-adjacency of two vertices is witnessed by a single pair of other vertices with the same sum; a general non-adjacent pair only has its midpoint expressed as a convex combination of possibly many other vertices, and the printed proof starts from the two-vertex form, which is exactly what needs proving (the statement has been checked numerically for $n\le 4$ exhaustively and sampled for $n=5$ ). The non-hypercube step must rule out a graph isomorphism to any $Q_d$ , which the printed observation about $\hat\delta_{\{i\}}$ and $\hat\delta_{\{j\}}$ does not do by itself.

Formalization scope

Players are Fin n (0-based), coalitions are Finset (Fin n), and a game is a vector Finset (Fin n) → ℝ. The coordinate at $\varnothing$ is part of the vector and is fixed at $0$ by $\mathcal G_+(n)$ ; the paper's space $\mathbb R^{2^N\setminus\{\varnothing\}}$ is an affine copy, so vertices, edges, sums and dimension are unchanged. Balancedness is the nonemptiness of the core, using the published definition Supermodularity.Cooperative.Core; the paper's inequality description (4) is linked to it by Theorem 1. A polytope is the convex hull of a finite set. Vertices are extreme points, adjacency is the published Hirsch.Adj (distinct points whose segment is an extreme subset), a hypercube is a graph isomorphic to $Q_d$ for some $d\ge 0$ , and Hamilton-connected is stated with Mathlib's Walk.IsHamiltonian for every ordered pair of distinct vertices.

The goal is stated for every $n$ ; at $n=0$ the polytope is empty and every clause holds trivially. Proposition 1 and Theorem 9 keep the paper's $n\ge 1$ , and the non-hypercube step needs $n\ge 2$ ( $\mathcal{BG}_+(1)$ is one point, whose graph is $Q_0$ ).

Lemma 5's "In addition" clause is formalized for every pair of vertices $v_3,v_4$ with $v_1+v_2=v_3+v_4$ , the stronger of the two possible readings. The printed proof of Lemma 5 assumes a two-vertex representation of the midpoint, a gap a solver must close.

Vertices are never defined as balanced 0-1 games, and adjacency is never defined through the families $\mathcal D$ or the exchange condition: either choice would make Theorem 8 or Lemma 5 true by definition and empty the goal.

Contributions welcome: a proof of the Naddef–Pulleyblank theorem from Definition 1; facts about extreme points and faces of polytopes given as convex hulls; the vertex characterization via cores.

Selected references

P. Garcia-Segador, M. Grabisch, P. Miranda, On the set of balanced games, arXiv:2501.14341v1, 2025 (Mathematics of Operations Research, 2025). https://arxiv.org/abs/2501.14341
D. Naddef, W. R. Pulleyblank, Hamiltonicity and combinatorial polyhedra, Journal of Combinatorial Theory, Series B 31 (1981), 297–312.
O. Bondareva, Some applications of linear programming to the theory of cooperative games, Problemy Kibernetiki 10 (1963), 119–139 (in Russian).
L. S. Shapley, On balanced sets and cores, Naval Research Logistics Quarterly 14 (1967), 453–460.
D. Gillies, Some theorems on n-person games, PhD thesis, Princeton, 1953.
T. Matsui, S. Tamura, Adjacency on combinatorial polyhedra, Discrete Applied Mathematics 56 (1995), 311–321.

11 thms3 active usersReviewed

Completed

Linear algebra Machine Learning Statistics·Captain: mikedeng1

SYN-DIGITS: A Synthetic Control Framework for Calibrated Digital Twin Simulation: Error Bound for Ridge Fit-and-Transfer on a New QuestionResearch Paper

Motivation

Large language models are increasingly used as digital twins of survey respondents: a model is prompted with a persona and asked to answer the same questionnaire a human would. The appeal is cost and speed, since a new question can be "fielded" to thousands of simulated respondents in minutes. The obstacle is fidelity. Large language models exhibit systematic bias and miscalibration relative to real human behavior (Fan, Huang, Peng, Wang, Wu, 2026).

SYN-DIGITS proposes to calibrate twin output with ideas from synthetic control (Abadie, Diamond, Hainmueller, 2010): learn on the twins how answers to a new question relate to answers to existing questions, then apply the learned relation to the humans, whose answers to the existing questions are observed. The paper evaluates ten calibration methods of this kind on MovieLens and on the Twin-2K-500 survey dataset. Its Theorem 4.1 is the explanation offered for why this works even when twins and humans disagree: the error of the transferred prediction splits into a structural part, controlled by how well the twins' inter-question structure aligns with the humans', and an estimation part that shrinks with sample size.

Setting

There are $n$ users and $m$ existing questions. The human response matrix is $Y \in \mathbb{R}^{n\times m}$ and the twin response matrix on the same questions is $\tilde Y \in \mathbb{R}^{n\times m}$ . For a new question, the twins' answers $\tilde Y_v \in \mathbb{R}^n$ are observed and the humans' answers $Y_v \in \mathbb{R}^n$ are to be predicted.

Latent factor model. There are user embeddings $U \in \mathbb{R}^{n\times d}$ , question embeddings $V \in \mathbb{R}^{m\times d}$ (one row per question) and a noise matrix $\mathcal E \in \mathbb{R}^{n\times m}$ with $Y = UV^\top + \mathcal E$ . The new question has embedding $v \in \mathbb{R}^d$ and noise $\mathcal E_v$ , so $Y_v = Uv + \mathcal E_v$ . Its embedding is decomposed as $v = V^\top b + e$ : $b \in \mathbb{R}^m$ are coefficients on the existing questions and $e \in \mathbb{R}^d$ is the part no combination of existing questions represents.

Ridge fit-and-transfer. With the sample moments of the twin system

\hat{\tilde\Sigma} = \tfrac1n \tilde Y^\top\tilde Y, \qquad \hat{\tilde\gamma} = \tfrac1n \tilde Y^\top \tilde Y_v,

and a penalty $\lambda \ge 0$ , the Ridge fit on the twins is $\hat\beta = (\hat{\tilde\Sigma} + \lambda I)^{-1}\hat{\tilde\gamma}$ , and the prediction is its transfer to the humans, $\hat Y_v = Y\hat\beta$ .

Population target. With the population moments $\tilde\Sigma = \frac1n\mathbb E[\tilde Y^\top\tilde Y]$ and $\tilde\gamma = \frac1n\mathbb E[\tilde Y^\top\tilde Y_v]$ , the target coefficients are $\beta^* = (\tilde\Sigma + \lambda I)^{-1}\tilde\gamma$ and the structural residual is $r = Y_v - Y\beta^*$ .

Vector norms $\|\cdot\|_2$ are Euclidean, matrix norms $\|\cdot\|_2$ are spectral, and $\sigma_{\min}$ is the smallest singular value.

Formalization targets

Goal: Theorem 4.1 (p. 11), both clauses

\|\hat Y_v - Y_v\|_2 \le \|r\|_2 + \frac{\|Y\|_2}{\sigma_{\min}(\hat{\tilde\Sigma}) + \lambda}\Big(\|\hat{\tilde\Sigma} - \tilde\Sigma\|_2\|\beta^*\|_2 + \|\hat{\tilde\gamma} - \tilde\gamma\|_2\Big),

\|r\|_2 \le \|Ue\|_2 + \|\mathcal E_v - \mathcal E b\|_2 + \frac{\|Y\|_2}{\sigma_{\min}(\tilde\Sigma) + \lambda}\Big(\lambda\|b\|_2 + \|\tilde\gamma - \tilde\Sigma b\|_2\Big).

The first term of the first bound is the structural error and the second is the estimation error. The bound is deterministic: it holds for every realization of the data, with no probabilistic assumption.

Milestones (Appendix B.1, pp. 32–33)

The residual split $\hat Y_v - Y_v = Y(\hat\beta - \beta^*) - r$ and its norm bound.
The fact $\|(S + \lambda I)^{-1}\|_2^{-1} = \sigma_{\min}(S) + \lambda$ for positive semidefinite $S$ .
The normal equations and the coefficient error bound for $\|\hat\beta - \beta^*\|_2$ .
The structural split $r = Ue + (\mathcal E_v - \mathcal E b) + Y(b - \beta^*)$ and its norm bound.
The population coefficient bound for $\|\beta^* - b\|_2$ .

Significance

The theorem isolates what calibration on twin data needs. The estimation error is a perturbation term: it vanishes whenever the twin sample moments concentrate around their population values, which standard concentration results give as $n \to \infty$ . The structural error vanishes in the idealized case of no residual embedding, no noise, $\lambda = 0$ and twin covariance exactly aligned with the humans', and is small when these hold approximately. The statement therefore makes precise the paper's claim that full twin fidelity is not required for useful transfer, and it is the template for analysing other instantiations of fit-and-transfer (Lasso, synthetic control weights) listed in the paper's Table 1.

The result is proved in the paper's Appendix B.1. To our knowledge it has no machine-checked proof. The mission produces one, together with a reusable formal statement of the Ridge fit-and-transfer estimator and of the spectral fact relating the regularized inverse to the smallest singular value.

Difficulty

Most of the argument is linear algebra and the triangle inequality. The step that needs real matrix analysis is the identity $\|(S + \lambda I)^{-1}\|_2^{-1} = \sigma_{\min}(S) + \lambda$ for positive semidefinite $S$ : it requires relating the operator norm of an inverse to the spectrum of a symmetric matrix, and relating the smallest singular value (defined variationally, as an infimum over unit vectors) to the smallest eigenvalue. A naive bound via submultiplicativity gives only an inequality in the wrong direction. A second point needing care is invertibility: the normal equations $(\hat{\tilde\Sigma} + \lambda I)\hat\beta = \hat{\tilde\gamma}$ and $(\tilde\Sigma + \lambda I)\beta^* = \tilde\gamma$ hold only when the regularized matrices are invertible, which must be derived from the positivity of $\sigma_{\min}(\cdot) + \lambda$ and positive semidefiniteness.

Formalization scope

Users, questions and latent coordinates are indexed by Fin n, Fin m, Fin d; vectors are Fin k → ℝ and matrices are Matrix (Fin a) (Fin b) ℝ. The Euclidean norm is vnorm x = √(x ⬝ᵥ x). The spectral norm and $\sigma_{\min}$ are GaussianMatrix.specNorm and GaussianMatrix.sMin from the published definition GaussianMatrix_basic; sMin is the infimum of $\|Ax\|_2$ over unit vectors (and $0$ on an empty index type). The mission's own definitions (SynDigits.Ridge.Model) are the sample moments, the Ridge coefficients, the fit, the transferred prediction, $\beta^*$ and $r$ .

Conventions the formalization commits to:

The population moments are generalized: $\tilde\Sigma$ is any positive semidefinite matrix and $\tilde\gamma$ any vector. The paper's expectations are such objects, so the theorem specializes to the printed one.
The latent factor model enters as hypotheses $Y = UV^\top + \mathcal E$ , $Y_v = Uv + \mathcal E_v$ , $v = V^\top b + e$ . The paper prints $v = Vb + e$ ; with $V \in \mathbb{R}^{m\times d}$ only $V^\top b$ is well typed. The noise $\mathcal E_v$ in $Y_v = Uv + \mathcal E_v$ follows Theorem 4.1's noisy setting and its proof (p. 32); §4.1 (p. 9) writes the noiseless $Y_v = Uv$ , the case $\mathcal E_v = 0$ .
Lean's matrix inverse is total and returns $0$ on a singular matrix. The hypotheses $\lambda \ge 0$ , $\sigma_{\min}(\hat{\tilde\Sigma}) + \lambda > 0$ and $\sigma_{\min}(\tilde\Sigma) + \lambda > 0$ exclude exactly the cases where the paper's inverses do not exist. Without them the junk value $\hat\beta = \beta^* = 0$ would make the statement a different (and false) claim, so no formalization may drop them; equally, no formalization may replace $\hat\beta$ by a free vector or predict with $\tilde Y\hat\beta$ instead of $Y\hat\beta$ , which would trivialize or change the theorem.
The milestone on the inverse norm is stated for $m \ge 1$ , since an empty matrix has spectral norm $0$ .

Infrastructure that a complete development needs: the spectral theorem for real symmetric matrices in the operator-norm form (Mathlib has Matrix.IsHermitian.eigenvalues and the $\ell^2$ operator norm), and the identification of sMin with the smallest eigenvalue for positive semidefinite matrices. That identification is reusable beyond this mission, for any work using GaussianMatrix.sMin. Contributions welcome: proofs of the milestones in any order, and general lemmas on sMin and specNorm.

Selected references

G. J. Fan, C. Huang, T. Peng, K. Wang, Y. Wu, SYN-DIGITS: A Synthetic Control Framework for Calibrated Digital Twin Simulation, arXiv:2604.07513v1, 2026. https://arxiv.org/abs/2604.07513
A. Abadie, A. Diamond, J. Hainmueller, Synthetic Control Methods for Comparative Case Studies, Journal of the American Statistical Association 105(490), 2010. https://doi.org/10.1198/jasa.2009.ap08746
A. E. Hoerl, R. W. Kennard, Ridge Regression: Biased Estimation for Nonorthogonal Problems, Technometrics 12(1), 1970. https://doi.org/10.1080/00401706.1970.10488634

8 thms3 active usersReviewed

Combinatorics Graph Theory Operations Research+1·Captain: mikedeng1

On the Effect of Symmetry Requirement for Rendezvous on the Complete Graph: Symmetric Strategies Wait at Least (n+1)/2 + 2⁻³⁶nResearch Paper

Motivation

Rendezvous search asks how two agents who cannot communicate should move so as to meet as soon as possible. Alpern posed the problem in 1976, and it became a standard topic in search games (Alpern and Gal, The Theory of Search Games and Rendezvous, 2003). Its simplest discrete version is played on the complete graph $K_n$ : there are $n$ locations, every location can be reached from every other in one step, and the players have no common way to name the locations.

The version studied here distinguishes two settings. In the asymmetric setting the players may agree in advance on different roles. In the symmetric setting they must use the same randomized rule, as two identical robots or two strangers with no way to tell who is who would. The question is whether symmetry has a cost, and how large it is.

Timeline:

1976: Alpern poses rendezvous search; the "telephone problem" becomes the rendezvous game on $n$ discrete locations, originally in the symmetric setting.
1990: Anderson and Weber solve the asymmetric game on $K_n$ : every pair of strategies has expected waiting time at least $(n+1)/2$ , and the wait-for-mommy pair attains it (one player stays at one location, the other visits every location once in random order). For the symmetric game they propose the Anderson–Weber strategy, whose expected waiting time is asymptotically slightly below $0.829n$ , and show it is optimal for $n=2$ .
2012: Weber proves the Anderson–Weber strategy optimal for $n=3$ ; for $n=4$ a slightly better strategy outside that family is known. Asymptotic optimality of the Anderson–Weber strategy remains a conjecture.
2020: Bonamy, Pilipczuk and Sereni prove the first lower bound for the symmetric game, for every $n\ge2$ , that exceeds the asymmetric value $(n+1)/2$ by a linear term (arXiv:2002.03764). The journal version, with Weber, appeared in Mathematics of Operations Research in 2023.

Setting

There are $n$ locations and two players $A$ and $B$ . Each player numbers the locations privately by $[n]=\{1,\dots,n\}$ .

A tactic is a function $\tau:[n]\to[n]$ . In round $i$ the player visits location $\tau(i)$ of her own numbering. The set of tactics is $\Theta_n$ .
A strategy is a probability distribution $\sigma$ on $\Theta_n$ . The set of strategies is $\Sigma_n$ .
The binding is a permutation $\pi$ of $[n]$ , drawn uniformly at random, that translates $A$ 's numbering into $B$ 's.
Player $A$ draws $\tau_A\sim\sigma_A$ , player $B$ draws $\tau_B\sim\sigma_B$ , and $\pi$ is drawn uniformly. The three draws are independent. The waiting time is

T\langle\sigma_A,\sigma_B\rangle=\min\bigl(\{\,i\in[n]:\pi(\tau_A(i))=\tau_B(i)\,\}\cup\{n+1\}\bigr).

It is the first round in which both players stand at the same place, and $n+1$ if they do not meet within $n$ rounds.

For fixed tactics, $W(\tau_A,\tau_B)=\mathbb E_\pi[T]$ , so that $\mathbb E\,T\langle\sigma_A,\sigma_B\rangle=\sum_{\tau_A,\tau_B}\sigma_A(\tau_A)\sigma_B(\tau_B)W(\tau_A,\tau_B)$ .
A tactic is passive if it visits at most $n/2$ distinct locations ( $|\tau([n])|\le n/2$ ) and active otherwise (Definition 3).
For tactics $\tau_A,\tau_B$ , the pair set is $F=\{(\tau_A(i),\tau_B(i)):i\in[n]\}$ , with $m=|F|$ . The match count $X$ is the number of pairs $(i,j)\in F$ with $\pi(i)=j$ . No rendezvous occurs exactly when $X=0$ .

Formalization targets

Goal: Theorem 1

For every $n\ge2$ and every strategy $\sigma\in\Sigma_n$ ,

\mathbb E\,T\langle\sigma,\sigma\rangle\ \ge\ \frac{n+1}{2}+2^{-36}\,n .

The paper states "there exists $\varepsilon>0$ " and determines $\varepsilon=2^{-36}$ at the end of its proof. The goal uses that constant, which is uniform in $n$ .

Milestones

In the order of the proof:

Theorem 2: $\mathbb E\,T\langle\sigma_A,\sigma_B\rangle\ge (n+1)/2$ for all $\sigma_A,\sigma_B$ .
Equation (1): $W\ge(n+1)/2$ for all pairs of tactics.
$W$ is symmetric, and equation (2) splits $\mathbb E\,T\langle\sigma,\sigma\rangle$ into passive and active parts.
Lemma 5: if $\mathbb P(\text{no rendezvous})\ge\beta>0$ , then $W\ge (n+1)/2+(\beta^2/2)n$ .
Equation (6): $\mathbb P(\text{no rendezvous})=\mathbb P(X=0)$ .
Assertion 1: joint match probabilities of 2, 3 and 4 distinct pairs.
Assertion 2: $\mathbb E X^4\le 15$ .
Theorem 7, the Paley–Zygmund inequality. It is referenced from the platform in an equivalent form.
Lemma 6: if $m\ge(1-\sqrt{\alpha/2})n$ and $\operatorname{Var}X\ge\alpha$ , then $\mathbb P(X=0)\ge\alpha^2/128$ .
Lemma 8: if $F$ contains at least $\alpha\binom n2$ disjoint pairs, then $\operatorname{Var}X\ge\alpha$ .
Lemma 9: a bipartite degree-splitting lemma.
Lemma 10: for tactics of the same kind with $|F|\ge\frac{11}{12}n$ , $\operatorname{Var}X\ge 1/32$ .
Lemma 4: for tactics of the same kind, $W\ge(n+1)/2+2^{-35}n$ .

Significance

The result. Without the symmetry constraint the optimum is exactly $(n+1)/2$ . Theorem 1 shows that requiring both players to use the same strategy costs a linear number of extra rounds, with a constant independent of $n$ . According to the paper, no asymptotic lower bound above $(n+1)/2$ was known for the symmetric game before. The bound is proved for the game stopped after $n$ rounds; since stopping can only shorten the waiting time, it also bounds the unstopped game, for which the Anderson–Weber strategy achieves about $0.829n$ . The intermediate results also stand alone: Lemma 4 bounds the waiting time for any two tactics of the same kind, and Lemmas 6–8 relate anti-concentration of the match count to the structure of a set of pairs.

Formalizing it. The result is proved on paper and, as far as is known, has not been machine-checked. A formalization would give the platform a discrete rendezvous game on $K_n$ , which it does not yet have; the existing rendezvous material is the continuous game on the line. It would also give exact moment computations for indicator sums over a uniformly random permutation, and a bipartite edge-splitting lemma. Two printed statements, Lemma 5 and equation (6), write the no-rendezvous event as $\tau_A(\pi(i))\neq\tau_B(i)$ , and both are false as printed. The mission states them with the event of the game's definition, $\pi(\tau_A(i))\neq\tau_B(i)$ , which is the event their proofs use.

Difficulty

The only general tool for this game is the union bound: in each round the players meet with probability at most $1/n$ . This gives $(n+1)/2$ for every pair of strategies, and it cannot detect symmetry, because the bound is tight for a pair of different strategies. A symmetric strategy, however, has a constant probability of producing two tactics of the same kind. The work is to show that two passive tactics, or two active ones, fail to meet in all $n$ rounds with constant probability.

The match count $X$ has mean $m/n\le1$ , so this is an anti-concentration statement about a sum of dependent indicators. Bounding the variance from below requires a quadratic number of disjoint pairs in $F$ , which is a structural fact about bipartite graphs. Bounding the fourth moment from above requires joint probabilities of up to four matches. The constants have to be carried exactly through all of these steps to reach $2^{-36}$ .

Formalization scope

Locations and rounds are Fin n, and Lean round $i$ is round $i+1$ of the paper.
A tactic is Fin n → Fin n, and a binding is Equiv.Perm (Fin n).
Every expectation or probability over the binding is the finite average over the $n!$ permutations (avgPerm); no measure theory is used.
The waiting time is the least $i+1$ with $\pi(\tau_A(i))=\tau_B(i)$ , or $n+1$ .
A strategy is an element of stdSimplex ℝ (Fin n → Fin n), so $\sigma$ ranges over all probability vectors on all $n^n$ tactics.
$\mathbb E\,T\langle\sigma_A,\sigma_B\rangle$ is expWait σA σB, the double sum of $\sigma_A(\tau_A)\sigma_B(\tau_B)W(\tau_A,\tau_B)$ .
$\operatorname{Var}X$ is $\mathbb E X^2-(\mathbb EX)^2$ .
Disjoint pairs in $F$ are counted as unordered pairs.
The §3 statements carry the paper's standing hypothesis $n\ge2$ .

The goal takes one strategy vector $\sigma$ for both players. A version with two strategies is false (wait-for-mommy), a version with deterministic strategies only is a special case, and a version in which $\varepsilon$ may depend on $n$ is weaker. None of these counts as the goal.

A complete development needs:

moment computations for indicator sums over a uniform permutation;
the Paley–Zygmund inequality, which is on the platform as OAI.IndependentProducts.second_moment_tail_bound;
a degree-splitting argument for bipartite graphs;
the Anderson–Weber union-bound argument.

The permutation-moment lemmas and Lemma 9 can be reused beyond this mission. Proofs of any milestone are welcome, and so are alternative arguments with better constants.

Selected references

M. Bonamy, M. Pilipczuk, J.-S. Sereni, On the effect of symmetry requirement for rendezvous on the complete graph, arXiv:2002.03764v1, 2020; with R. Weber, Mathematics of Operations Research, 2023. https://arxiv.org/abs/2002.03764
E. J. Anderson, R. R. Weber, The rendezvous problem on discrete locations, Journal of Applied Probability 27(4), 1990. https://doi.org/10.2307/3214798
R. Weber, Optimal symmetric rendezvous search on three locations, Mathematics of Operations Research 37(1), 2012. https://doi.org/10.1287/moor.1110.0528
S. Alpern, S. Gal, The Theory of Search Games and Rendezvous, Kluwer, 2003. https://doi.org/10.1007/b100809
R. E. A. C. Paley, A. Zygmund, A note on analytic functions in the unit circle, Proc. Cambridge Philos. Soc. 28(3), 1932. https://doi.org/10.1017/S0305004100010112

15 thms3 active usersReviewed

Completed

Combinatorics Complexity Theory·Captain: yousofy

Block Sensitivity vs. Sensitivity: Reach $2.131121719190$ Open Problem

The regular theorem's proof has been accepted by Prove2Me.

Open the proved theorem.

What this mission establishes

For a total Boolean function, sensitivity counts the largest number of individual bit flips that can change the output at one input. Block sensitivity allows each change to flip a nonempty set of bits, with the sets required to be pairwise disjoint. The campaign asks how large block sensitivity can be compared with sensitivity as the latter grows.

This entry targets the exact rational exponent

\alpha=2.131121719190=\frac{2131121719190}{10^{12}}.

Its goal is the campaign's shared statement: for every $\varepsilon>0$ and every integer $S\ge2$ , there is a total Boolean function $f$ with

s(f)\ge S, \qquad bs(f)\ge s(f)^{\alpha-\varepsilon}.

The construction behind the goal

The proof uses the Paley tournament of order $11987$ , a single binary labeling meeting 23 simultaneous exclusion families, twenty nested Boolean predicates, and a four-phase recurrence. A 2130-entry integer invariant yields actual Boolean functions with

16^m\le s(f_m)\le 230508375206254\cdot45238253^m, \qquad bs(f_m)\ge11987^{4m}.

Consequently the formal proof contains the stronger exact exponent

\beta=\frac{4\log(11987)}{\log(45238253)}, \qquad 2.131125283430<\beta.

The mission keeps the requested value $2.131121719190$ as its canonical recorded goal. The exact stronger endpoint and logarithmic comparison remain named theorems in the full proof source.

Formal statement and provenance

The goal imports Definitions.Def_SensitivitySeparation and Definitions.Def_SensitivityCampaign. These are the campaign's own definitions of sensitivity, block sensitivity, and the quantified exponent property. The checked Lean proof establishes the simultaneous labeling, actual Boolean transfer, exact recurrence, block witnesses, and asymptotic conclusion together.

This is an original construction and certificate for the block-sensitivity versus sensitivity campaign. The regular theorem is already proved on Prove2Me. This draft references that accepted theorem as its goal. The captain performs the final review and submission; campaign inclusion and the attested value remain subject to moderator approval.

5 thms3 active usersReviewed

Markov Chain Probability Reinforcement Learning+1·Captain: mikedeng1

Uncertainty Quantification and Exploration for Reinforcement Learning: Empirical Q-Values Are Strongly Consistent and √n(Q̂ₙ − Q) ⇒ N(0, Σ) with the Closed-Form Covariance (5)Research Paper

Motivation

A reinforcement-learning agent that learns a Markov decision process (MDP) from data ends up with point estimates of the Q-values: the long-run discounted reward of taking an action in a state and acting optimally afterwards. Point estimates say nothing about their own reliability. Choosing between two actions whose estimated values differ by a small margin, deciding how much more data to collect, or allocating exploration effort all need the sampling distribution of the estimate. Finite-sample bounds (Kearns and Singh 1998) give rates with loose constants. Asymptotic normality gives exact limiting constants.

Zhu, Dong and Lam establish a central limit theorem for the plug-in Q-value estimate of a finite MDP whose data are collected by an exploration policy, with an explicit covariance matrix. For a fixed policy, the analogous result for the value function was obtained by Mannor, Simester, Sun and Tsitsiklis (2007). The new step is the optimal Q-values, which depend on the data through a maximum over actions. The paper uses the covariance to design a pure-exploration policy (Q-OCBA) that allocates samples to maximize the probability of selecting the optimal policy.

Setting

Let $\mathcal S$ and $\mathcal A$ be finite nonempty sets of states and actions. A pair $(s,a)$ has a random reward with law $R(s,a)$ on $\mathbb R$ , mean $\mu_R(s,a)$ and variance $\sigma^2_R(s,a)$ , and moves to state $k$ with probability $P(k\mid s,a)$ . The discount factor is $\gamma\in[0,1)$ . The Bellman operator is

\mathcal T_{r,P'}(Q)(s,a)=r(s,a)+\gamma\sum_{k\in\mathcal S}P'(k\mid s,a)\max_{a'}Q(k,a'),

and the Q-values are its fixed point $Q=\mathcal T_{\mu_R,P}(Q)$ , with $V^*(s)=\max_aQ(s,a)$ .

Data are collected by an exploration policy $\pi(a\mid s)$ . Starting from some state, the agent repeatedly takes $a_t\sim\pi(\cdot\mid s_t)$ , observes $r_t\sim R(s_t,a_t)$ , and moves to $s_{t+1}\sim P(\cdot\mid s_t,a_t)$ . The state-action pairs then form a Markov chain with transition matrix $\tilde P^\pi((s,a),(s',a'))=P(s'\mid s,a)\pi(a'\mid s')$ . From $n$ observations, the plug-in estimates are the sample mean reward $\hat\mu_{R,n}(s,a)$ and the empirical transition frequencies $\hat P_n(k\mid s,a)$ at each pair, with fixed initial values at unvisited pairs. The estimate $\hat Q_n$ is the fixed point of $\mathcal T_{\hat\mu_{R,n},\hat P_n}$ .

The standing assumptions are:

Assumption 1: finite reward variances, with rewards independent of the next state given $(s,a)$ .
Assumption 2: every state has a unique optimal action $a^*(s)$ .
Assumption 3: $\tilde P^\pi$ is irreducible. Its stationary distribution $w$ is then positive and equals the long-run visit frequency of each pair.

Formalization targets

Goal: Theorem 1

Under Assumptions 1–3, $\hat Q_n\to Q$ almost surely, and

\sqrt n(\hat Q_n-Q)\Rightarrow\mathcal N(0,\Sigma),\qquad \Sigma=(I-\gamma\tilde P^{\pi^*})^{-1}W^{-1}(D_R+\gamma^2D_Q)\big((I-\gamma\tilde P^{\pi^*})^{-1}\big)^T.

Here $\tilde P^{\pi^*}((s,a),(s',a'))=P(s'\mid s,a)\mathbb 1(a'=a^*(s'))$ , and $W$ , $D_R$ , $D_Q$ are diagonal with entries $w(s,a)$ , $\sigma^2_R(s,a)$ and $(V^*)^T\Sigma_{P_{s,a}}V^*$ . The matrix $\Sigma_{P_{s,a}}$ is the multinomial covariance of $P(\cdot\mid s,a)$ . The covariance is part of the statement: the paper's subsequent results (Corollary 1, Q-OCBA) use it.

Milestones (the proof of Theorem 1, App. A.1)

(22): $[\hat\mu_{R,n},\hat P_n]\to[\mu_R,P]$ almost surely.
$\frac1n\#\{t\le n:(s_t,a_t)=(i,j)\}\to w(i,j)$ almost surely.
(23): $\sqrt n([\hat\mu_{R,n},\hat P_n]-[\mu_R,P])\Rightarrow\mathcal N(0,\Sigma_{R,P})$ , where $\Sigma_{R,P}=\operatorname{diag}(W^{-1}D_R,D_P)$ and $D_P$ is block diagonal with blocks $\Sigma_{P_{s,a}}/w(s,a)$ .
$I-\gamma\tilde P'$ is invertible for every stochastic $P'$ and every $Q'$ with unique argmaxes.
The fixed point $\phi(r',P')$ is continuously differentiable at $(\mu_R,P)$ , with gradient $(I-\gamma\tilde P^{\pi^*})^{-1}[\,I\mid\gamma\operatorname{blockdiag}((V^*)^T)\,]$ .
$\hat Q_n\to Q$ almost surely.
$\nabla\phi\,\Sigma_{R,P}\,\nabla\phi^T=\Sigma$ .

Significance

The result. Theorem 1 gives asymptotically exact simultaneous confidence regions for all Q-values from one trajectory of exploration data. The closed form of $\Sigma$ shows how each source of noise contributes: reward noise through $D_R$ , transition noise through $D_Q$ , the amount of data at each pair through $W^{-1}$ , and propagation through the dynamics of the optimal policy through $(I-\gamma\tilde P^{\pi^*})^{-1}$ . This decomposition is what makes $\Sigma$ usable as an objective for allocating exploration effort, which the paper's Q-OCBA policy does. Corollary 1 (CLT for the optimal value $V^*$ ) is derived from it.

Formalizing it. The result is proved in the paper, but the proof cites its probabilistic core: a joint central limit theorem for empirical transition frequencies of an irreducible finite Markov chain (Trevezas and Limnios 2009, Proposition 3), together with the multivariate delta method. A machine-checked proof would also certify that the covariance formula, with its transposes and weights, is correct as printed. No Q-value CLT or Markov-chain CLT for empirical transition matrices is currently formalized on the platform. The existing Markov-chain CLTs there are scalar and assume uniform ergodicity.

Difficulty

The deterministic half (milestones 4, 5, 7) is linear algebra plus an implicit-function argument. The obstacle is that $Q$ depends on $(\mu_R,P)$ through a maximum, which is not differentiable at ties. Assumption 2 removes ties at $(\mu_R,P)$ , and differentiability holds only on a neighbourhood where the argmax stays the same.

The probabilistic half is harder. A natural first idea is to treat the visits to each pair as i.i.d. samples and apply the classical multivariate CLT. This fails because the number of visits is random and depends on the whole trajectory, and the samples at different pairs are dependent through the chain. The CLT (23) needs a martingale or regeneration argument for the Markov chain on state-action pairs. The chain is only assumed irreducible, so it may be periodic, and uniformly ergodic CLTs do not apply directly.

Formalization scope

Indexing and spaces. State-action pairs are indexed by S × A with Fintype, DecidableEq and Nonempty; the paper's flattening $(i-1)m_a+j$ is notation only. $P$ , $\pi$ and the initial state law are PMFs, and rewards are probability measures on $\mathbb R$ with MemLp id 2 (Assumption 1).
Discount. $0\le\gamma<1$ is pinned; the paper leaves it implicit.
Data law. The data form the Markov chain $((s_t,a_t),r_t)$ on $(\mathcal S\times\mathcal A)\times\mathbb R$ described in Setting, with law given by the published MarkovChainCLT.chainMeasure. Every initial state law is allowed. Time is 0-based.
Fixed points. The fixed point is the limit of value iteration (bellmanFix). It is the unique fixed point whenever the Bellman operator is a contraction, which covers every stochastic $P'$ and a neighbourhood of $(\mu_R,P)$ .
Assumptions 2 and 3. Assumption 2 is a strict inequality $Q(s,a)<Q(s,a^*(s))$ for $a\ne a^*(s)$ . Assumption 3 is $\forall x,y\ \exists m,\ (\tilde P^\pi)^m(x,y)>0$ , and $w$ is bound by the stationarity equations.
Limits. The Gaussian limits are Mathlib's multivariateGaussian on EuclideanSpace, and convergence in distribution is TendstoInDistribution.

Trivializations ruled out.

Matrix.inv returns $0$ on singular matrices, but $I-\gamma\tilde P^{\pi^*}$ is invertible under the pins, so $\Sigma$ is not a junk zero.
multivariateGaussian returns a point mass for a non-positive-semidefinite matrix, but $\Sigma$ and $\Sigma_{R,P}$ are positive semidefinite.
A non-strict argmax (which would admit ties and the non-Gaussian limit of the paper's Theorem 2) is excluded.
Rewards and transitions live on one trajectory under one chain law, not on independent spaces.

Infrastructure. A complete development needs:

an ergodic theorem for finite irreducible Markov chains (milestone 2);
a multivariate Markov-chain CLT (milestone 3), which is reusable well beyond this mission;
the multivariate delta method and continuous mapping in TendstoInDistribution form;
differentiability of a contraction fixed point in parameters.

Contributions of any of these as standalone lemmas are welcome.

Not posed. Corollaries 1–2 and Theorems 2–6 of the paper (optimal-value and fixed-policy CLTs, non-unique optimal policies, constrained MDPs, Q-OCBA consistency, approximate value iteration, kernel representations) are not part of this mission.

Selected references

Y. Zhu, J. Dong, H. Lam, Uncertainty Quantification and Exploration for Reinforcement Learning, Operations Research, 2024; arXiv:1910.05471v3, 2022. https://arxiv.org/abs/1910.05471
S. Mannor, D. Simester, P. Sun, J. N. Tsitsiklis, Bias and Variance Approximation in Value Function Estimates, Management Science 53(2):308–322, 2007. https://doi.org/10.1287/mnsc.1060.0614
S. Trevezas, N. Limnios, Variance Estimation in the Central Limit Theorem for Markov Chains, Journal of Statistical Planning and Inference 139(7):2242–2253, 2009. https://www.sciencedirect.com/journal/journal-of-statistical-planning-and-inference/vol/139/issue/7
R. J. Serfling, Approximation Theorems of Mathematical Statistics, Wiley, 2009 (delta method). https://doi.org/10.1002/9780470316481
M. Kearns, S. Singh, Finite-Sample Convergence Rates for Q-Learning and Indirect Algorithms, Advances in Neural Information Processing Systems 11, 996–1002, 1998.

10 thms3 active usersReviewed

Completed

Combinatorics Machine Learning Operations Research+1·Captain: mikedeng1

The Power of Subsampling in Submodular Maximization: SampleGreedy is a (p+1)²/p-approximation for non-negative submodular maximization over p-extendible systemsResearch Paper

Motivation

Many selection problems in machine learning and operations research ask for a set of items that maximizes a utility with diminishing returns, subject to a combinatorial feasibility constraint: summarizing a collection of images or documents, placing sensors, recommending a diverse set of products, or choosing a set of edges that forms a matching. Diminishing returns is submodularity; the feasibility constraints in these examples (matroids, intersections of matroids, matchings, knapsack-type systems) are instances of $p$ -extendible systems, a class introduced by Mestre (ESA 2006). Many useful objectives, such as graph cuts and diversity-regularized utilities, are non-monotone: adding an item can lower the value.

The greedy algorithm has a long history for this problem class. Fisher, Nemhauser and Wolsey (1978, doi:10.1007/BFb0121195) showed that greedy gives a $(p+1)$ -approximation for monotone submodular objectives over $p$ -systems, a class that contains $p$ -extendible systems. For non-monotone objectives, the known greedy-based algorithms ran the greedy algorithm repeatedly. Gupta, Roth, Schoenebeck and Talwar (WINE 2010) obtained roughly $3p$ , Mirzasoleiman et al. (2016) roughly $2p$ , and Feldman, Harshaw and Karbasi (COLT 2017) $p + O(\sqrt p)$ , each with $\Omega(nkp)$ or $\Omega(nk\sqrt p)$ oracle queries. Harshaw, Kazemi, Feldman and Karbasi (arXiv:2104.02772; Mathematics of Operations Research, 2022) showed that a single random subsampling of the ground set, followed by one run of the plain greedy algorithm, gives a $(p+1)^2/p$ -approximation for non-negative submodular objectives with expected $O(n + nk/p)$ oracle calls. This mission formalizes that guarantee.

Setting

Let $\mathcal N$ be a finite ground set of size $n$ , with a fixed linear order $u_1 < \dots < u_n$ that is used only to break ties. A set function is a map $f : 2^{\mathcal N} \to \mathbb R$ . The marginal gain of $u$ at $S$ is $f(u \mid S) = f(S \cup \{u\}) - f(S)$ .

$f$ is submodular if $f(A \cup \{e\}) - f(A) \ge f(B \cup \{e\}) - f(B)$ whenever $A \subseteq B$ and $e \notin B$ ; monotone if $A \subseteq B$ implies $f(A) \le f(B)$ ; linear if the submodular inequality always holds with equality.
A predicate $\mathcal I$ on subsets is an independence system if $\emptyset \in \mathcal I$ and $\mathcal I$ is closed under taking subsets. It is $p$ -extendible if for all $A \subseteq B$ in $\mathcal I$ and every $e \notin A$ with $A \cup \{e\} \in \mathcal I$ there is $Y \subseteq B \setminus A$ with $|Y| \le p$ and $(B \setminus Y) \cup \{e\} \in \mathcal I$ .

The problem is $\max_{S \in \mathcal I} f(S)$ for non-negative submodular $f$ ; OPT denotes a maximizer.

SampleGreedy with sampling probability $q$ keeps each element independently with probability $q$ , giving a sample $\mathcal N'$ . It then starts from $S = \emptyset$ and repeatedly adds the element $u \in \mathcal N'$ of largest marginal gain among those with $S \cup \{u\} \in \mathcal I$ and $f(u \mid S) > 0$ , ties broken by the fixed order, until no such element is left. Its expected value is

\mathbb E_q[f(S)] = \sum_{\mathcal N' \subseteq \mathcal N} q^{|\mathcal N'|}(1-q)^{n-|\mathcal N'|}\, f\big(\mathrm{SampleGreedy}(\mathcal N')\big).

For the analysis the paper introduces Algorithm 2, which runs greedy over the whole ground set, flips a $q$ -coin for each chosen element, and maintains a set $O$ (initially OPT), removal sets $O_u$ , snapshots $S_u$ and indicators $X_u$ (" $u$ was considered") and $Y_u$ .

Formalization targets

Goal: Theorem 1 (p. 7)

For non-negative submodular $f$ , a $p$ -extendible system with $p \ge 1$ , and every $T \in \mathcal I$ : SampleGreedy's output is always independent, and $$f(T) \le \frac{(p+1)^2}{p},\mathbb E_{1/(p+1)}[f(S)], \qquad f(T) \le (p+1),\mathbb E_{1/(p+1)}[f(S)] \ \text{if $f$ is monotone},

f(T) \le p,\mathbb E_{1/p}[f(S)] \ \text{if $f$ is linear}.$$

Milestones

In attack order: Lemma 3 (p. 8, already Proved on the platform: a random set whose elements each appear with probability at most $q$ keeps a $(1-q)$ fraction of $g(\emptyset)$ in expectation); Lemma 4 (p. 10, SampleGreedy and Algorithm 2 have the same output law); Lemma 5 (p. 11, invariants of Algorithm 2); Lemma 6 (p. 12, $f(S) \ge f(S\cup \mathrm{OPT}) - \sum_u |O_u \setminus S|\, f(u\mid S_u)$ ); Lemma 7 (p. 13, inequality (5)); Lemma 8 (p. 14); the display of §4.1.1 (p. 14); Lemma 9 (p. 15, linear objectives); Lemma 10 (p. 16, inequality (7)).

Significance

The result shows that one random subsample plus one greedy pass beats the repeated-greedy algorithms for non-monotone objectives over $p$ -extendible systems, both in ratio and in query count, and matches the classical $p+1$ for monotone objectives. Since no polynomial-query algorithm achieves a ratio better than $p + 1/2$ for this problem (Feldman, Harshaw and Karbasi 2017, Theorem 4), the ratio $(p+1)^2/p = p + 2 + 1/p$ is nearly tight. The proof technique, which couples the subsampled algorithm with an auxiliary algorithm that flips coins only for the elements it considers, is reused in the paper's streaming algorithm and in later subsampling-based algorithms.

The result is proved on paper; no machine-checked version is known. A formalization would give a checked analysis of a randomized greedy algorithm over an abstract independence system, including the coupling of two random processes, which is the step that informal proofs usually treat most briefly. It would also give reusable definitions of $p$ -extendible systems and of greedy runs with explicit tie-breaking. The mission also records a defect of the printed text: Lemma 9 as printed is false for linear functions with $f(\emptyset) > 0$ , so it is stated here with $f(\emptyset) = 0$ .

Difficulty

The obvious argument would analyze SampleGreedy directly, but there the sample and the greedy path are entangled: which element is chosen next depends on the whole sample. The analysis instead goes through Algorithm 2, and the hard step is Lemma 4, an exact equality of output laws. Its proof needs both algorithms to break ties identically and the coins to be fixed in advance. After that, the expectation bounds of Lemmas 7, 8 and 10 condition on the history up to the iteration in which a given element is considered, and the coin of that element is independent of that history. In the finite-sum encoding this conditioning becomes a combinatorial regrouping of the $2^n$ coin outcomes, which has to be carried out explicitly. Lemma 6 requires a disjointness argument for the sets $O_u \setminus S$ across the whole run.

Formalization scope

The ground set is a Fintype α with a LinearOrder α, which is the paper's tie-breaking order (p. 10). Set functions are Finset α → ℝ, and $\mathcal I$ is a predicate Finset α → Prop. The parameter $p$ is a natural number with $p \ge 1$ . Submodularity is the published lattice form NonmonotoneSubmod.Shared.Submodular ( $f(S\cup T)+f(S\cap T)\le f(S)+f(T)$ ), equivalent on finite ground sets to the paper's (1). The while loops run for exactly $n$ iterations, which is enough because each effective iteration adds or considers a new element. Expectations are exact finite sums over the $2^n$ samples or coin outcomes. Algorithm 2's coins are a fixed bit set, and its line 6 is one fixed minimum-cardinality choice. " $\alpha$ -approximation" for a randomized algorithm is read, as in the paper's proof, as $\mathbb E[f(S)] \ge f(\mathrm{OPT})/\alpha$ , stated against every independent $T$ . Linear means (1) with equality and allows $f(\emptyset) \neq 0$ , except in Lemma 9, which adds $f(\emptyset)=0$ . The oracle-count clause $O(nk/p)$ of Theorem 1 is not formalized.

Trivializing encodings are excluded. The expected value is a sum over the greedy runs on each sample, with the sample as the greedy pool (not the whole ground set followed by a filter). The weights sum to 1. The comparison set is always assumed independent. The ratio $(p+1)^2/p$ is real division. A sanity file checks that the output on a sample differs from the output on the whole ground set.

A complete development needs the greedy run's invariants, the coupling of Lemma 4, and the regrouping of finite sums over coin outcomes by the history before a given element is considered. The last of these is reusable for any analysis of an algorithm that flips independent coins. Proofs of any milestone, and alternative proofs of Lemma 4, are welcome.

Selected references

C. Harshaw, E. Kazemi, M. Feldman, A. Karbasi, The Power of Subsampling in Submodular Maximization, Mathematics of Operations Research, 2022; preprint arXiv:2104.02772v1, 2021. https://arxiv.org/abs/2104.02772
M. Feldman, C. Harshaw, A. Karbasi, Greed is Good: Near-Optimal Submodular Maximization via Greedy Optimization, COLT, 2017. https://arxiv.org/abs/1704.01652
N. Buchbinder, M. Feldman, J. Naor, R. Schwartz, Submodular Maximization with Cardinality Constraints, SODA, 2014. https://doi.org/10.1137/1.9781611973402.106
M. L. Fisher, G. L. Nemhauser, L. A. Wolsey, An analysis of approximations for maximizing submodular set functions – II, Mathematical Programming Study 8, 1978. https://doi.org/10.1007/BFb0121195
J. Mestre, Greedy in Approximation Algorithms, ESA, 2006. https://doi.org/10.1007/11841036_49

13 thms3 active usersReviewed

Quantum Information Representation Theory Statistics·Captain: mikedeng1

Parallel Treatment of Estimation of SU(2) and Phase Estimation: with a Reference System, n = 2d − 1 Uses of an Unknown SU(2) Matrix Reach Worst-Case Error sin²(π/(2d+2)), so n²·Error → π²Research Paper

Motivation

Two parties who do not share a reference frame can align one by sending quantum systems through an unknown rotation. Mathematically, a device applies an unknown matrix $g\in\mathrm{SU}(2)$ to each of $n$ qubits, and the task is to estimate $g$ from one measurement on the output. How fast the smallest achievable error falls with $n$ is a basic question of quantum metrology and quantum statistics: classical repetition gives order $1/n$ , and entangled inputs can do better.

Masahito Hayashi's paper (arXiv:quant-ph/0407053v3) shows that, with the right input, estimating an SU(2) action reduces exactly to the phase-estimation problem solved by Bužek, Derka and Massar. The reduction yields an error of order $1/n^2$ with the explicit constant $\pi^2$ .

Timeline.

1999. Bužek, Derka and Massar (quant-ph/9808042) determine the optimal phase estimate (the "quantum clock"), with error $\cong\pi^2/(4n^2)$ .
2001. Acín, Jané and Vidal (quant-ph/0012015) study optimal estimation of SU(2) dynamics.
2002. Fujiwara (doi:10.1103/PhysRevA.65.012316) shows that a reference system reduces the error for a single use of $g$ .
2003–2004. Bagan, Baig and Muñoz-Tapia (quant-ph/0303019) and Chiribella, D'Ariano, Perinotti and Sacchi (quant-ph/0405095) obtain $1/n^2$ scaling for reference-frame alignment.
2004. Hayashi (this paper) gives the reduction to phase estimation.
2005. Chiribella, D'Ariano and Sacchi (quant-ph/0506267) prove that the error is optimal among all measurements in a general group framework.

Setting

Let $\mathrm{SU}(2)$ be the group of $2\times2$ complex unitary matrices of determinant one, and let $\mu$ be its invariant (Haar) probability measure. The cost of reporting $\hat g$ when the truth is $g$ is

d(g,\hat g)=1-\Big|\tfrac12\operatorname{Tr}(g^{-1}\hat g)\Big|^2 .

For each $j\ge1$ , let $V^j$ be the $j$ -dimensional irreducible representation of $\mathrm{SU}(2)$ on a space $\mathcal H_j$ . If $g$ has eigenvalues $e^{\pm i\theta/2}$ , its character is

\chi_j(g)=\operatorname{Tr}V^j_g=\frac{\sin(j\theta/2)}{\sin(\theta/2)}=U_{j-1}\big(\operatorname{Re}\operatorname{Tr}g/2\big),

where $U_m$ is the Chebyshev polynomial of the second kind.

For $n=2d-1$ uses of $g$ with a reference system on which $g$ does not act, the paper works on

\bigoplus_{k=1}^d\mathcal H_{2k}\otimes\mathcal H_{2k,R},\qquad U_g=\bigoplus_k V^{2k}_g\otimes I .

Its ingredients are:

Input. $x_{\vec x}=\bigoplus_kx_k\,x^{2k}_E$ , where $x\in\mathbb C^d$ satisfies $\sum_k|x_k|^2=1$ and $x^{2k}_E=\operatorname{vec}(I)/\sqrt{2k}$ is maximally entangled.
Measurement. For a Hermitian $T=(t_{k,l})\ge0$ with $t_{k,k}=1$ ,

M^T(d\hat g)=U_{\hat g}\Big(\sum_{k,l}t_{k,l}\,|(2k)x^{2k}_E\rangle\langle(2l)x^{2l}_E|\Big)U_{\hat g}^\dagger\,\mu(d\hat g).

Error at a fixed true $g$ .

\mathcal D_g(M,x)=\int d(g,\hat g)\,\operatorname{Tr}M(d\hat g)\,U_g|x_{\vec x}\rangle\langle x_{\vec x}|U_g^\dagger .

The method value of an input is $v(x)=\frac12\big(1-\sum_{k=1}^{d-1}|x_k||x_{k+1}|\big)$ .

Formalization targets

Goal: exact error, attained optimum, and the constant $\pi^2$

The goal theorem has four parts.

For every $d$ , irreducible representations of dimensions $2,4,\dots,2d$ with the Weyl characters exist.
For every unit $x$ and every admissible $T$ , $M^T$ is a POVM, and at every true $g$

\mathcal D_g(M^T,x)=\tfrac12\sum_k|x_k|^2t_{k,k}-\tfrac14\sum_{k=1}^{d-1}\operatorname{Re}\big(\overline{x_k}x_{k+1}t_{k,k+1}+\overline{x_{k+1}}x_kt_{k+1,k}\big)\ \ge\ v(x).

Equality holds for the phase-aligned $T$ , $t_{k,l}=\frac{x_k}{|x_k|}\overline{\frac{x_l}{|x_l|}}$ . 3. For $d\ge1$ , $\displaystyle\min_{\|x\|=1}v(x)=\sin^2\frac{\pi}{2d+2}$ , and the minimum is attained. 4.

\lim_{d\to\infty}(2d-1)^2\sin^2\frac{\pi}{2d+2}=\pi^2 .

Milestones

(15) Weyl integration over $\mathrm{SU}(2)$ .
(12) The single-irrep integral $\int d(I,\hat g)|\chi_j|^2\,d\mu=\frac34$ for $j=1$ and $\frac12$ for $j\ge2$ .
(13) $\int d(I,\hat g)\chi_{2k}\overline{\chi_{2l}}\,d\mu=\frac12\delta_{k,l}-\frac14\delta_{k,l-1}-\frac14\delta_{k-1,l}$ .
Schur orthogonality. A published theorem.
Normalization. $M^T$ integrates to the identity.
(14) The exact error formula, its lower bound and equality.
(11) Bužek's optimum $\sin^2\frac{\pi}{2(n+2)}$ in exact form.

Significance

The result. The error of a covariant SU(2) measurement on this space equals, coefficient by coefficient, the error of a covariant phase measurement. Eq. (13) says that the SU(2) character integral has the same tridiagonal kernel as the phase-estimation identity (7). Optimizing the input therefore becomes the largest-eigenvalue problem for a path graph, and that problem has a closed-form solution. With $n=2d-1$ uses, the protocol reaches error $\sin^2(\pi/(n+3))\sim\pi^2/n^2$ . This beats the $1/n$ rate of independent uses, and the paper gives the explicit constant. Chiribella, D'Ariano and Sacchi later showed that $v(x)$ is optimal over all measurements; the present paper does not prove that.

Formalizing it. No part of this computation is machine-checked yet:

the Weyl integration formula for $\mathrm{SU}(2)$ ;
the character integrals (12)–(13);
the covariant-POVM normalization;
the exact error identity;
the eigenvalue optimum and its limit.

The paper's own displays contain slips: the conjugation in (8), (9) and (14), the $j=1$ value on p. 9, the coefficients of the expansion on p. 10, and a quoted Bužek vector that is not the minimizer. A checked development fixes these.

Difficulty

The obvious route through (13) is to "expand the product of characters and keep the constant and $\cos\theta$ , $\cos2\theta$ terms", as p. 10 does. That route needs the Weyl integration formula. Mathlib has the Haar measure but no Weyl integration formula for $\mathrm{SU}(2)$ , no compactness instance on Matrix.specialUnitaryGroup, and no classification of its irreducible representations.

The reduction from the operator integral in (14) to the scalar integral (13) needs two further facts: Schur orthogonality on each pair of blocks, and the invariance of $\mu$ to move from $\hat g$ to $g^{-1}\hat g$ .

The optimum over inputs is a Perron–Frobenius problem for a path graph. It is easy to state with $\cong$ , but in exact form it needs the attained eigenvector $a_k\propto\sin(\pi(k+1)/(d+1))$ , not the vector the paper quotes.

Formalization scope

Representations.

$\mathrm{SU}(2)$ is Matrix.specialUnitaryGroup (Fin 2) ℂ.
The pinned Mathlib has no topological-group, compactness or measurable instances on it, so these are instance hypotheses (IsTopologicalGroup, CompactSpace, MeasurableSpace with BorelSpace).
$\mu$ is any left- and right-invariant probability measure dg.
Irreducible representations are the published BasedIrreps (based, continuous, unitary, irreducible), indexed $k=0,\dots,d-1$ for $\mathcal H_2,\dots,\mathcal H_{2d}$ .
A spin family requires dimension $2(k+1)$ and the Weyl character $U_{2k+1}(\operatorname{Re}\operatorname{Tr}g/2)$ . The character hypothesis is a true property of every such representation and is what the paper uses on p. 9.
The space, action and input are the published CanonicalIndex, canonicalAction and canonicalInput (with identity block unitaries).

Measurement and error.

Measurements are DensityPOVMs: a reference measure and a PSD operator density integrating to $I$ .
The cost is the published bellCost.
Probabilities are $\operatorname{Re}\operatorname{Tr}$ .
The error is pointwise in the true $g$ , as in the paper, not Haar-averaged.
In (14) the term with $x_0$ is absent.
The zero coefficient gets phase $1$ .

Ruled-out trivializations.

The irreducible representations are hypothesized, so clause 1 of the goal asserts that a spin family exists.
$T$ must be positive semidefinite with unit diagonal. Without the unit diagonal the seed is not normalized and the "error" can be made $0$ .
The error is not averaged over $g$ .
The optimum is stated with IsLeast, not sInf or ⨅.

Infrastructure. The reusable parts beyond this mission are:

Weyl integration for $\mathrm{SU}(2)$ , together with the compactness and topological-group instances;
the characters of the irreducible representations;
existence of the spin- $j/2$ representations (for example the published polynomial irreps Gap48.P23.polynomialIrrep);
the path-graph eigenvalue problem.

Proofs of any milestone, and of these supporting facts, are welcome.

Related work on the platform. The Chiribella–D'Ariano–Sacchi items of the Next46.P36 series pose related but different statements:

optimalPOVM and minimumEigenvalueInput concern a general compact group, a Haar-averaged risk, and optimality over all measurements.
cartesianFrameOptimum concerns SU(2) without a reference system, with a different cost.

This mission reuses their definition layer and their Schur orthogonality theorem. It states Hayashi's own reference-assisted protocol, with its exact pointwise error and the limit $\pi^2$ .

Not formalized. The following parts of the paper are out of scope:

the no-reference variant (pp. 8–9);
the even case $n=2d$ ;
§2's other phase-estimation results;
eqs. (16)–(17).

Selected references

M. Hayashi, Parallel Treatment of Estimation of SU(2) and Phase Estimation, arXiv:quant-ph/0407053v3 (2006). https://arxiv.org/abs/quant-ph/0407053
V. Bužek, R. Derka, S. Massar, Optimal Quantum Clocks, Phys. Rev. Lett. 82, 2207 (1999). https://arxiv.org/abs/quant-ph/9808042
G. Chiribella, G. M. D'Ariano, M. F. Sacchi, Optimal estimation of group transformations using entanglement, Phys. Rev. A 72, 042338 (2005). https://arxiv.org/abs/quant-ph/0506267
A. Fujiwara, Estimation of SU(2) operation and dense coding: an information geometric approach, Phys. Rev. A 65, 012316 (2002). https://doi.org/10.1103/PhysRevA.65.012316
A. Acín, E. Jané, G. Vidal, Optimal estimation of quantum dynamics, Phys. Rev. A 64, 050302 (2001). https://arxiv.org/abs/quant-ph/0012015
E. Bagan, M. Baig, R. Muñoz-Tapia, Entanglement-assisted alignment of reference frames using a dense covariant coding, Phys. Rev. A 69, 050303(R) (2004). https://arxiv.org/abs/quant-ph/0303019
G. Chiribella, G. M. D'Ariano, P. Perinotti, M. F. Sacchi, Efficient use of quantum resources for the transmission of a reference frame, Phys. Rev. Lett. 93, 180503 (2004). https://arxiv.org/abs/quant-ph/0405095

11 thms3 active usersReviewed

Linear algebra Quantum Error Correction Quantum Information·Captain: mikedeng1

Towards a Unified Framework for Approximate Quantum Error Correction: The Transpose Channel Corrects a Subsystem Code up to the Operator Norm of the PerturbationResearch Paper

Motivation

Quantum error correction protects quantum information from noise by storing it in a code and undoing the damage with a recovery operation. The textbook theory, the Knill–Laflamme conditions, characterizes codes that can be corrected perfectly. Real noise rarely admits perfect correction, and codes that are only approximately correctable can perform better than perfect ones: they can use fewer physical resources for a given target fidelity. Approximate quantum error correction (AQEC) asks for algebraic conditions that tell, from the noise and the code alone, how well a code can be corrected.

Mandayam and Ng (arXiv:1202.5139, Phys. Rev. A 2012) extend an earlier AQEC framework for subspace codes (Ng and Mandayam, arXiv:0909.0931, 2010) to subsystem codes, where information is stored in one tensor factor $A$ of a subspace $\mathcal H_A\otimes\mathcal H_B$ and the factor $B$ is a gauge whose state does not matter. Subsystem codes include noiseless subsystems and the Bacon–Shor family, and they are the natural setting for operator quantum error correction (Kribs, Laflamme and Poulin, arXiv:quant-ph/0412076, 2005).

Setting

The system space is $\mathcal H=\mathcal H_A\otimes\mathcal H_B\oplus\mathcal K$ , with $\mathcal H_A$ , $\mathcal H_B$ finite dimensional; $P$ is the projector onto $\mathcal H_{AB}=\mathcal H_A\otimes\mathcal H_B$ and $P_A,P_B$ the identities of the factors. The code $\mathcal C$ is the set of all product states $\rho_A\otimes\rho_B$ , with $\rho_A,\rho_B$ density operators.

The noise $\mathcal E$ is a completely positive, trace-preserving (CPTP) map with Kraus operators $E_1,\dots,E_N:\mathcal H_{AB}\to\mathcal H$ :

\mathcal E(\rho)=\sum_iE_i\rho E_i^\dagger,\qquad \sum_iE_i^\dagger E_i=P .

Write $\mathcal P_{\mathcal E}$ for the support of $\mathcal E(P)=\sum_iE_iE_i^\dagger$ . A recovery is a CP map $\mathcal R:\mathcal B(\mathcal P_{\mathcal E})\to\mathcal B(\mathcal H_{AB})$ that is trace preserving on $\mathcal P_{\mathcal E}$ .

The fidelity of states is $F(\rho,\sigma)=\mathrm{tr}\sqrt{\rho^{1/2}\sigma\rho^{1/2}}$ . The fidelity loss of the code state $\rho$ under $\mathcal E$ and $\mathcal R$ compares the information in $A$ before and after:

\eta_{\mathcal R}\{\rho\}=1-F^2\big(\mathrm{tr}_B\,\rho,\ \mathrm{tr}_B[(\mathcal R\circ\mathcal E)(\rho)]\big).

The code is $\epsilon$ -correctable on $A$ under $\mathcal E$ when some recovery has $\eta_{\mathcal R}\{\rho\}\le\epsilon$ for every $\rho\in\mathcal C$ .

The transpose channel $\mathcal R_P$ is the recovery with Kraus operators

R^P_i=P\,E_i^\dagger\,\mathcal E(P)^{-1/2},

the inverse square root being taken on the support of $\mathcal E(P)$ .

Formalization targets

Goal: Corollary 3

Suppose that, for all $i,j$ ,

PE_i^\dagger\mathcal E(P)^{-1/2}E_jP=P_A\otimes B_{ij}+\Delta_{ij}\qquad(12)

with $B_{ij}$ operators on $\mathcal H_B$ and $\Delta_{ij}$ operators on $\mathcal H_{AB}$ . Then the transpose channel is a recovery, and for every $\rho\in\mathcal C$

\eta_{\mathcal R_P}\{\rho\}\le\Big\|\sum_{ij}\Delta_{ij}^\dagger\Delta_{ij}\Big\|,

so $\mathcal C$ is $\epsilon$ -correctable on $A$ whenever $\epsilon\ge\|\sum_{ij}\Delta_{ij}^\dagger\Delta_{ij}\|$ (operator norm). The statement holds for every choice of the operators $B_{ij}$ ; each choice determines $\Delta_{ij}$ and gives a bound.

Theorem 2

Under (12), $\mathcal C$ is $\epsilon$ -correctable on $A$ for every $\epsilon\ge\eta_P$ , where

\eta_P=\max_{|\psi_A,\phi_B\rangle}\langle\phi_B|\sum_{ij}\Big[\langle\psi_A|\Delta^\dagger_{ij}\Delta_{ij}|\psi_A\rangle-\langle\psi_A|\Delta^\dagger_{ij}|\psi_A\rangle\langle\psi_A|\Delta_{ij}|\psi_A\rangle\Big]|\phi_B\rangle

is the fidelity loss of the transpose channel. Theorem 2 is sharper than Corollary 3; the corollary trades sharpness for a quantity that is easy to compute.

Milestones

The milestones follow the paper's own steps: the pure-state form (5) of the fidelity; the reduction of the worst case over $\mathcal C$ to pure product states; trace preservation of $\mathcal R_P$ on $\mathcal P_{\mathcal E}$ ; the trace-preservation identity of $\mathcal R_P\circ\mathcal E$ in terms of $B_{ij},\Delta_{ij}$ ; the fidelity formula (14) on pure product states; Theorem 2; and the bound of the expression (13) by the operator norm.

Significance

When all $\Delta_{ij}$ vanish, (12) is the paper's perfect-correction condition (Theorem 1), and the transpose channel is a perfect recovery. Corollary 3 quantifies the robustness of that statement: a perturbation of size $\|\sum\Delta^\dagger\Delta\|$ costs at most that much fidelity loss, with an explicit recovery. This turns the search for approximate subsystem codes into a check of a matrix inequality, and it supplies the sufficient half of a characterization whose necessary half (near-optimality of the transpose channel) the paper establishes only in restricted scenarios.

Status: the results are proved in the paper, not formalized. Prove2Me's catalog has no statement of Theorem 2, Corollary 3, or of perfect-correction conditions for subsystem codes. This mission states the subsystem-code model in Lean, with mixed code states and a possibly singular $\mathcal E(P)$ , and poses each step of the paper's proof as a target. The reduction to pure states needs the joint concavity of the fidelity, which Mathlib does not have; a proof of it is reusable across quantum information theory.

Difficulty

Two steps resist a direct computation. First, the code contains mixed product states, while the fidelity formula (14) is available only for pure ones; the passage from one to the other is the joint concavity of $F$ , a consequence of Uhlmann's theorem, not a linear-algebra identity. Second, $\mathcal E(P)$ need not be invertible: $\mathcal E(P)^{-1/2}$ is a pseudo-inverse, the transpose channel is trace preserving only on $\mathcal P_{\mathcal E}$ , and the trace-preservation identity of $\mathcal R_P\circ\mathcal E$ needs that each $E_j$ maps into $\mathcal P_{\mathcal E}$ . Arguments that treat $\mathcal E(P)^{-1/2}$ as an inverse are wrong in general.

Formalization scope

$\mathcal H_{AB}$ is indexed by a × b with $A$ first, matching ⊗ₖ and the published partial trace; $\mathcal H$ is a separate finite type o. The noise's Kraus operators are rectangular matrices Matrix o (a × b) ℂ, so $P$ , $P_A$ , $P_B$ are identity matrices and $P_A\otimes B_{ij}$ is 1 ⊗ₖ B i j.
Vectors are a → ℂ, unit when star ψ ⬝ᵥ ψ = 1; $|\psi\rangle\langle\psi|$ is vecMulVec ψ (star ψ).
Published definitions are reused: the fidelity (WildeQIT.fidelity $=F^2$ , rootFidelity $=F$ ), the partial trace WildeQIT.partialTraceRight, the channel action PeresTerno.krausUpdate, density matrices PeresTerno.IsDensityMatrix, and the support inverse square root and support projector QReversal.NearOpt.invSqrt, supportProj.
A recovery is any finite Kraus family $R_k$ from o to a × b with $\mathcal P_{\mathcal E}(\sum_kR_k^\dagger R_k)\mathcal P_{\mathcal E}=\mathcal P_{\mathcal E}$ . Full support of $\mathcal E(P)$ is not assumed.
$\epsilon$ -correctability is the existence of a recovery with fidelity loss at most $\epsilon$ on every code state; it is equivalent to the paper's $\epsilon\ge\eta_{\mathrm{op}}$ because the minimum defining $\eta_{\mathrm{op}}$ is attained. " $\epsilon\ge\eta_P$ " is stated as a bound on the expression (13) at every pair of unit vectors, with no supremum.
The norm in (15) is the operator norm, Mathlib's Matrix.Norms.L2Operator; neither the entrywise sup norm nor the Frobenius norm.

The statements carry no smallness hypothesis on $\Delta_{ij}$ , quantify over all code states including mixed ones rather than over pure states only, and admit only recoveries that are trace preserving on $\mathcal P_{\mathcal E}$ ; each of these restrictions would make the goal weaker or trivial.

Needed infrastructure: the continuous functional calculus identities for $X^{-1/2}XX^{-1/2}$ and for range inclusions of $\sum_iE_iE_i^\dagger$ , Kronecker-product algebra, and joint concavity (or Uhlmann's theorem) for the fidelity. Proofs of any milestone, and general fidelity lemmas usable beyond this mission, are welcome.

Selected references

P. Mandayam and H. K. Ng, Towards a unified framework for approximate quantum error correction, Phys. Rev. A 86, 012335 (2012). arXiv:1202.5139 (version v2 is the one formalized).
H. K. Ng and P. Mandayam, Simple approach to approximate quantum error correction based on the transpose channel, Phys. Rev. A 81, 062342 (2010). arXiv:0909.0931
D. Kribs, R. Laflamme and D. Poulin, Unified and generalized approach to quantum error correction, Phys. Rev. Lett. 94, 180501 (2005). arXiv:quant-ph/0412076
E. Knill and R. Laflamme, Theory of quantum error-correcting codes, Phys. Rev. A 55, 900 (1997). arXiv:quant-ph/9604034
H. Barnum and E. Knill, Reversing quantum dynamics with near-optimal quantum and classical fidelity, J. Math. Phys. 43, 2097 (2002). arXiv:quant-ph/0004088

14 thms3 active usersReviewed

Completed

Convex Optimization Discrete Geometry Operations Research·Captain: mikedeng1

Mixed-Integer Convex Representability: Closed Rational MICP-Representable Sets Whose Convex Subsets Have Bounded Diameter Are Finite Unions of Compact Convex and Closed Periodic SetsResearch Paper

Which sets can a mixed-integer convex program model?

Mixed-integer convex programming (MICP) optimizes over sets described by convex constraints together with the requirement that some variables be integers. Modern solvers handle such problems routinely, so a modeler who wants to optimize over a nonconvex set $S \subseteq \mathbb R^n$ asks a basic question first: can $S$ be written as the projection of the integer points of some closed convex set? This is the question of representability. For linear constraints with rational data it was settled by Jeroslow and Lowe in 1984: the rational MILP-representable sets are exactly the sets $\bigcup_{i=1}^k P_i + \mathrm{intcone}(U)$ with rational polytopes $P_i$ and a finite $U \subseteq \mathbb Z^n$ , so each is bounded or periodic (Theorem 1.1 of arXiv:1706.05135v3). For general convex constraints no comparable description exists, and the class is much richer: it contains unbounded sets that are neither periodic nor finite unions of convex sets.

Timeline:

1984, Jeroslow and Lowe characterize rational MILP-representable sets.
1987, Jeroslow shows that a set is pure binary MICP-R if and only if it is a finite union of closed convex sets sharing a common recession cone.
2018, Del Pia and Poskin characterize MICP-R sets under rational ellipsoidal restrictions on $M$ .
2017–2020, Lubin, Vielma and Zadik (arXiv:1706.05135v3, Mathematics of Operations Research 2022) give a binary characterization without recession-cone restrictions, a midpoint obstruction for the general case, and a structure theorem for rational MICP-representable sets, the subject of this mission.

Setting

Fix $n, p, d \in \mathbb Z_+ = \{0, 1, 2, \dots\}$ and write points of $\mathbb R^{n+p+d}$ as $(x, y, z)$ . A closed convex set $M \subseteq \mathbb R^{n+p+d}$ induces an MICP formulation of $S \subseteq \mathbb R^n$ when

x \in S \iff \exists\, y \in \mathbb R^p,\ z \in \mathbb Z^d:\ (x, y, z) \in M.

$S$ is MICP-R if such an $M$ exists, and binary MICP-R if moreover every point of $M$ with integer $z$ has $z \in \{0,1\}^d$ . The index set is $I = \mathrm{proj}_z(M)$ , the projection of all of $M$ , and the $z$ -projected sets are $A_z = \{x : \exists y,\ (x, y, z) \in M\}$ .

The recession cone of a set $C$ is $C_\infty = \{r : x + \lambda r \in C\ \forall x \in C,\ \lambda \ge 0\}$ . A set $I \subseteq \mathbb R^d$ is rationally unbounded if, for every $d'$ and every rational affine map $z \mapsto Az + b$ into $\mathbb R^{d'}$ , the image $I'$ is either bounded or has a nonzero integer recession direction. $S$ is rational MICP-R if it has a formulation whose index set is rationally unbounded; in the polyhedral and ellipsoidal special cases, exact characterizations were obtained only under such rationality assumptions.

A set $S$ is periodic if some $u \ne 0$ satisfies $x + \lambda u \in S$ for every $x \in S$ and $\lambda \in \mathbb N = \{1, 2, \dots\}$ . The diameter of $C \subseteq \mathbb R^n$ is $D(C) = \sup\{\|x - x'\|_2 : x, x' \in C\} \in [0, \infty]$ , and the MICP diameter of a formulation is $D_{\mathrm{MICP}}(M) = \sup_{z \in I \cap \mathbb Z^d} D(A_z)$ .

Formalization targets

Goal: Theorem 5.1

If $S \subseteq \mathbb R^n$ is closed and rational MICP-R, and there is a real $D$ with $D(C) \le D$ for every convex $C \subseteq S$ , then there are compact convex sets $C_1, \dots, C_{k_1}$ and closed periodic sets $S_1, \dots, S_{k_2}$ with

S = \Bigl(\bigcup_{j=1}^{k_1} C_j\Bigr) \cup \Bigl(\bigcup_{i=1}^{k_2} S_i\Bigr).

Milestones

The milestones follow the paper's proof (§6) in attack order:

Proposition 4.2: binary MICP-R sets are exactly finite unions of projections of nonempty closed convex sets, with the explicit lifted formulation (4.4).
Proposition 5.3 (finite-union clause): binary MICP-R sets are closed under finite unions.
Lemmas 6.3–6.7: the rational affine hull $\mathrm{aff}_{\mathbb Z}(I)$ and $I_{\mathbb Z} = I \cap \mathrm{aff}_{\mathbb Z}(I)$ ; unimodular alignment; a flatness dichotomy; rational changes of integer variables; slicing an index set.
Lemma 6.1: $S = S_0 \cup \bigcup_i S_i$ with $S_0$ binary MICP-R and each $S_i$ rationally formulated with an integer point in $\mathrm{relint}((I_i)_{\mathbb Z})$ .
Lemmas 6.8, 6.11–6.13: affine separation, width functions of the $z$ -projected sets, relaxing an integer variable along a recession direction, and periodic directions.
Lemma 6.2: binary MICP-R, or nearly periodic, or a formulation with one integer variable fewer.
Proposition 6.1: $S \subseteq S_0 \cup \bigcup_i T_i \subseteq \mathrm{cl}(S)$ with $S_0$ binary MICP-R and each $T_i$ nearly periodic.

Significance

Theorem 5.1 is the paper's structural result for rational MICP-R sets. It shows that the set $\{x \in \mathbb Z : f(x\sqrt 2) \notin (0.4, 0.6)\}$ , $f(t) = t - \lfloor t \rfloor$ , is not rational MICP-R although it is MICP-R, characterizes the compact rational MICP-R sets (for them binary variables suffice), and separates rational MICP from rational MILP on subsets of $\mathbb N$ (Propositions 5.4, 5.5). It also gives modelers a necessary condition to check before attempting a formulation.

The results are proved on paper; none of them, and none of the representability notions, has a machine-checked formalization that we know of. The mission produces the definitional layer (formulations, index sets, rational unboundedness, MICP diameter, rational affine hulls) and the full chain of §6, which reuses general facts from convex analysis and the geometry of numbers: unimodular alignment of lattice subspaces, a flatness theorem, and separation of convex and concave functions.

Difficulty

The obvious induction removes integer variables one at a time by relaxing an unbounded integer direction. It breaks in two places. First, relaxing a direction $r$ can merge the sets $A_z$ along $z + r\mathbb R$ into a set of unbounded diameter; the proof must show that this happens only when the formulation is nearly periodic, which needs the width functions of Lemma 6.11 and the uniqueness of the asymptotic direction in Lemma 6.13. Second, slicing an index set by $z_1 = i$ can destroy rational unboundedness, so the slices must be built by rational shrinking maps (Lemma 6.7) and the integrality of $I_{\mathbb Z}$ must be maintained by a flatness argument (Lemma 6.5). Because the index set is a projection of a closed set, it need not be closed, and its plain recession cone differs from that of its closure; the argument has to work with non-closed convex sets throughout.

Formalization scope

Points $x$ live in EuclideanSpace ℝ (Fin n), auxiliaries in Fin p → ℝ, integer variables in Fin d → ℝ with the lattice $\mathbb Z^d$ as the image of Fin d → ℤ. Closedness and convexity of $M$ are part of "induces". Diameters are extended Euclidean diameters (Metric.ediam, value $+\infty$ on unbounded sets), and $D_{\mathrm{MICP}}$ is valued in $[0, \infty]$ . Rational affine maps are $\mathbb Q$ -matrices with $\mathbb Q$ -offsets; rational unboundedness quantifies over every target dimension $d'$ . The recession cone is that of the set itself (the published Grunbaum2003.characteristicCone). Affine dimensions are integers with $\dim \emptyset = -1$ ; relative interiors are intrinsicInterior; extended-real support functions use EReal. Coordinates are $0$ -based.

Three statements carry a disclosed change: Lemma 6.4 adds $F \cap \mathbb Z^d \ne \emptyset$ (as printed it fails for $\{z_1 = 1/2\}$ ), Lemma 6.7 adds $\dim \mathrm{aff}_{\mathbb Z}(I) \ge 1$ (as printed it fails in dimension $0$ ), and Lemma 6.12 reads the $z$ -projected sets of the new formulation at integer indices.

Trivializing encodings are ruled out: the diameter is not Metric.diam (which is $0$ on unbounded sets), rational unboundedness is not tested on $I_\infty$ alone, periodicity requires $u \ne 0$ , the index set is the projection of all of $M$ , and $k_1, k_2$ are finite.

Contributions are welcome at every level: the binary characterization and the union lemma are self-contained; Lemmas 6.3–6.5 and 6.8 are reusable geometry-of-numbers and convex-analysis facts; proofs of Lemmas 6.1, 6.2 and Proposition 6.1 assemble them.

Selected references

M. Lubin, J. P. Vielma, I. Zadik, Mixed-integer convex representability, Mathematics of Operations Research, 2022; arXiv:1706.05135v3. https://arxiv.org/abs/1706.05135v3
R. G. Jeroslow, J. K. Lowe, Modeling with integer variables, Mathematical Programming Studies 22, 167–184, 1984 (reference [31] of arXiv:1706.05135v3).
R. G. Jeroslow, Representability in mixed integer programming, I: characterization results, Discrete Applied Mathematics 17(3), 223–243, 1987 (reference [32] of arXiv:1706.05135v3).
R. T. Rockafellar, Convex Analysis, Princeton University Press, 1970. https://doi.org/10.1515/9781400873173
A. Basu, M. Conforti, G. Cornuéjols, G. Zambelli, Maximal lattice-free convex sets in linear subspaces, Mathematics of Operations Research 35(3), 2010. https://doi.org/10.1287/moor.1100.0461

29 thms3 active usersReviewed

Algorithmic Game Theory Operations Research Probability·Captain: mikedeng1

Approximation and Convergence of Large Atomic Congestion Games: Equilibria of Bernoulli Congestion Games Converge to Poisson Flows Whose Means Are Wardrop Equilibria of a Limit GameResearch Paper

Motivation

Traffic models in transportation and network design come in two kinds. Nonatomic congestion games, with Wardrop equilibria, treat traffic as a continuum of infinitesimal users. Atomic games have finitely many players, each with a non-negligible effect on congestion. The Wardrop model is the one used in practice, and the usual justification is that it is the limit of atomic games as the number of players grows. Cominetti, Scarsini, Schröder and Stier-Moses (arXiv:2001.02797v7, forthcoming in Mathematics of Operations Research) make this precise in two regimes. In the first, the players' weights vanish. In the second, each player is present only with a small probability.

This mission is about the second regime, Bernoulli congestion games. Each of many potential users takes part only with a small probability, for example a commuter who may or may not travel on a given day. The limit is a Wardrop model for the mean flows, but with modified costs, and the flows themselves stay random: they are Poisson. This links Wardrop equilibria with Myerson's Poisson games (Myerson 1998).

Setting

A congestion structure consists of a finite set $\mathcal E$ of resources, each with a cost $c_e:\mathbb N^*\to\mathbb R_+$ that is nonnegative and weakly increasing on $\mathbb N^*=\{1,2,\dots\}$ , and a finite set $\mathcal T$ of types. Each type $t$ has a nonempty family $\mathcal S_t\subseteq 2^{\mathcal E}$ of feasible strategies.

In the nonatomic game with demands $d=(d_t)_t$ , a strategy flow $y=(y_{t,s})$ and a load vector $x=(x_e)$ are feasible, $(y,x)\in\mathcal F(d)$ , when $d_t=\sum_{s\in\mathcal S_t}y_{t,s}$ , $y_{t,s}\ge0$ and $x_e=\sum_t\sum_{s\in\mathcal S_t}y_{t,s}\mathbb 1_{\{e\in s\}}$ . A feasible pair is a Wardrop equilibrium for costs $C_e$ when every used strategy is cheapest: $\hat y_{t,s}>0$ implies $\sum_{e\in s}C_e(\hat x_e)\le\sum_{e\in s'}C_e(\hat x_e)$ for all $s,s'\in\mathcal S_t$ .

A Bernoulli congestion game $\Gamma_B$ has finitely many players $i$ , each with a type $t_i$ and a participation probability $u_i\in(0,1]$ . Player $i$ plays a mixed strategy $\sigma_i$ on $\mathcal S_{t_i}$ and is present ( $U_i=1$ ) with probability $u_i$ , independently of the other players. The random flows and loads are

Y_{t,s}=\sum_{i:t_i=t}U_i\mathbb 1_{\{S_i=s\}},\qquad X_e=\sum_iU_{i,e},\qquad U_{i,e}=U_i\mathbb 1_{\{e\in S_i\}},

with means $y_{t,s}=\sum_{i:t_i=t}u_i\sigma_i(s)$ and $x_e=\sum_iu_i\sigma_{i,e}$ . A present player on resource $e$ pays $c_e(1+Z_{i,e})$ , where $Z_{i,e}=\sum_{j\ne i}U_{j,e}$ is the load of the others. A profile $\hat\sigma$ is a Bayesian Nash equilibrium when every strategy in its support minimizes $\sum_{e\in s}\mathsf E_{\hat\sigma}[c_e(1+Z_{i,e})]$ .

The limit game $\breve\Gamma^\infty$ is the nonatomic game with the same demands and the auxiliary costs

\breve c_e(x)=\mathsf E[c_e(1+X)],\qquad X\sim\mathrm{Poisson}(x).

Formalization targets

Goal: Theorem 2

Consider a sequence $\Gamma^n_B$ with $|\mathcal N^n|\to\infty$ , $u^n=\max_iu^n_i\to0$ and $d^n_t=\sum_{i:t^n_i=t}u^n_i\to d_t$ (14). Assume condition (18): there are $\nu$ and $d_{\max}>\sum_td_t$ with $\mathsf E|\Delta^2c_e(1+V)|\le\nu$ for all $e$ , where $V\sim\mathrm{Poisson}(d_{\max})$ and $\Delta^2c_e(k)=c_e(k+2)-2c_e(k+1)+c_e(k)$ . For every sequence of Bayesian Nash equilibria $\hat\sigma^n$ :

(\hat y^n,\hat x^n)\ \text{bounded},\qquad (\hat y,\hat x)=\lim_k(\hat y^{\varphi(k)},\hat x^{\varphi(k)})\ \Rightarrow\ (\hat y,\hat x)\in\mathsf{WE}(\breve\Gamma^\infty),

and along that subsequence $Y^n_{t,s}\to\mathrm{Poisson}(\hat y_{t,s})$ jointly and independently, and $X^n_e\to\mathrm{Poisson}(\hat x_e)$ , in total variation.

Milestones

The milestones are the results the proof of Theorem 2 uses, in attack order:

the Poisson–Poisson total-variation bound (46);
the Barbour–Hall bound, Theorem 9(a);
the limit theorem for arbitrary profiles, Proposition 1;
the Poisson-moment facts, Propositions 5(a)–(b);
the smoothness of Poisson mixtures, Proposition 6(b), and the derivative bound, Corollary 5(a);
the Borisov–Ruzankin bound, Theorem 9(b);
Lemma 1 in two parts: the regularity of $\breve c_e$ , and the uniform approximation (21) of a player's expected cost by $\breve c_e(x_e)$ , with a corrected constant (see Formalization scope).

Significance

Theorem 2 justifies a Wardrop description for large games with rare participation, and it says which Wardrop model. The costs are not $c_e$ but their Poisson averages $\breve c_e$ , which account for the player's own presence and for the randomness of the others. The theorem also describes the fluctuations: flows are asymptotically independent Poisson variables, while loads are Poisson but correlated. The paper builds its approximation rates (§6) and its price-of-anarchy convergence results (§7) on the same Poisson calculus.

The result is proved in the paper. As far as is known, none of it is formalized. Mathlib has the Poisson distribution but no Poisson approximation of Bernoulli sums. The platform has nonatomic routing models and one-variable Chen–Stein bounds, but no Bernoulli players and no convergence-of-equilibria theorem. Formalizing the mission therefore produces:

a checked Barbour–Hall bound and Poisson–Poisson total-variation bound;
a calculus of Poisson mixtures (integrability transfer, smoothness, derivative bounds);
the first machine-checked limit theorem from atomic equilibria to Wardrop equilibria.

Difficulty

The obvious approach is to say that Bayesian Nash equilibrium inequalities pass to the limit because the expected costs converge. That step fails without control on $c_e$ : the costs are unbounded and evaluated at random loads, so convergence of the laws in total variation does not give convergence of $\mathsf E[c_e(1+Z_{i,e})]$ . Condition (18) supplies the integrability, and the error must be bounded uniformly in the player and the profile. The Borisov–Ruzankin bound gives this, but at the Poisson parameter $z_{i,e}$ rather than at $d_{\max}$ , so integrability has to be transferred between Poisson parameters. The other difficulties are independence of the limit flows, which is a joint statement on $\mathbb N^{\{(t,s)\}}$ , and differentiating series in their Poisson parameter up to the end point $d_{\max}$ .

Formalization scope

Model. Players are Fin N, strategies are Finset E, and types and resources are finite types. Costs are c : E → ℕ → ℝ, nonnegative and monotone on $\{k\ge1\}$ ; $c_e(0)$ is never read. The page prints $c_e:\mathbb N_+\to\mathbb N_+$ and $\nu\in\mathbb N$ , which are read as real-valued, the weaker hypothesis. Nonempty $\mathcal S_t$ is made explicit.
Probability space. $\Omega=(\{0,1\}\times 2^{\mathcal E})^{\mathcal N}$ carries the product weights $\prod_i\mathsf P_i(\omega_i)\sigma_i(s_i)$ . Expectations are finite sums, and the laws of flows, loads and the flow vector are image measures. Laws are therefore computed from $u$ and $\sigma$ , never passed in as free measures.
Total variation. Total variation is the published MarkovChainCLT.tvDist, the supremum over events (15). Poisson laws are Mathlib's poissonMeasure.
Accumulation points are limits along a strictly increasing $\varphi$ .
Independence. "The $Y_{t,s}$ are independent" is formalized as total-variation convergence of the joint law of $(Y^n_{t,s})$ to the product of Poisson laws. On a countable space this is equivalent to the joint convergence in distribution that the paper proves.
Junk values. Every expectation that is a series carries summability: in (18), Propositions 5–6, Corollary 5 and Theorem 9(b). Without it, a cost such as $c_e(k)=k!$ would satisfy (18) through Lean's value $0$ for a divergent tsum, and Theorem 2 would become false. Derivatives are taken within $[0,d_{\max}]$ . Lemma 1 and Theorem 9 assume $u<1$ and $p<1$ , so that $(1-u)^{-2}$ is not Lean's $1/0=0$ .
Correction to Lemma 1 (21). As printed, (21) is false. Take one resource with $c_e(j)=403(j-2)^+$ , $\nu=1$ , $d_{\max}=6$ and 300 players with $u_i=1/100$ . Then $|\mathsf E[c_e(1+Z_{i,e})]-\breve c_e(3)|=4.1311>\Lambda(1/100)=4.0552$ . The mission states (21) with $\tilde\Lambda(u)=\frac{\nu d_{\max}e^{d_{\max}}}{2}\frac{ue^u}{(1-u)^2}+u\zeta$ , which is what the paper's proof gives once Proposition 5(a) transfers (18) to the parameter $z_{i,e}$ . It adds the counterexample as a separate item. Theorem 2 needs only $\tilde\Lambda(u)\to0$ and is unaffected.
Not trivializable. The goal cannot hold vacuously: the hypotheses are met by one resource, one type, $n+1$ players with $u_i=1/(n+1)$ and linear costs, for which every profile is an equilibrium (checked in Lean).
Contributions. Contributions toward any milestone are welcome. The Poisson-approximation and Poisson-mixture results (Theorem 9, (46), Propositions 5–6, Corollary 5) do not depend on the game and can be reused elsewhere.
Out of scope. Weighted games (Theorem 1), Poisson games (Theorems 3–4), rates (§6) and price of anarchy (§7) are not part of this mission.

Selected references

R. Cominetti, M. Scarsini, M. Schröder, N. Stier-Moses, Approximation and Convergence of Large Atomic Congestion Games, Mathematics of Operations Research (forthcoming), arXiv:2001.02797v7, 2022. https://arxiv.org/abs/2001.02797
A. D. Barbour, P. Hall, On the rate of Poisson convergence, Math. Proc. Cambridge Philos. Soc. 95(3), 1984. https://doi.org/10.1017/S0305004100061806
I. S. Borisov, P. S. Ruzankin, Poisson approximation for expectations of unbounded functions of independent random variables, Annals of Probability 30(4), 2002. https://doi.org/10.1214/aop/1039548369
J. A. Adell, A. Lekuona, Sharp estimates in signed Poisson approximation of Poisson mixtures, Bernoulli 11(1), 2005. https://doi.org/10.3150/bj/1110228242
R. B. Myerson, Population uncertainty and Poisson games, International Journal of Game Theory 27, 1998. https://doi.org/10.1007/s001820050079
J. G. Wardrop, Some theoretical aspects of road traffic research, Proceedings of the Institution of Civil Engineers, Part II, 1, 325–378, 1952 (no DOI given in the paper).

14 thms3 active usersReviewed

Combinatorics Operations Research Optimization·Captain: mikedeng1

M♮-Convexity and Its Applications in Operations: Optimal Solutions Are Nonincreasing in the Parameters for SSQM♮-Concave Objectives on a BoxResearch Paper

Motivation

Many operations models ask how an optimal decision moves when a parameter moves. The classical answer is lattice programming (Topkis 1998): when the objective is supermodular, so that decisions and parameters are complements, optimal solutions are nondecreasing in the parameters. Inventory, assortment and resource-allocation problems often have the opposite structure. Stock already on hand, capacity already committed, or a budget already spent substitutes for new decisions, and one expects optimal decisions to be nonincreasing in such parameters. Supermodularity cannot express substitution between several decision variables at once, and before the work of Chen and Li no general tool covered this case.

Xin Chen and Menglong Li (SSRN 3431474; Operations Research, 2021, doi:10.1287/opre.2020.2070) supply that tool. They take the M♮-convex functions of discrete convex analysis (Murota 2003) and a quasi version of them, and show that maximizing a concave function of this kind over a box gives optimal solutions that decrease in the parameters. The paper then applies the result to multi-product inventory control with substitutable demand and to portfolio contracts.

Setting

All vectors here are integer vectors. For a finite index set $K$ , write $\mathbf e_i$ for the $i$ -th unit vector of $\mathbb Z^K$ and $\mathbf e_0 = 0$ . For $x, y \in \mathbb Z^K$ , $\operatorname{supp}^+(x-y) = \{k : x_k > y_k\}$ and $\operatorname{supp}^-(x-y) = \{k : x_k < y_k\}$ .

A function $G : \mathbb Z^K \to \mathbb R \cup \{-\infty\}$ has effective domain $\operatorname{dom} G = \{x : G(x) > -\infty\}$ . It is SSQM♮-concave (semistrictly quasi M♮-concave; Definition 1, p. 8, applied to $-G$ ) if for all $x, y \in \operatorname{dom} G$ and every $i \in \operatorname{supp}^+(x-y)$ there are $j \in \operatorname{supp}^-(x-y) \cup \{0\}$ and an integer $\alpha_0 > 0$ such that for every integer $\alpha \in [0, \alpha_0]$ , writing $d = \mathbf e_i - \mathbf e_j$ ,

G(x - \alpha d) > G(x) \quad\text{or}\quad G(y + \alpha d) > G(y) \quad\text{or}\quad G(x - \alpha d) = G(x),\ G(y + \alpha d) = G(y).

Every M♮-concave function is SSQM♮-concave, and so is every strictly increasing transform of one.

The parametric problem (3), p. 10, has a parameter $s \in \mathbb Z^m$ , a decision $a \in \mathbb Z^n$ , and an objective $G : \mathbb Z^m \times \mathbb Z^n \to \mathbb R \cup \{-\infty\}$ ; the value $-\infty$ encodes constraints beyond the box. A box is $B = [l, u] \cap \mathbb Z^n$ with $l_k \in \mathbb Z \cup \{-\infty\}$ , $u_k \in \mathbb Z \cup \{+\infty\}$ and $l \le u$ . The problem is

\max\ G(s, a) \quad\text{s.t. } a \in B,

and $\mathcal A^*_B(s)$ denotes its set of optimal solutions. A correspondence $s \mapsto \mathcal A(s)$ is nonincreasing on a set $S$ of parameters (the weak induced set ordering) if for all $s \le s'$ in $S$ , every $a \in \mathcal A(s)$ dominates some $a' \in \mathcal A(s')$ , and every $a' \in \mathcal A(s')$ is dominated by some $a \in \mathcal A(s)$ , with $\le$ componentwise.

Formalization targets

Goal: Theorem 3, p. 10

Let $G$ be SSQM♮-concave in $(s, a)$ and let $S$ be the set of parameters for which (3) has an optimal solution of finite value. Then for all $s, s' \in S$ with $s \le s'$ ,

\forall a \in \mathcal A^*_B(s)\ \exists a' \in \mathcal A^*_B(s'),\ a' \le a, \qquad \forall a' \in \mathcal A^*_B(s')\ \exists a \in \mathcal A^*_B(s),\ a' \le a .

Milestones (steps of the proof on p. 11)

Box feasibility. If $a, a' \in B$ , $a_i < a'_i$ and $j = 0$ or $a'_j < a_j$ , then $a' - (\mathbf e_i - \mathbf e_j)$ and $a + (\mathbf e_i - \mathbf e_j)$ lie in $B$ .
Exchange step. For optimal $a$ at $s$ and $a'$ at $s'$ with finite values and $a_i < a'_i$ , some admissible $j$ makes $a' - (\mathbf e_i - \mathbf e_j)$ optimal at $s'$ and $a + (\mathbf e_i - \mathbf e_j)$ optimal at $s$ , while preserving $a'_k \le a_k$ for $k < i$ .
Induction claim. $\mathcal A^*_B(s') \cap I_{\le,i}(a) \neq \emptyset$ for $i = 0, \dots, n$ , where $I_{\le,i}(a) = \{a' : a'_k \le a_k,\ k \le i\}$ .
First half. Some $a'' \in \mathcal A^*_B(s')$ satisfies $a'' \le a$ .
Second half. For every $a' \in \mathcal A^*_B(s')$ some $a \in \mathcal A^*_B(s)$ satisfies $a \ge a'$ .

Significance

Theorem 3 is the substitution counterpart of Topkis's monotonicity theorem. In the paper it yields Theorem 4 (for M♮-concave $G$ , also $\mathbf e^{\mathsf T}\mathcal A^*_B(s) + \mathbf e^{\mathsf T}s$ is nondecreasing, so a unit increase in the parameters lowers the total decision by at most one unit), and through Theorem 5 the monotone and bounded-sensitivity structure of optimal order quantities in multi-product inventory systems with substitution. Results of this shape are the usual route to structured optimal policies and to approximation and learning algorithms that exploit them.

The result is proved in the paper; it has not been formalized. The platform holds the discrete-convex-analysis vocabulary this mission reuses (characteristic vectors, positive and negative supports, effective domains of $\mathbb R \cup \{-\infty\}$ -valued functions, from Murota's book) and the supermodular, nondecreasing monotonicity theorems of Topkis, but no comparative-statics result for M♮-type objectives. A machine-checked Theorem 3 would be the base for formalizing Theorem 4 and the inventory application.

Difficulty

Topkis's argument compares $a$ and $a'$ through their meet and join, which is exactly what fails here: under substitution the meet and join of two optimal solutions need not be optimal. The exchange property gives a single unit move $\mathbf e_i - \mathbf e_j$ at a time, and that move may lower one coordinate while raising another. The difficulty is to organize such moves so that a whole vector inequality $a'' \le a$ is reached without undoing coordinates already fixed, and to handle objectives that take the value $-\infty$ , where the exchange property says nothing.

Formalization scope

Integers only. $\mathcal F = \mathbb Z$ . The paper's Assumption (⋆) (upper semicontinuity of $G$ ) is automatic there and does not appear. The real case is out of scope.
Finite optimal values. The paper takes $S = \{s : \mathcal A^*_B(s) \neq \emptyset\}$ . With that $S$ the theorem is false: for $m = n = 1$ , $B = [0, 1]$ , $G(s, a) = a$ if $s = 1$ and $-\infty$ otherwise, $G$ is SSQM♮-concave but $\mathcal A^*_B(0) = \{0, 1\}$ and $\mathcal A^*_B(1) = \{1\}$ . The formal $S$ (finiteParams) keeps only parameters with an optimal solution of finite value, which is what the proof uses. It is not strengthened to " $G$ finite on the box".
Encoding. $G$ is (Fin m ⊕ Fin n → ℤ) → WithBot ℝ with $\bot = -\infty$ ; the joint point $(s, a)$ is Sum.elim s a. The index $j = 0$ is none : Option K. The third alternative of Definition 1 is two equalities, equivalent to the paper's differences on $\operatorname{dom} G$ . The definition quantifies over every integer $\alpha \in [0, \alpha_0]$ , not one $\alpha$ . Box ends are WithBot ℤ and WithTop ℤ. Over $\mathbb Z$ the proof's "small $\alpha$ " is $\alpha = 1$ in the milestones.
No trivialization. The class SSQMNatConcave keeps $j \in \operatorname{supp}^- \cup \{0\}$ (restricting to $\operatorname{supp}^-$ gives Murota's narrower SSQM class), and the order in both halves is $a' \le a$ ; reversing either half gives the false nondecreasing statement. A sanity file checks that the hypotheses are satisfiable (the zero objective) and that the paper's $S$ fails on the example above.
Reused definitions. DiscreteConvex.MConvexFunctions.{CharVec, SuppPos, SuppNeg} and DiscreteConvex.EconomicEquilibrium.UDom. The SSQM♮-concave class, the box, $\mathcal A^*_B$ and the weak induced set ordering are new and reusable for Theorem 4 and the applications.

Contributions welcome: proofs of the milestones, and formalizations of Proposition 1 (M♮-concave implies SSQM♮-concave) and Theorem 4.

Selected references

Xin Chen and Menglong Li, M♮-Convexity and Its Applications in Operations, Operations Research, 2021; preprint SSRN 3431474. https://ssrn.com/abstract=3431474 , https://doi.org/10.1287/opre.2020.2070
Kazuo Murota, Discrete Convex Analysis, SIAM Monographs on Discrete Mathematics and Applications, 2003. https://doi.org/10.1137/1.9780898718508
Kazuo Murota and Akiyoshi Shioura, Quasi M-convex and L-convex functions — quasiconvexity in discrete optimization, Discrete Applied Mathematics 131(2):467–494, 2003 (cited by Chen and Li, p. 8).
Donald M. Topkis, Supermodularity and Complementarity, Princeton University Press, 1998. https://doi.org/10.1515/9781400822539

11 thms3 active usersReviewed

Operations Research Probability Stochastic Systems·Captain: mikedeng1

To Pool or Not to Pool: Queueing Design for Large-Scale Service Systems: In Moderate Overload, Dedicated Queues Under JSQ Match Pooled Abandonment While Their Delay Probability Stays Below OneResearch Paper

Motivation

Large service systems (call centers, hospital wards, emergency departments) must decide how customers wait. In a pooled queue (PQ) all customers wait in one line served by $n$ agents; in dedicated queues (DQ) each server has its own line, which is what physical layouts, server-specific information and accountability often force. Classical queueing theory says pooling is more efficient: an idle server never coexists with a waiting customer. Cao, He, Huang and Liu (Operations Research, 2020) show that when customers may abandon and join the shortest queue, the efficiency loss of dedicated queues vanishes in large systems, and that in moderate overload the dedicated design has a strictly better delay probability than the pooled one. Service-level contracts are written in terms of this probability, so the comparison bears directly on staffing and design decisions.

Setting

There are $n$ servers. Customers arrive in a Poisson process of rate $\lambda$ ; service times are exponential with mean $1/\mu$ ; each waiting customer has an exponential patience time with mean $1/\theta$ and leaves when its wait exceeds it. The traffic intensity is $\rho = \lambda/(n\mu)$ .

In the DQ–JSQ system each arriving customer joins a server with the fewest customers and stays in that server's FCFS queue. Let $Q_i$ be the number of servers with at least $i$ customers. $Q = (Q_i)_{i \ge 1}$ is a continuous-time Markov chain (genAb): an arrival joins a server with exactly $i$ customers when $Q_1 = \dots = Q_i = n > Q_{i+1}$ , and each of the $Q_i - Q_{i+1}$ servers with exactly $i$ customers loses one at rate $\mu + \theta(i-1)$ . The PQ system is the M/M/n+M (Erlang-A) queue with the same $\lambda, \mu, \theta$ .

The potential waiting time (PWT) $W$ is the time a customer would wait for service if it never abandoned; the actual waiting time (AWT) is $V = W \wedge R$ , with $R$ the customer's patience. A customer who joins a server with $i$ customers has PWT distributed as $T_a(i)$ , a sum of independent exponentials with rates $\mu, \mu + \theta, \dots, \mu + (i-1)\theta$ .

Along a sequence of systems with arrival rates $\lambda_n$ and $\lambda_n/(n\mu) \to \rho$ (condition (21)), the fluid constants are

q = \frac{\mu(\rho - 1)^+}{\theta}, \qquad \bar q = \lfloor q \rfloor + 1, \qquad r = q - \lfloor q \rfloor,

and the moderate overload condition (1) is $1 < \rho < 1 + \theta/\mu$ , equivalently $0 < q < 1$ .

Formalization targets

Goal: Theorem 5

Under (21) and (1), with $w = \ln(\rho)/\theta$ , nine pairs of steady-state limits hold as $n \to \infty$ (subscripts D and P for the two designs), among them

\lim P^n_D(\mathrm{Ab}) = \frac{\rho - 1}{\rho} = \lim P^n_P(\mathrm{Ab}), \qquad \lim P^n_D(\mathrm{De}) = \frac{r(\mu + \theta)}{\rho\mu} < 1 = \lim P^n_P(\mathrm{De}),

\lim \mathrm{Var}(W^n_D) = \frac{r(\mu + \theta)}{\rho\mu^3}\Bigl(2 - \frac{r(\mu + \theta)}{\rho\mu}\Bigr) > 0 = \lim \mathrm{Var}(W^n_P),

together with the limits of the mean occupancy, mean AWT, the conditional means of $W$ and $V$ , and mean PWT. The goal is the full nine-part statement as printed.

Milestones

The fluid model and its invariant state $q^*$ (Theorems 1 and 2), the steady-state limit $Q^n(\infty)/n \Rightarrow q^*$ (Theorem 3(ii)), the distribution of $T_a(i)$ ((22), (23)), the PWT limit

W^n \Rightarrow \chi\,T_a(\bar q) + (1 - \chi)\,T_a(\lfloor q \rfloor), \qquad P(\chi = 1) = \frac{r(\mu + \theta\bar q)}{\rho\mu}

(Theorem 4), its moderate-overload specialisation (Remark 3), and the pooled abandonment limit, already proved on the platform as ErlangA.Abandonment.theorem_1 (Garnett, Mandelbaum and Reiman, 2002).

Significance

The result separates two performance measures that are usually treated together. In moderate overload the two designs agree to first order in occupancy, abandonment and mean actual wait, so the capacity loss of dedicated queues is negligible; but the dedicated design lets a positive fraction $1 - p$ of customers enter service immediately, while in the pooled design almost every customer waits. The cost is fairness: delayed customers in dedicated queues wait about one full service time, and the PWT variance stays positive, whereas the pooled PWT concentrates at $w$ . These limits drive the staffing comparison of §6 of the paper.

All statements are proved in the paper's e-companion; none is formalized. The mission produces machine-checked versions of a fluid model with reflection-type constraints, an interchange-of-limits theorem for a countable-state chain with unbounded rates, hypoexponential distributions, and many-server limits of Erlang-A waiting times (Whitt, 2004), most of which are reusable across the many-server literature.

Difficulty

The pooled system is a birth–death chain with an explicit stationary law; the dedicated system is not. Its stationary law has no closed form, so the DQ limits cannot be computed directly. The natural approach, a process-level fluid limit followed by $t \to \infty$ , does not by itself give the steady-state statements: the two limits must be interchanged, which needs tightness of the stationary laws and global attraction to $q^*$ (Theorem 2). The fluid model itself is a reflection system in which $\bar U_i$ may grow only when $\bar Q_i = 1$ , so even its well-posedness (Theorem 1) is not a standard ODE result. Finally, weak convergence of $W^n$ (Theorem 4) does not yield convergence of means and variances without uniform integrability.

Formalization scope

The DQ–JSQ state space and the stationary-law predicate are the published JSQHalfinWhitt.Tightness.State (0-based: Lean q.1 i is $Q_{i+1}$ ) and IsStationaryDist (probability solutions of $\pi\mathcal G = 0$ ); the chain is non-explosive, so these are its stationary laws. The arrival rate in genAb is the total rate $\lambda$ .
The PQ stationary law is the published ErlangA.Abandonment.stationaryDist; $P_P(\mathrm{Ab})$ and $P_P(\mathrm{De})$ are the published probAbandon and probWait.
Waiting-time laws are measures on $\mathbb R$ (additive convolutions of expMeasure). The DQ PWT law is a definition: the arrival-seen mixture $\sum_i \pi\{\text{join a server with } i\}\,\mathcal L(T_a(i))$ (PASTA). Patience is an independent expMeasure θ; conditional means are ratios.
Fluid model: paper indices; (11)–(13), (15) for all $t \ge 0$ with the integral required to exist; (16) in integrated form; (14) as " $\bar U_i' = 0$ almost everywhere on $\{\bar Q_i < 1\}$ ". Uniqueness is asserted on $t \ge 0$ only.
Theorem 3(ii)'s " $\bar Q^n(t) \Rightarrow \bar Q^n(\infty)$ " is read as existence and uniqueness of the stationary law; convergence to $q^*$ is convergence in probability in the metric $d$ .
Added hypotheses: $\mu, \theta, \lambda_n > 0$ , and $\rho > 0$ for the fluid model.
A statement that holds because a quantity takes Lean's default value is ruled out: the goal also asserts, for every $n$ , that both PWT laws are probability laws with finite second moment and that both occupancy series converge, and the DQ laws are built from the stationary law of the chain, never from the limit mixture.

Contributions are welcome on the fluid model (Theorems 1–2), the hypoexponential facts ((22), (23)), the Erlang-A many-server limits, and the DQ–JSQ interchange of limits.

Selected references

P. Cao, S. He, J. Huang, Y. Liu, To Pool or Not to Pool: Queueing Design for Large-Scale Service Systems, Operations Research, Articles in Advance, 2020. https://doi.org/10.1287/opre.2019.1976
O. Garnett, A. Mandelbaum, M. Reiman, Designing a Call Center with Impatient Customers, Manufacturing & Service Operations Management 4(3), 2002. https://doi.org/10.1287/msom.4.3.208.7753
W. Whitt, Efficiency-Driven Heavy-Traffic Approximations for Many-Server Queues with Abandonments, Management Science 50(10), 2004. https://doi.org/10.1287/mnsc.1040.0279
A. Braverman, Steady-State Analysis of the Join-the-Shortest-Queue Model in the Halfin–Whitt Regime, Mathematics of Operations Research 45(3), 2020. https://doi.org/10.1287/moor.2019.1023

16 thms3 active usersReviewed

Completed

Convex Optimization Optimization Probability·Captain: mikedeng1

Complexity Analysis of a Sampling-Based Interior Point Method for Convex Optimization: Lower Bounds on the Smallest Eigenvalue of Boltzmann Covariance Matrices over a Convex BodyResearch Paper

Motivation

Interior point methods for convex optimization need a self-concordant barrier for the feasible set, and for many convex bodies, such as the subtour elimination polytope, membership can be decided in polynomial time while no efficiently computable barrier is known. The entropic barrier of Bubeck and Eldan (arXiv:1412.1587) is a self-concordant barrier defined for every convex body, and its gradient and Hessian are the mean and covariance of an exponential family of distributions on the body. Abernethy and Hazan (arXiv:1507.02528) proposed to run an interior point method with this barrier, estimating its derivatives by sampling. Badenbroek and de Klerk (arXiv:1811.07677) give a complexity analysis of such a sampling-based method when only a membership oracle for the body is available.

Any analysis of this kind has to control how badly conditioned the covariance matrices met along the way can be. Section 3.1 of Badenbroek and de Klerk supplies this control: a lower bound on the smallest eigenvalue of every Boltzmann covariance matrix over the body, in terms of the inner and outer radii of the body, the dimension, and the complexity parameter of the entropic barrier. This mission formalizes that section.

Setting

Fix $n\ge 0$ and work in $\mathbb R^n$ with the Euclidean inner product $\langle\cdot,\cdot\rangle$ and norm $\|\cdot\|$ . A convex body $K\subseteq\mathbb R^n$ is a compact convex set with non-empty interior. Throughout, $K$ contains a Euclidean ball of radius $r>0$ and is contained in a Euclidean ball of radius $R$ .

The log partition function of $K$ is

f(\theta)=\ln\int_K e^{\langle\theta,x\rangle}\,dx,\qquad \theta\in\mathbb R^n .

For each $\theta$ , the Boltzmann distribution over $K$ with parameter $\theta$ is the probability law on $K$ with density proportional to $e^{\langle\theta,x\rangle}$ ; at $\theta=0$ it is the uniform distribution on $K$ . Its mean is $\mathbb E_\theta[X]$ and its covariance matrix is

\Sigma(\theta)=\mathbb E_\theta\big[(X-\mathbb E_\theta[X])(X-\mathbb E_\theta[X])^\top\big],

which is also the Hessian of $f$ at $\theta$ . The local norm at $\theta$ is $\|v\|_\theta=\sqrt{\langle v,\Sigma(\theta)v\rangle}$ . For a symmetric positive semidefinite $A$ , $\lambda_{\min}(A)=\min_{\|v\|=1}\langle v,Av\rangle$ and $\lambda_{\max}(A)=\max_{\|v\|=1}\langle v,Av\rangle$ .

The entropic barrier is the Fenchel conjugate $f^*(x)=\sup_{\theta}\{\langle\theta,x\rangle-f(\theta)\}$ , for $x$ in the interior of $K$ . Its complexity parameter is a number $\vartheta$ with $Df^*(x)[h]\le\sqrt{\vartheta\,D^2f^*(x)[h,h]}$ for all interior $x$ and all directions $h$ ; the paper's $\vartheta$ is the least such number, $\sup_x\|g^*_x(x)\|^{*2}_x$ (Definition 2.2). It is known that $\vartheta=n+o(n)$ .

Formalization targets

Goal: Theorem 3.1

For every $\theta\in\mathbb R^n$ with $\|\theta\|\le\frac1{4R}$ ,

\lambda_{\min}(\Sigma(\theta))\ \ge\ \frac1{16}\Big(\frac r{n+1}\Big)^2,

and for every $\theta$ with $\|\theta\|>\frac1{4R}$ ,

\lambda_{\min}(\Sigma(\theta))\ \ge\ \frac1{64}\Big(\frac1{4R\|\theta\|}\Big)^{4\sqrt\vartheta+2}\Big(\frac r{n+1}\Big)^2 .

Milestones

In the order the proof uses them:

Display (12): $\lambda_{\max}(\Sigma(\theta))\le(2R)^2$ for all $\theta$ .
Lemma 3.1 (Kannan–Lovász–Simonovits): if $\Sigma(0)=I$ then $K$ lies in a Euclidean ball of radius $n+1$ .
Lemma 3.2: $\lambda_{\min}(\Sigma(0))\ge\frac14\big(\frac r{n+1}\big)^2$ .
Display (4): for $\|\theta_1-\theta_0\|_{\theta_0}<1$ and $v\ne0$ ,

1-\|\theta_1-\theta_0\|_{\theta_0}\le\frac{\|v\|_{\theta_1}}{\|v\|_{\theta_0}}\le\frac1{1-\|\theta_1-\theta_0\|_{\theta_0}} .

Display (13): $\|\theta\|_\theta^2\le\vartheta$ for all $\theta$ . This milestone is the already-published open statement EntropicBarrier.Universal.nuBound_iff_covariance, whose forward direction is (13).
Display (14): if $\|\theta\|\le\frac1{4R}$ then $\|\theta\|_0\le\frac12$ and $\|v\|_\theta\ge\frac14\frac r{n+1}\|v\|$ .
Display (15): along $\theta_k=(1-\frac1{2\sqrt\vartheta+1})^k\theta$ , consecutive points are within local distance $\frac12$ , and $\|v\|_\theta\ge 2^{-m}\|v\|_{\theta_m}$ .
The bound on $2^{-m-2}$ : with $m=\big\lceil\log_2(\frac1{4R\|\theta\|})/\log_2(1-\frac1{2\sqrt\vartheta+1})\big\rceil$ , one has $\|\theta_m\|\le\frac1{4R}$ and $2^{-m-2}\ge\frac18(4R\|\theta\|)^{1/\log_2(1-\frac1{2\sqrt\vartheta+1})}\ge\frac18(4R\|\theta\|)^{-2\sqrt\vartheta-1}$ .

Significance

The result. Theorem 3.1 bounds the condition number of every Boltzmann covariance over $K$ : together with display (12), it places the spectrum of $\Sigma(\theta)$ in an explicit interval depending only on $r$ , $R$ , $n$ , $\vartheta$ and $\|\theta\|$ . In the paper this enters the analysis of the interior point method (display (52) and Lemma 6.3), where sampled estimates of $\Sigma(\theta)$ must be accurate relative to the local norm. Lemma 3.2 on its own is a statement about the uniform distribution on a convex body that is of independent use in sampling and rounding algorithms.

Formalizing it. The results are proved in the paper, apart from Lemma 3.1 and display (4), which it cites (Kannan–Lovász–Simonovits 1995, Bubeck–Eldan 2014). None of them has been machine-checked. The mission builds on the published Lean layer of the Bubeck–Eldan entropic-barrier mission (convex bodies, the log partition function, the exponential family, its covariance form), so results proved here become reusable facts about that shared layer. The paper's headline, Theorem 6.2 (the complexity of the full sampling-based method), is not part of this mission: its complexity statement is asymptotic in $O^*$ form and its proof relies on results of other papers that the paper does not state.

Difficulty

The upper bound (12) is immediate, because $K$ has diameter at most $2R$ . The lower bound is not: the Boltzmann law concentrates near the boundary of $K$ in the direction of $\theta$ as $\|\theta\|$ grows, and no direct estimate of the variance in the other directions is available. Near $\theta=0$ the obstacle is the base case itself, which needs a quantitative statement that a convex body in isotropic position is not too elongated (Lemma 3.1). For large $\|\theta\|$ the obstacle is that self-concordance only compares local norms at parameters within local distance less than one, so a single comparison with $\theta=0$ is not possible, and the number of comparisons must be controlled through the complexity parameter. On the formal side, the identification of $\Sigma(\theta)$ with the Hessian of $f$ , the self-concordance of $f$ , and the relation between $\vartheta$ and $\|\theta\|_\theta$ all require differentiation under the integral sign over a convex body, which Mathlib supports only in pieces.

Formalization scope

Space. $\mathbb R^n$ is EuclideanSpace ℝ (Fin n) with Lebesgue measure; the inner product is the Euclidean one.
Objects reused, not redefined. IsConvexBody (compact, convex, non-empty interior), logPartition ( $f$ ), entropicBarrier ( $f^*$ ), expFamily K θ (the Boltzmann law), covForm K θ h k ( $\langle h,\Sigma(\theta)k\rangle$ ) and SatisfiesNuBound are the published Bubeck–Eldan definitions. New definitions: the local norm localNorm K θ v = √(covForm K θ v v), the sequence thetaSeq, and the step count mSteps (natural-number ceiling).
Spectral bounds. " $\lambda_{\min}(\Sigma(\theta))\ge c$ " is stated as $\langle v,\Sigma(\theta)v\rangle\ge c\|v\|^2$ for all $v$ , and " $\lambda_{\max}\le c$ " dually; no matrices or eigenvalue API are used.
Complexity parameter. $\vartheta$ enters as SatisfiesNuBound K (entropicBarrier K) ϑ with $\vartheta\ge0$ . This is equivalent to the paper's reading: the least admissible $\vartheta$ satisfies the predicate, and the second bound of Theorem 3.1 weakens as $\vartheta$ grows. Milestones 7 and 8 additionally require $\vartheta>0$ , since the argument divides by $2\sqrt\vartheta$ .
Balls. The inner ball is open, the outer one closed; for a compact $K$ this is no loss. In Lemma 3.1 the centre of the ball is existential, as printed.
Powers. $(\cdot)^{4\sqrt\vartheta+2}$ and $(\cdot)^{-2\sqrt\vartheta-1}$ are real powers, $2^{-m}$ and $2^{-m-2}$ integer powers, $\log_2$ is Real.logb 2.
Ruling out trivializations. The goal is about the covariance form of the given body $K$ , not about an abstract operator with assumed self-concordance or eigenvalue bounds, and $\vartheta$ is tied to the entropic barrier of $K$ rather than being an unconstrained real or a bound on $\|\theta\|_\theta$ assumed outright.
Infrastructure needed. Differentiation of $\theta\mapsto\int_K e^{\langle\theta,x\rangle}dx$ under the integral; positivity and finiteness of the moments of the Boltzmann law; the Kannan–Lovász–Simonovits ball bound for isotropic convex bodies; self-concordance of $f$ . The first two are reusable for any exponential-family statement on the platform. Proofs of the Bubeck–Eldan open statements, in particular nuBound_iff_covariance, directly serve milestone 5 and are welcome contributions.

Selected references

R. Badenbroek, E. de Klerk, Complexity Analysis of a Sampling-Based Interior Point Method for Convex Optimization, arXiv:1811.07677v1, 2018; Mathematics of Operations Research, 2022. https://arxiv.org/abs/1811.07677
S. Bubeck, R. Eldan, The entropic barrier: a simple and optimal universal self-concordant barrier, arXiv:1412.1587, 2014. https://arxiv.org/abs/1412.1587
J. Abernethy, E. Hazan, Faster convex optimization: Simulated annealing with an efficient universal barrier, arXiv:1507.02528, 2015. https://arxiv.org/abs/1507.02528
R. Kannan, L. Lovász, M. Simonovits, Isoperimetric problems for convex bodies and a localization lemma, Discrete & Computational Geometry 13 (1995), 541–559. https://doi.org/10.1007/BF02574061
J. Renegar, A Mathematical View of Interior-Point Methods in Convex Optimization, SIAM, 2001. https://doi.org/10.1137/1.9780898718812

14 thms3 active usersReviewed

Quantum Information·Captain: Goku

Quantum information can be negativeResearch Paper

Motivation

Given an unknown quantum state distributed over two systems, we determine how much quantum communication is needed to transfer the full state to one system. This communication measures the "partial information" one system needs conditioned on it's prior information. It turns out to be given by an extremely simple formula, the conditional entropy. In the classical case, partial information must always be positive, but we find that in the quantum world this physical quantity can be negative. If the partial information is positive, its sender needs to communicate this number of quantum bits to the receiver; if it is negative, the sender and receiver instead gain the corresponding potential for future quantum communication. We introduce a primitive "quantum state merging" which optimally transfers partial information. We show how it enables a systematic understanding of quantum network theory, and discuss several important applications including distributed compression, multiple access channels and multipartite assisted entanglement distillation (localizable entanglement). Negative channel capacities also receive a natural interpretation.

This mission is the statement-level formalization of Quantum information can be negative (arXiv:quant-ph/0505062v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Optimal state merging has signed cost S(A|B) (Unnumbered main result: optimal quantum state merging and negative information, PDF p. 2). 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

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

Application 1; Figure 2 and all-subset inequalities: An independently operational signed m-sender compression rate region with one decoder, local encoders, free classical messages, separate Bell input/output resources for every sender, and full purifying-reference reconstruction. (hard)
Application 2: noiseless coding with side information: A source-consistent definition of E_p(AU:R), including the correct purification/environment channel and one-copy versus regularized rate convention for the asserted one-way iff region. (source-ambiguity)
Application 3, equation (2): A two-coordinate signed quantum MAC transmission code with independent reference inputs, individually local encoders, one joint memoryless channel/decoder, explicitly charged sender-decoder Bell resources and the allowed classical messages. (hard)
Application 4, equation (3): An arbitrary-number-of-individually-local-helpers i.i.d. EPR-distillation protocol and its asymptotic rate threshold, without initial shared assistance or quantum helper collaboration. (hard)

Selected references

Quantum information can be negative, arXiv:quant-ph/0505062v1, https://arxiv.org/abs/quant-ph/0505062v1

17 thms3 active usersReviewed

Quantum Information·Captain: Goku

Quantum states representing perfectly secure bits are always distillableResearch Paper

Motivation

It is proven that recently introduced states with perfectly secure bits of cryptographic key (private states representing secure bit) [K. Horodecki et al., Phys. Rev. Lett. 94, 160502 (2005)] as well as its multipartite and higher dimension generalizations always represent distillable entanglement. The corresponding lower bounds on distillable entanglement are provided. We also present a simple alternative proof that for any bipartite quantum state entanglement cost is an upper bound on distillable cryptographic key in bipartite scenario.

This mission is the statement-level formalization of Quantum states representing perfectly secure bits are always distillable (arXiv:quant-ph/0602176v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Every exact nontrivial private state has positive GHZ distillable entanglement (Abstract; II.A–B, PDF p. 1). 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

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

II.B, last paragraph, suggested POVM extension: A complete multi-outcome locally orthogonal filtering instrument, with specified support notion, failure completion, admissible key-pair family and exact efficiency conclusion. (source-ambiguity)

Selected references

Quantum states representing perfectly secure bits are always distillable, arXiv:quant-ph/0602176v2, https://arxiv.org/abs/quant-ph/0602176v2

19 thms3 active usersReviewed

Quantum Information·Captain: Goku

Optimal quantum source coding with quantum information at the encoder and decoderResearch Paper

Motivation

Consider many instances of an arbitrary quadripartite pure state of four quantum systems ABCD. Alice holds the AC part of each state, Bob holds B, while D represents all other parties correlated with ABC. Alice is required to redistribute the C systems to Bob while asymptotically preserving the overall purity. We prove that this is possible using Q qubits of communication and E ebits of shared entanglement between Alice and Bob, provided that Q geq I(C;D|B)/2 and Q+E geq H(C|B), proving the optimality of the Luo-Devetak outer bound. The optimal qubit rate provides the first known operational interpretation of quantum conditional mutual information. We also show how our protocol leads to a fully operational proof of strong subadditivity and uncover a general organizing principle, in analogy to thermodynamics, that underlies the optimal rates.

This mission is the statement-level formalization of Optimal quantum source coding with quantum information at the encoder and decoder (arXiv:0706.2907v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 5 (Method of types): all simultaneous typical-projection bounds (Theorem 5 (Method of types): all simultaneous typical-projection bounds, PDF p. 4). 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

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

Theorem 1 (seed): exact quantum state-redistribution rate region: Source-preserving signed quantum/ebit redistribution achievability and exact operational region (hard)
Theorem 2: redistribution with generated qubits and ebits: Redistribution with separately generated forward identity channels and ebits (hard)
Theorem 3: redistribution with coherent communication: Redistribution with a coherently generated cobit channel (hard)
Theorem 4: robust one-shot redistribution protocol — source dimension defect: A uniquely specified normalized CPTP repair of the dimension-defective encoder in Theorem 4 (source-ambiguity)
Lemma 1 (Composition lemma [18]): Operational simulation of arbitrary finite resource bundles and their asymptotic composition (hard)
Lemma 2 (Cancellation lemma [18]): Operational resource addition/scaling and sublinear catalytic input (hard)
§V, unnumbered: optimal classical communication cost: Classical-only redistribution protocols with a finite entanglement trade (hard)
§I/§V, unnumbered: optimal successive redistribution: Composable two-step source-preserving redistribution and computed step costs (hard)
§V, unnumbered: pure bipartite source redistribution: Zero-rate redistribution with permitted sublinear communication (hard)
§V, unnumbered: flagged conditionally decoupled source cost: Flagged conditionally decoupled source construction and its operational cost (hard)
§V, unnumbered: redistribution with separate consumed and generated ebits: Source-preserving redistribution with distinct initial and final Bell resources (hard)

Selected references

Optimal quantum source coding with quantum information at the encoder and decoder, arXiv:0706.2907v2, https://arxiv.org/abs/0706.2907v2

20 thms3 active usersReviewed

Completed

Quantum Information·Captain: Goku

On the von Neumann capacity of noisy quantum channelsResearch Paper

Motivation

We discuss the capacity of quantum channels for information transmission and storage. Quantum channels have dual uses: they can be used to transmit known quantum states which code for classical information, and they can be used in a purely quantum manner, for transmitting or storing quantum entanglement. We propose here a definition of the von Neumann capacity of quantum channels, which is a quantum mechanical extension of the Shannon capacity and reverts to it in the classical limit. As such, the von Neumann capacity assumes the role of a classical or quantum capacity depending on the usage of the channel. In analogy to the classical construction, this capacity is defined as the maximum von Neumann mutual entropy processed by the channel, a measure which reduces to the capacity for classical information transmission through quantum channels (the "Kholevo capacity") when known quantum states are sent. The quantum mutual entropy fulfills all basic requirements for a measure of information, and observes quantum data-processing inequalities. We also derive a quantum Fano inequality relating the quantum loss of the channel to the fidelity of the quantum code. The quantities introduced are calculated explicitly for the quantum "depolarizing" channel. The von Neumann capacity is interpreted within the context of superdense coding, and an "extended" Hamming bound is derived that is consistent with that capacity.

This mission is the statement-level formalization of On the von Neumann capacity of noisy quantum channels (arXiv:quant-ph/9609024v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

21 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is von Neumann capacity of the Pauli depolarizing channel (V.A, (5.18): von Neumann capacity of the Pauli depolarizing channel, PDF p. 11). 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

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

VI.B, unnumbered weak-converse claim after (6.12): A fixed operational coding model, resource convention and rate unit, with a converse covering arbitrary degenerate/approximate block codes of fidelity tending to one. (source-ambiguity)

Selected references

On the von Neumann capacity of noisy quantum channels, arXiv:quant-ph/9609024v3, https://arxiv.org/abs/quant-ph/9609024v3

32 thms3 active usersReviewed

Quantum Information·Captain: Goku

"Squashed Entanglement" - An Additive Entanglement MeasureResearch Paper

Motivation

In this paper, we present a new entanglement monotone for bipartite quantum states. Its definition is inspired by the so-called intrinsic information of classical cryptography and is given by the halved minimum quantum conditional mutual information over all tripartite state extensions. We derive certain properties of the new measure which we call "squashed entanglement": it is a lower bound on entanglement of formation and an upper bound on distillable entanglement. Furthermore, it is convex, additive on tensor products, and superadditive in general. Continuity in the state is the only property of our entanglement measure which we cannot provide a proof for. We present some evidence, however, that our quantity has this property, the strongest indication being a conjectured Fannes type inequality for the conditional von Neumann entropy. This inequality is proved in the classical case.

This mission is the statement-level formalization of "Squashed Entanglement" - An Additive Entanglement Measure (arXiv:quant-ph/0308088v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

18 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Superadditivity and tensor-product additivity (§II, Proposition 4 (p.1 seed), PDF p. 3). 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.

Selected references

"Squashed Entanglement" - An Additive Entanglement Measure, arXiv:quant-ph/0308088v3, https://arxiv.org/abs/quant-ph/0308088v3

34 thms3 active usersReviewed

Completed

Quantum Information·Captain: Goku

Entanglement of Distillation and Conditional Mutual InformationResearch Paper

Motivation

In previous papers, we expressed the Entanglement of Formation in terms of Conditional Mutual Information (CMI). In this brief paper, we express the Entanglement of Distillation in terms of CMI.

This mission is the statement-level formalization of Entanglement of Distillation and Conditional Mutual Information (arXiv:quant-ph/0202144v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Common-cause classical laws have zero CMI (§2, Eq.(5), PDF p. 3). 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

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

§4, Eq.(32); abstract p.1: A source-supported theorem connecting an independently defined operational entanglement-of-distillation rate to the proposed two-input functional (32). (source-ambiguity)

Results already in Mathlib

These results of the paper are already proved in Mathlib, so they are not open goals here: InformationTheory.klDiv_comp_right_le.

Selected references

Entanglement of Distillation and Conditional Mutual Information, arXiv:quant-ph/0202144v2, https://arxiv.org/abs/quant-ph/0202144v2

15 thms3 active usersReviewed

Completed

Quantum Information·Captain: Goku

On the quantification of entanglement in infinite-dimensional quantum systemsResearch Paper

Motivation

We investigate entanglement measures in the infinite-dimensional regime. First, we discuss the peculiarities that may occur if the Hilbert space of a bi-partite system is infinite-dimensional, most notably the fact that the set of states with infinite entropy of entanglement is trace-norm dense in state space, implying that in any neighborhood of every product state there lies an arbitrarily strongly entangled state. The starting point for a clarification of this counterintuitive property is the observation that if one imposes the natural and physically reasonable constraint that the mean energy is bounded from above, then the entropy of entanglement becomes a trace-norm continuous functional. The considerations will then be extended to the asymptotic limit, and we will prove some asymptotic continuity properties. We proceed by investigating the entanglement of formation and the relative entropy of entanglement in the infinite-dimensional setting. Finally, we show that the set of entangled states is still trace-norm dense in state space, even under the constraint of a finite mean energy.

This mission is the statement-level formalization of On the quantification of entanglement in infinite-dimensional quantum systems (arXiv:quant-ph/0112064v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 10: no separable ball under a strict mean-energy bound (Proposition 10: no separable ball under a strict mean-energy bound (seed paper result), PDF p. 13). 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

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

Eq. (24): A valid source-supplied relative-entropy rate inequality under second-argument tensor-power approximation (source-ambiguity)
Eq. (27) and preceding identity: An unambiguous free-energy definition, entropy log base, inverse-temperature convention and correctly ordered Gibbs identity (source-ambiguity)

Selected references

On the quantification of entanglement in infinite-dimensional quantum systems, arXiv:quant-ph/0112064v3, https://arxiv.org/abs/quant-ph/0112064v3

21 thms3 active usersReviewed

Completed

Algorithmic Game Theory Linear algebra Operations Research·Captain: mikedeng1

Equilibria and Systemic Risk in Saturated Networks: necessary and sufficient conditions for uniqueness of saturated network equilibria, class by class, when the spectral radius is at most oneResearch Paper

Motivation

Many models of contagion in networks reduce to the same fixed-point equation: each node receives a linear combination of the states of its in-neighbours plus an exogenous term, and its own state is that inflow clipped to an interval. In the interbank clearing model of Eisenberg and Noe (Management Science, 2001) the states are payments capped by liabilities; in network games with strategic complementarities and bounded actions the states are best responses; in flow networks with finite capacities the states are flows. Massai, Como and Fagnani (arXiv:1912.04815, Mathematics of Operations Research) study this equation in a common form, with no sign restriction on the exogenous term and no normalisation of the interaction matrix. For a regulator or a modeller, the first question about such an equation is whether its solution is unique: when it is not, the outcome of a default cascade, or the play of a game, is not determined by the data.

Earlier uniqueness results covered special cases: Eisenberg and Noe proved uniqueness of the clearing vector under a regularity condition on the liability network, and contraction arguments give uniqueness when the interaction matrix has spectral radius below one. The paper treats every nonnegative interaction matrix with spectral radius at most one.

Setting

The nodes form a finite set $\mathcal V$ . A network is a pair $(P, w)$ with $P$ an entrywise nonnegative $\mathcal V \times \mathcal V$ matrix and $w$ a nonnegative vector; an exogenous flow is an arbitrary $c \in \mathbb R^{\mathcal V}$ . Writing $S_0^{w}$ for the coordinatewise clipping $(S_0^w(y))_i = \min\{\max\{y_i, 0\}, w_i\}$ , a network equilibrium is a solution of

x = S_0^w(P^\top x + c), \qquad\text{i.e.}\qquad x_i = \min\Big\{\max\Big\{\sum_j x_j P_{ji} + c_i,\ 0\Big\},\ w_i\Big\}.

The set of equilibria is $\mathcal X$ . The spectral radius $\rho(A)$ of a square matrix is the largest modulus of its complex eigenvalues. The digraph $\mathcal G_P$ has a link $i \to j$ when $P_{ij} \neq 0$ ; its strongly connected components are the classes of $P$ , and $P^{(ll)}$ denotes the principal block of $P$ on the class $\mathcal V_l$ . After a permutation of the nodes, $P$ is block upper triangular with these blocks on the diagonal. A class is basic if $\rho(P^{(ll)}) = \rho(P)$ and final if no link leaves it. A network is non-expansive if $\rho(P) < 1$ , or $\rho(P) = 1$ and every basic class is final. For an equilibrium $x$ , a node is surplus, exposed or deficit according as its inflow $c_i + \sum_k P_{ki}x_k$ lies above $w_i$ , in $[0, w_i]$ , or below $0$ .

Formalization targets

Goal: Theorem 2 (p. 16)

Assume $\rho(P) \le 1$ , let $\mathcal V_l$ be a class and fix the equilibrium on the nodes upstream of $\mathcal V_l$ . Put $u^{(l)} = c^{(l)} + \sum_{i<l} P^{(il)\top}x^{(i)}$ . Then the projection $x^{(l)}$ of the equilibria on $\mathcal V_l$ is

unique when $\rho(P^{(ll)}) < 1$ ;
when $\rho(P^{(ll)}) = 1$ , with right and left dominant eigenvectors $p^{(l)}$ , $\pi^{(l)}$ of $P^{(ll)}$ , non-unique if and only if

p^{(l)\top}u^{(l)} = 0, \qquad \min_{i \in \mathcal V_l}\frac{\nu^{(l)}_i}{\pi^{(l)}_i} + \min_{i \in \mathcal V_l}\frac{w_i - \nu^{(l)}_i}{\pi^{(l)}_i} > 0,

where $\nu^{(l)} = P^{(ll)\top}\nu^{(l)} + u^{(l)}$ ; and in that case the projections form the segment $\{\nu^{(l)} + \alpha\pi^{(l)}\}$ with $\alpha$ between minus the first minimum and the second.

The goal is a statement about $\mathcal X$ , the equilibria of the whole network, not about an isolated block.

Milestones

The milestones follow the paper's own chain of results:

Proposition 1 (i): $\mathcal X$ is a complete lattice.
Proposition 2: Perron–Frobenius facts for nonnegative and irreducible matrices.
Lemma 1 and Proposition 3: a positive vector $v$ with $Pv \le v$ exists if and only if the network is non-expansive.
Theorem 1 and Corollary 1: for non-expansive networks the surplus/exposed/deficit partition is the same for every equilibrium, and on it all equilibria solve one linear system.
Proposition 4: $\rho(P) < 1$ gives a unique equilibrium.
Proposition 5: the irreducible case with $\rho(P) = 1$ , where the equilibria are non-unique exactly when $p^\top c = 0$ and the segment condition (29) holds, and then form the segment (30).

Significance

Theorem 2 answers the uniqueness question completely for $\rho(P) \le 1$ , a range that contains every stochastic and sub-stochastic matrix and hence the standard interbank and flow-network models. It reduces uniqueness to finitely many checks, one per class, each a linear equation and two finite minima. It also shows that when uniqueness fails there is a continuum of equilibria (a segment on each critical class) rather than isolated ones, which is false for $\rho(P) > 1$ (Remark 9 of the paper). Theorem 1 says that, for non-expansive networks, which nodes are defaulting, solvent-but-exposed, or in surplus does not depend on the equilibrium selected; this is the robustness property the paper uses for systemic-risk measures.

None of these results has a machine-checked proof that we know of. The mission also produces reusable linear algebra: the Perron–Frobenius theorem for nonnegative matrices with the complex spectral radius (absent from Mathlib), its irreducible refinements, and the characterisation of matrices admitting a positive subinvariant vector.

Difficulty

The obvious argument is the contraction one: when $\rho(P) < 1$ the map $x \mapsto S_0^w(P^\top x + c)$ is a contraction in a suitable norm. At $\rho(P) = 1$ that argument fails, and non-uniqueness genuinely occurs. Even non-expansiveness in some norm is not enough: Example 1 of the paper has $\rho(P) = 1$ , a simple eigenvalue, and still an equilibrium-dependent partition, because a basic class is not final. The difficulty is to localise the critical behaviour to the classes of spectral radius one. It also needs the projection of the equilibrium set on a class, with its upstream values fixed, to be exactly the equilibrium set of a smaller irreducible network. Then the whole of $\mathcal X$ has to be identified with a segment of the kernel line of $I - P^{(ll)\top}$ intersected with a box.

Formalization scope

Nodes are a finite type with decidable equality. $P$ is a real matrix with nonnegative entries and $w$ a nonnegative vector, so $w_i = 0$ is allowed. The exogenous flow $c$ is unrestricted in sign. $\rho$ is Mathlib's spectralRadius ℂ of the complexified matrix (in $[0,\infty]$ ), never the real spectral radius. Equilibria are the solutions of (1) with $\min$ / $\max$ exactly as in (3). Classes are strongly connected components of $\mathcal G_P$ with reachability by paths of length at least zero, so a node on no cycle forms a class with block $[0]$ . Instead of assuming $P$ in block triangular form, the goal quantifies over a class and fixes the equilibrium on the nodes upstream of it. "Non-unique" is Set.Nontrivial. Minima over a class are Finset.inf' over a nonempty index set. Dominant eigenvectors are nonnegative, nonzero eigenvectors for the eigenvalue $1$ ; positivity of $\pi$ is not assumed.

Four printed slips are read as intended and disclosed in the items:

the sums $\sum_{k \ne i}$ in the partition (19) are the full sums of (1);
"connected components" on p. 10 are strongly connected components;
the third bullet of Theorem 2 sums over $i < l$ ;
Proposition 2 (iv) is stated as $\rho(P)x = P^\top x + c$ , which agrees with the printed equation when $\rho(P) = 1$ .

Several formalizations would trivialise the goal and are ruled out:

a block-only reading, in which the class projection is replaced by solutions of the block equation, is Proposition 5 again;
the real spectral radius makes the hypotheses depend silently on Perron–Frobenius;
assuming $c \ge 0$ , $w > 0$ , $P$ sub-stochastic or irreducible removes the cases the theorem is about.

A complete development needs the Perron–Frobenius theory of nonnegative and irreducible matrices, the Tarski fixed-point theorem (in Mathlib), and the condensation of a digraph into its strongly connected components. The Perron–Frobenius milestones are reusable well beyond this mission and are welcome as independent contributions. The continuity results of §5 (Theorem 3, Corollaries 2–3) are out of scope.

Selected references

L. Massai, G. Como, F. Fagnani, Equilibria and Systemic Risk in Saturated Networks, Mathematics of Operations Research; arXiv:1912.04815v2, 2021. https://arxiv.org/abs/1912.04815
L. Eisenberg, T. H. Noe, Systemic Risk in Financial Networks, Management Science 47(2), 2001. https://doi.org/10.1287/mnsc.47.2.236.9835
A. Berman, R. J. Plemmons, Nonnegative Matrices in the Mathematical Sciences, SIAM, 1994. https://doi.org/10.1137/1.9781611971262

12 thms3 active usersReviewed

Convex Optimization Optimization Probability·Captain: mikedeng1

Universal Barrier is n-Self-Concordant: The Universal Barrier of Every Proper Convex Domain in ℝⁿ Is an n-Self-Concordant BarrierResearch Paper

Motivation

Interior-point methods minimize a linear function over a convex set $K\subseteq\mathbb R^n$ by following the minimizers of $t\,c^{\mathsf T}x+\varphi(x)$ , where $\varphi$ is a self-concordant barrier for $K$ . The number of Newton steps the path-following method needs to reach accuracy $\epsilon$ is $O(\sqrt{\nu}\log(1/\epsilon))$ , where $\nu$ is the barrier's self-concordance parameter. A smaller $\nu$ is a better iteration bound, and the question of the smallest $\nu$ achievable for an arbitrary convex domain is a basic question of the theory.

1994: Nesterov and Nemirovski introduced the universal barrier, defined for every convex domain without lines, and proved it is $O(n)$ -self-concordant (Interior-Point Polynomial Algorithms in Convex Programming, SIAM, Theorem 2.5.1). They also showed that no barrier for the simplex or the cube has parameter below $n$ .
2015: Bubeck and Eldan introduced the entropic barrier, proved it is $(1+o(1))n$ -self-concordant, and showed that on convex cones both the universal and the entropic barrier are $n$ -self-concordant (arXiv:1412.1587).
2021: Lee and Yue proved that the universal barrier is $n$ -self-concordant on every proper convex domain in $\mathbb R^n$ , $n\ge1$ (arXiv:1809.03011, Mathematics of Operations Research). This mission formalizes that result.

Setting

A convex domain is a convex set $K\subseteq\mathbb R^n$ with non-empty interior; it is proper if it contains no line $\{x+tv:t\in\mathbb R\}$ with $v\neq0$ . $K$ need not be closed or bounded. For $x\in\operatorname{int}(K)$ the polar set of $K$ with respect to $x$ is

K^\circ(x)=\{y\in\mathbb R^n:\ y^{\mathsf T}(z-x)\le1\ \text{ for all } z\in K\},

a convex body, and the universal barrier is $\varphi(x)=\log\mathrm{Vol}_n(K^\circ(x))$ .

A function $\varphi$ on $\operatorname{int}(K)$ is a barrier if $\varphi(x)\to+\infty$ as $x\to\partial K$ . A convex, three times continuously differentiable $\varphi$ is self-concordant if, for all $x\in\operatorname{int}(K)$ and $h\in\mathbb R^n$ ,

|D^3\varphi(x)[h,h,h]|\le2\,(D^2\varphi(x)[h,h])^{3/2},\tag{1}

and $\nu$ -self-concordant if moreover $|D\varphi(x)[h]|\le(\nu\,D^2\varphi(x)[h,h])^{1/2}$ (2).

The proof works with one-dimensional laws. For a convex body $L$ and $h\neq0$ , the marginal density $p(L,h;\cdot)$ is the density of $y^{\mathsf T}h$ for $y$ uniform on $L$ . For a density $p$ on $\mathbb R$ , $\mu_1(p)$ is its mean, $\mu_2^2(p)$ its variance and $\mu_3^3(p)$ its third central moment; $\mu_2^3(p)=(\mu_2^2(p))^{3/2}$ . A density is $\tfrac1m$ -concave if $p^{1/m}$ is concave on its support (for $m=0$ : $p$ is constant on its support, up to endpoints).

Formalization targets

Goal: Theorem 2

\text{For } n\ge1 \text{ and every proper convex domain } K\subseteq\mathbb R^n,\ \ \varphi(x)=\log\mathrm{Vol}_n(K^\circ(x)) \text{ is an } n\text{-self-concordant barrier for } K.

The parameter $n$ is exact, so the goal carries no constant to improve.

Milestones

The barrier property of $\varphi$ .
Brunn's concavity principle for hyperplane sections (Theorem 1 with $F=h^\perp$ ): $p(L,h;\cdot)$ is $\tfrac1{n-1}$ -concave.
Lemma 2: a non-increasing density on $[0,1]$ has mean at most $\tfrac12$ .
The polynomial inequality $f_0(\gamma)\ge0$ for $\gamma\ge1$ (§4.1.7).
Proposition 1, inequality (5): for a $\tfrac1{k-1}$ -concave density with $0\in\operatorname{Supp}(p)$ , $\mu_1^2(p)\le k(k+2)\mu_2^2(p)$ .
Lemma 3: affine invariance of the family $\mathcal Q$ and of $\Xi(p)=|\mu_3^3(p)/\mu_2^3(p)|$ .
Lemma 4: the polynomial inequality $g(\gamma,k)\ge0$ for $\gamma\ge1$ , $k\ge2$ .
Proposition 1, inequality (4): for a $\tfrac1{k-1}$ -concave density,

|\mu_3^3(p)|\le2\sqrt{\tfrac{k+2}{k}}\,\tfrac{k-1}{k+3}\,\mu_2^3(p).

Lemma 1: $D\varphi$ , $D^2\varphi$ , $D^3\varphi$ at $x$ along $h$ as polynomials in the moments of $p(K^\circ(x),h;\cdot)$ .
Inequality (9): $\ell(t)=(2t^3+6t+4c_n)/(1+t^2)^{3/2}\le2\sqrt{n+1}$ , with $c_n=(n-1)/(2\sqrt n)$ .

Significance

The theorem settles the self-concordance parameter of the universal barrier for every proper convex domain: it is $n$ , and by the lower bound of Nesterov and Nemirovski no barrier does better in general. It implies the $n$ -self-concordance results for cones as special cases, and it gives a canonical barrier attaining the optimal iteration bound $O(\sqrt n\log(1/\epsilon))$ on any domain. Proposition 1, a pair of sharp moment inequalities for $s$ -concave distributions, is of independent interest; it extends the third-moment bound for log-concave laws used by Bubeck and Eldan.

The result is proved on paper; none of it is formalized. A complete development would give machine-checked statements of the universal barrier, its derivative formulas, Brunn's principle for hyperplane sections, and the moment inequalities, all of which are reusable for other barrier constructions (the entropic barrier missions on the platform use the same definitions of barrier and self-concordance). The two polynomial inequalities (milestones 4 and 7) are self-contained and the appendix proof of Lemma 4 is long elementary calculus, a natural target for automation.

Difficulty

The derivative formulas reduce $n$ -self-concordance to moment inequalities for the marginal of the polar body. The obvious argument uses only log-concavity of marginals (Prékopa–Leindler) and the log-concave third-moment bound; it yields $\nu=O(n)$ and loses a constant. Exactness requires the stronger $\tfrac1{n-1}$ -concavity and moment bounds that are sharp for every $k$ , attained by $k\,t^{k-1}$ on $[0,1]$ . Proposition 1 is an extremal problem over an infinite-dimensional class of densities, and the sharp constants surface only as polynomial inequalities in a parameter $\gamma\ge1$ whose degree grows with $k$ (milestones 4 and 7); Lemma 4 must hold uniformly in the integer $k\ge2$ , and small $k$ behave differently. The localization lemma the paper cites for the reduction is not in Mathlib. On the analytic side, Lemma 1 requires differentiating $\log\mathrm{Vol}_n(K^\circ(x))$ three times under the integral for a possibly unbounded $K$ .

Formalization scope

The space is EuclideanSpace ℝ (Fin n) with Lebesgue measure volume. The goal's conclusion is the published predicate EntropicBarrier.Universal.IsNuSelfConcordantBarrier K φ n: barrier limits at every frontier point within $\operatorname{int}(K)$ ; convexity, $C^3$ and inequality (1) on $\operatorname{int}(K)$ through the published line-restriction form ConvexOptimization.IsSelfConcordantOn; and (2) in one-sided form, equivalent to the two-sided one. Lemma 1 uses Fréchet derivatives iteratedFDeriv. The universal barrier is a total function; its values off $\operatorname{int}(K)$ are junk and never read. All of $K$ 's standing assumptions (convex, non-empty interior, no line) are bundled in IsProperConvexDomain, together with $n\ge1$ .

Three conventions correct slips of the page and are disclosed in each item:

$s$ -concavity is quantified over support points. Definition 5 read literally (for all $t_1,t_2\in\mathbb R$ ) is satisfied by no probability density, which would make Proposition 1 vacuously true and Brunn's principle false. The formalization uses the paper's own usage, "on its support". This trivializing reading is ruled out by design, and a sanity check exhibits a density satisfying every hypothesis of Proposition 1.
Marginals are normalized by their own integral, since $\mathrm{Vol}_{n-1}(\text{slice})/\mathrm{Vol}_n(L)$ integrates to $1/\|h\|$ ; the published section measure is an unnormalized Hausdorff measure, and the normalization removes its constant. Milestones 2 and 9 assume $h\neq0$ .
The family $\mathcal Q$ requires $a<b$ ; the degenerate case is the Dirac case the paper treats separately.

Densities are non-negative functions with integral $1$ , and moments are Bochner integrals; a $\tfrac1{k-1}$ -concave density has bounded support, so they are genuine. Not formalized: Brunn's principle for general $k$ , the localization lemma (Theorem 3) and its corollaries, the limiting reductions of §4.1.1–§4.1.5 and §4.2.1, and the internals of Appendix A. Contributions of any of these as supporting lemmas, of Brunn–Minkowski-type tools for sections, and of differentiation-under-the-integral results for polar volumes are welcome.

Selected references

Y. T. Lee and M.-C. Yue, Universal Barrier is n-Self-Concordant, Mathematics of Operations Research 46(3), 2021; arXiv:1809.03011v4. https://arxiv.org/abs/1809.03011
Yu. Nesterov and A. Nemirovski, Interior-Point Polynomial Algorithms in Convex Programming, SIAM, 1994. https://doi.org/10.1137/1.9781611970791
S. Bubeck and R. Eldan, The entropic barrier: a simple and optimal universal self-concordant barrier, COLT 2015; arXiv:1412.1587. https://arxiv.org/abs/1412.1587
M. Fradelizi and O. Guédon, The extreme points of subsets of s-concave probabilities and a geometric localization theorem, Discrete & Computational Geometry 31(2), 2004. https://doi.org/10.1007/s00454-003-2868-y
S. Brazitikos, A. Giannopoulos, P. Valettas and B.-H. Vritsiou, Geometry of Isotropic Convex Bodies, AMS, 2014. https://doi.org/10.1090/surv/196

16 thms3 active usersReviewed

All missions

Entangling operations and their implementation using a small amount of entanglement: The Gate exp(−i(π/2^N)σx⊗σx) Is Implemented with Unit Probability Using α_N f_N < 5.97932·α_N Ebits on AverageResearch Paper

Motivation

Setting

Formalization targets

Goal: unit probability at cost αNfN\alpha_Nf_NαN​fN​

Milestones

Significance

Difficulty

Formalization scope

Selected references

Pricing and Optimization in Shared Vehicle Systems: An Approximation Framework: Elevated-Flow-Relaxation Prices Earn an m/(m+n−1) Fraction of the Optimal State-Dependent ObjectiveResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 15

Milestones

Significance

Difficulty

Formalization scope

Selected references

M-Convex Function Minimization Under L1-Distance Constraint and Its Application to Dock Reallocation in Bike-Sharing System: Steepest Descent from the Center Is Optimal at Every L1 RadiusResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.2

Milestones

Significance

Difficulty

Formalization scope

Selected references

On the Set of Balanced Games: The Polytope of Nonnegative Balanced Games Is Combinatorial and Its Adjacency Graph Is Hamilton-ConnectedResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 12

Milestones

Significance

Difficulty

Formalization scope

Selected references

SYN-DIGITS: A Synthetic Control Framework for Calibrated Digital Twin Simulation: Error Bound for Ridge Fit-and-Transfer on a New QuestionResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.1 (p. 11), both clauses

Milestones (Appendix B.1, pp. 32–33)

Significance

Difficulty

Formalization scope

Selected references

On the Effect of Symmetry Requirement for Rendezvous on the Complete Graph: Symmetric Strategies Wait at Least (n+1)/2 + 2⁻³⁶nResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1

Milestones

Significance

Difficulty

Formalization scope

Selected references

Block Sensitivity vs. Sensitivity: Reach 2.1311217191902.1311217191902.131121719190Open Problem

What this mission establishes

The construction behind the goal

Formal statement and provenance

Uncertainty Quantification and Exploration for Reinforcement Learning: Empirical Q-Values Are Strongly Consistent and √n(Q̂ₙ − Q) ⇒ N(0, Σ) with the Closed-Form Covariance (5)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1

Milestones (the proof of Theorem 1, App. A.1)

Significance

Difficulty

Formalization scope

Selected references

The Power of Subsampling in Submodular Maximization: SampleGreedy is a (p+1)²/p-approximation for non-negative submodular maximization over p-extendible systemsResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 7)

Goal: unit probability at cost $\alpha_Nf_N$

Block Sensitivity vs. Sensitivity: Reach $2.131121719190$ Open Problem

Goal: exact error, attained optimum, and the constant $\pi^2$