Linear algebra

Motivation

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

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

Setting

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

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

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

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

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

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

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

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

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

Formalization targets

Recovery error

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

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

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

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

Selected references

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

Motivation

Matrix approximation replaces a large or complicated matrix with a random matrix that is easier to store or compute. Averaging independent realizations improves accuracy while retaining the structure of each realization. Examples in Tropp's monograph include sparse approximations and randomized matrix products. The practical question is how the number of samples, the size of one sample, and its second moment control the spectral norm error. Tropp, §6.2

The book proves a matrix Bernstein inequality in Theorem 6.1.1, then applies it to an empirical matrix average in Corollary 6.2.1. Theorem 6.1.1 is already posed as TroppMatrixConcentration.matrix_bernstein on Prove2Me and is currently Open. This mission records the application with its own hypotheses and constants. The capstone concerns the estimator that a reader would construct, rather than a sum of abstract centered summands. Tropp, §§6.1–6.2

Setting

Let $B$ be a fixed complex $d_1\times d_2$ matrix. A sample matrix $R$ has the same size, has expectation $B$, and has spectral norm at most $L$ almost surely. The equality $\mathbb ER=B$ makes one sample an unbiased estimate of $B$. The almost-sure bound limits the size of every sample except on a probability-zero set. The dimensions $d_1,d_2$ are positive integers, and $n$ is a positive sample count.

Take independent copies $R_1,\ldots,R_n$ with the distribution of $R$. Their matrix sampling estimator is

$$\overline R_n=\frac1n\sum_{k=1}^nR_k.$$

For any rectangular matrix $A$, $A^*$ denotes its conjugate transpose and $\|A\|$ its spectral norm. The per-sample second moment is

$$m_2(R)=\max\{\|\mathbb E(RR^*)\|,\|\mathbb E(R^*R)\|\}.$$

Both terms matter for a rectangular matrix: $RR^*$ and $R^*R$ act on different coordinate spaces. All expectations of matrices are entrywise expectations, represented by Bochner integrals in Lean. The almost-sure norm bound guarantees the moments used here are finite. Tropp, equations (6.2.4)–(6.2.6)

Formalization targets

Empirical matrix approximation

Corollary 6.2.1 gives an expectation estimate and a tail estimate for the same estimator. For every real $t\ge0$,

$$\mathbb E\|\overline R_n-B\|\le \sqrt{\frac{2m_2(R)\log(d_1+d_2)}{n}}+ \frac{2L\log(d_1+d_2)}{3n},$$ $$\mathbb P\{\|\overline R_n-B\|\ge t\}\le (d_1+d_2)\exp\left(\frac{-nt^2/2}{m_2(R)+2Lt/3}\right).$$

The goal includes both bounds. The expectation estimate controls average error; the tail estimate controls the chance of an error above a chosen threshold. The dimension enters only through $\log(d_1+d_2)$ in the expectation bound and the factor $d_1+d_2$ in the tail bound. These are the book's constants, including the factors $2$ and $3$ in the linear terms. Tropp, Corollary 6.2.1, p. 81

Supporting statements

The milestone list follows Corollary 6.1.2 for uncentered summands, the bound $\|n^{-1}(R_k-B)\|\le2L/n$, and the variance estimate $v(\overline R_n-B)\le m_2(R)/n$. Equation (6.2.7) is a companion: a stated lower bound on $n$ implies $\mathbb E\|\overline R_n-B\|\le2\varepsilon$ for $\varepsilon>0$. Tropp, pp. 77, 82

Significance

The result turns a bound on one random matrix into a quantitative guarantee for an empirical approximation. It lets a user choose a sample count for a target error and evaluate both average error and failure probability. The same framework is instantiated later in the monograph for matrix sparsification and multiplication; those applications depend on controlling $L$ and $m_2(R)$ for their particular sampling laws. Tropp, §§6.2–6.4

This is a known mathematical result proved in the book. Its Lean statement is an open formalization target. The mission adds a reusable empirical-mean definition and application statements built on the already published matrix spectral norm and rectangular second-moment definitions. A proof of the general matrix Bernstein theorem remains separate; the mission can draw on it when that platform theorem is proved.

Difficulty

The estimator error is a centered sum, but the sampling assumptions are given for an uncentered random matrix $R$. Bounding the centered summands changes the uniform bound from $L$ to $2L/n$. The variance parameter must be related to the second moment of one uncentered sample, with the correct $1/n$ scaling. Dropping the common-distribution condition would leave no relation between the samples' second moments and $m_2(R)$. Applying scalar concentration to entries would not directly give the stated spectral norm bound or its dimension dependence. Tropp, proof of Corollary 6.2.1, p. 82

Formalization scope

Matrices are Matrix (Fin d₁) (Fin d₂) ℂ. The spectral norm and rectSecondMoment are imported from tc's published TroppMatrixConcentration definitions. An arbitrary probability space carries a measurable reference matrix $R_0$ and a finite family $R_k$; iIndepFun expresses independence and IdentDistrib expresses equality in law with $R_0$. The estimator is the finite sum scaled by $n^{-1}$. No particular sampling scheme or deterministic choice of $R$ is fixed: the formal goal requires only the source's unbiasedness and boundedness conditions.

The Lean statements explicitly require $d_1,d_2\ge1$, $n>0$, measurability, and the almost-sure form of $\|R\|\le L$. These make the logarithm and inverse sample count meaningful and make the random matrix laws well behaved. For the uncentered Bernstein corollary, integrability of each $S_k$ is explicit because a bounded deviation from an unspecified mean alone does not establish that the mean exists. The goal also asserts integrability of its error norm, preventing a Bochner integral from silently taking Lean's default value for a nonintegrable function. The bound on $R$ supplies that integrability. When the denominator in a tail formula is zero, the displayed total real division gives a loose bound at the degenerate case; the source's probabilistic claim remains valid.

Contributions that formalize the centered-summand calculation, the variance estimate, or the transfer from the general matrix Bernstein theorem are within scope. The imported matrix and probability definitions are reusable in other matrix concentration missions. The local empirical-mean definition is reusable whenever a matrix estimator averages finitely many random samples.

Selected references

• Joel A. Tropp, An Introduction to Matrix Concentration Inequalities, Foundations and Trends in Machine Learning 8(1–2), 2015, arXiv:1501.01571v1, especially §§6.1–6.4.

Motivation

Estimating a large matrix that is approximately low rank from a few noisy linear measurements is a basic problem of high-dimensional statistics. It covers matrix completion (recovering a ratings table from a small sample of entries), multi-task regression and quantum state tomography. The standard estimator penalizes the nuclear norm, the sum of the singular values, which is the convex surrogate of the rank. Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256v4; Ann. Statist. 39(5), 2011) study a variant of this estimator that uses the known distribution of the design. Their Theorem 1 proves sharp oracle inequalities, with leading constant 1, under a global isometry condition on the design (Assumption 1).

Global isometry is a strong requirement. For sparse vectors, the analogous requirement was relaxed to the restricted eigenvalue condition of Bickel, Ritov and Tsybakov (Ann. Statist. 37, 2009), which only asks for curvature on a cone of approximately sparse directions. The random-design version is due to Koltchinskii (Bernoulli 15, 2009), and a matrix version of the cone appears in Negahban, Ravikumar, Wainwright and Yu (arXiv:1010.2731). Theorem 2 of the paper is the matrix counterpart of the restricted eigenvalue analysis for this estimator. It keeps the leading constant 1, and the price is a stronger tuning condition, λ ≥ 3‖M‖∞ instead of 2‖M‖∞. Section 5.4 of the same paper derives from it a sharp sparsity oracle inequality for the ordinary vector Lasso.

Setting

Observe n pairs (Xᵢ, Yᵢ), i = 1, …, n, where Xᵢ is a random m₁ × m₂ real matrix and Yᵢ a real random variable, satisfying the trace regression model

$$\mathbb E(Y_i \mid X_i) = \operatorname{tr}(X_i^\top A_0),$$

for an unknown matrix A₀. Write ⟨A, B⟩ = tr(AᵀB), and let ‖A‖₁, ‖A‖₂ and ‖A‖∞ be the nuclear, Frobenius and operator norms, the last being the largest singular value. The design enters through the bilinear form

$$\langle A, B\rangle_{L_2(\Pi)} = \frac1n\sum_{i=1}^n \mathbb E\big(\langle A, X_i\rangle\langle B, X_i\rangle\big),$$

with semi-norm ‖A‖_{L₂(Π)}. Two random objects are built from the sample: the noise matrix M = (1/n) Σᵢ (YᵢXᵢ − 𝔼(YᵢXᵢ)), and, for λ > 0 and a set 𝔸 of matrices, the estimator Â^λ, any minimizer over 𝔸 of

$$L_n(A) = \|A\|_{L_2(\Pi)}^2 - \Big\langle \frac2n\sum_{i=1}^n Y_iX_i, A\Big\rangle + \lambda\|A\|_1 .$$

Let A = Σ_{j≤r} σⱼ uⱼvⱼᵀ be a singular value decomposition, with support (S₁, S₂), the spans of the uⱼ and of the vⱼ. Write 𝒫_A⊥(B) = P_{S₁⊥} B P_{S₂⊥} for the part of B orthogonal to both singular spaces, and 𝒫_A(B) = B − 𝒫_A⊥(B). When 𝔸 is a linear subspace and c₀ ≥ 0, the cone ℂ_{A,c₀} consists of the B ∈ 𝔸 with ‖𝒫_A⊥(B)‖₁ ≤ c₀‖𝒫_A(B)‖₁. The restricted constant μ_{c₀}(A) is the infimum of the μ′ > 0 such that ‖𝒫_A(B)‖₂ ≤ μ′‖B‖{L₂(Π)} for every B ∈ ℂ{A,c₀}. The paper uses μ(A) := μ₅(A).

Formalization targets

Goal: Theorem 2, (2.19)

Let 𝔸 be a linear subspace. If λ ≥ 3‖M‖∞, then

$$\|\hat A^\lambda - A_0\|_{L_2(\Pi)}^2 \le \inf_{A \in \mathbb A}\Big[\|A - A_0\|_{L_2(\Pi)}^2 + \lambda^2\mu^2(A)\operatorname{rank}(A)\Big].$$

The bound is deterministic: it holds for every realization of the sample on which λ ≥ 3‖M‖∞. A₀ need not lie in 𝔸, and nothing is assumed about the design beyond what makes the objects finite.

Milestones

The milestones are the displays of the proof, in the order the proof uses them:

1. (2.8), the inequality obtained from the first-order optimality condition of the estimator, which the proof of Theorem 1 already uses;
2. (2.20), in the case ⟨Â^λ − A₀, Â^λ − A⟩_{L₂(Π)} > 0;
3. (2.21), the splitting of ⟨M, Â^λ − A⟩ along 𝒫_A and 𝒫_A⊥;
4. (2.22), the inequality (λ − 2Δ)‖𝒫_A⊥(Â^λ − A)‖₁ ≤ (λ + 2Δ)‖𝒫_A(Â^λ − A)‖₁ with Δ = ‖M‖∞;
5. the membership Â^λ − A ∈ ℂ_{A,5} and the resulting bound by μ(A);
6. the final two-step display with the constant 1 + 2√2/3.

Significance

Theorem 2 gives a sharp oracle inequality whose only design-dependent quantity is a restricted constant. That constant is finite in situations where the global isometry of Theorem 1 fails. The result covers every linear subspace 𝔸, for example all matrices, the diagonal matrices or matrices with a prescribed sparsity pattern. In the diagonal case it becomes a sharp sparsity oracle inequality for the vector Lasso under a restricted eigenvalue condition (the paper's Theorem 14). The oracle inequalities of Bickel, Ritov and Tsybakov under the same condition have a leading constant larger than 1.

The result is proved in the paper, in about half a page that leans on the proof of Theorem 1. No machine-checked version exists. A formalization pins down two things the printed proof leaves to the reader: the convex-analytic optimality condition behind (2.8), and the "obvious modification of (2.10)" and "some algebra" behind (2.20) and the final display. It also reuses and extends the platform's matrix vocabulary: nuclear and operator norms, SVD data, and the tangent and normal projections of the matrix completion missions.

Difficulty

The estimator is defined implicitly as a minimizer, so the analysis has to go through first-order conditions. Those require the subdifferential of the nuclear norm and a choice of subgradient that matches the support of the comparison matrix A. Mathlib has neither a characterization of this subdifferential nor the monotonicity argument in matrix form. The obvious route, copying Theorem 1, fails at the step that uses Assumption 1 to pass from Frobenius to L₂(Π) norms: without a global isometry, that comparison is available only on the cone ℂ_{A,5}, and the error is known to lie there only in the case ⟨Â^λ − A₀, Â^λ − A⟩_{L₂(Π)} > 0 and only for λ ≥ 3‖M‖∞. The constant 5 = (λ + 2Δ)/(λ − 2Δ) at λ = 3Δ is not slack. A linear subspace, not just a convex set, is needed so that Â^λ − A lies in 𝔸, where the cone lives.

Formalization scope

Matrices are RealMatrix m₁ m₂ from the published MatrixCompletion definitions. These supply ⟨·,·⟩ (matrixInner), the nuclear, Frobenius and operator norms, SVD data SVD A r, the sign matrix Σuⱼvⱼᵀ, and 𝒫_A, 𝒫_A⊥ (tangentProjection, normalProjection). This mission adds two definition files.

• Model. ⟨·,·⟩{L₂(Π)}, M, L_n and the estimator, all at a fixed outcome ω. The structure TraceRegression holds the standing assumptions: measurable Xᵢ and Yᵢ, square-integrable entries of Xᵢ, integrable Yᵢ and YᵢXᵢ, and 𝔼(Yᵢ | σ(Xᵢ)) = tr(XᵢᵀA₀) almost surely. The page leaves the integrability implicit. Without it a Bochner integral would silently be 0 and ‖·‖{L₂(Π)} would be meaningless. Expectations of matrices are entrywise. Independence of the pairs (p. 1) is not assumed: Theorem 2 does not use it. The estimator is any minimizer of L_n over 𝔸.
• Cone and restricted constant. ℂ_{A,c₀} ⊆ 𝔸 and the predicate "μ′ is a cone constant". μ(A) can be +∞ (no constant exists), and a real infimum of an empty set is 0. So every statement is made for every cone constant μ′ for (A, 5). This is equivalent to the infimum form and makes the bound vacuous exactly when the paper's is. A formalization with a real sInf would make (2.19) false and is ruled out.

The other conventions are these. "inf over A ∈ 𝔸" is a bound for every A ∈ 𝔸. rank(A) is Matrix.rank. n ≥ 1 and λ > 0 are assumed, as on the page. (2.8) is stated for a convex 𝔸, as in the proof of Theorem 1 where it is derived. (2.21) is stated for an arbitrary matrix in place of Â^λ − A. No printed statement needed correction.

A complete development needs the subdifferential of the nuclear norm ((2.1) of the paper), the first-order condition for constrained convex minimization, the identity (2.9) and the facts (2.10), and trace duality, which is on the platform as matrix_trace_duality_inequality. The subdifferential of the nuclear norm and the projection estimates are reusable well beyond this mission. Contributions of those general lemmas are welcome.

Selected references

• V. Koltchinskii, K. Lounici, A. B. Tsybakov, Nuclear-norm penalization and optimal rates for noisy low-rank matrix completion, arXiv:1011.6256v4, 2016 (Ann. Statist. 39(5), 2302–2329, 2011). https://arxiv.org/abs/1011.6256
• P. J. Bickel, Y. Ritov, A. B. Tsybakov, Simultaneous analysis of Lasso and Dantzig selector, Ann. Statist. 37(4), 1705–1732, 2009. https://doi.org/10.1214/08-AOS620
• V. Koltchinskii, The Dantzig selector and sparsity oracle inequalities, Bernoulli 15(3), 799–828, 2009. https://doi.org/10.3150/09-BEJ187
• S. Negahban, P. Ravikumar, M. J. Wainwright, B. Yu, A unified framework for high-dimensional analysis of M-estimators with decomposable regularizers, arXiv:1010.2731, 2010 (Statist. Sci. 27(4), 2012). https://arxiv.org/abs/1010.2731
• G. A. Watson, Characterization of the subdifferential of some matrix norms, Linear Algebra Appl. 170, 33–45, 1992. https://doi.org/10.1016/0024-3795(92)90407-2

Motivation

Many estimation problems in statistics and machine learning ask for an unknown matrix observed only through noisy linear measurements: matrix completion (recover a large matrix from a few noisy entries, as in collaborative filtering), multi-task regression, and quantum state tomography. A common structural prior is that the unknown matrix has low rank, and the standard convex surrogate for rank is the nuclear norm, the sum of the singular values. Penalizing a least-squares criterion by the nuclear norm gives an estimator that can be computed by convex optimization.

Koltchinskii, Lounici and Tsybakov (arXiv:1011.6256v4; Ann. Statist. 39(5), 2011) study a nuclear-norm penalized estimator in the general trace regression model and prove that it satisfies sharp oracle inequalities: the excess prediction error is bounded by the best approximation error over a class of matrices with leading constant exactly $1$, plus a remainder governed by either the nuclear norm ("slow rate") or the rank ("fast rate") of the approximating matrix. A distinctive feature of their estimator is that it uses the known design distribution $\Pi$, which the empirical-risk estimators of the earlier literature (Candès and Plan 2010; Rohde and Tsybakov 2011; Negahban and Wainwright 2011) do not exploit; for noisy matrix completion the previously available bounds were suboptimal. Their Theorem 1 is the deterministic core from which the paper's matrix completion rates (Theorem 4) follow by bounding one random matrix in operator norm.

Setting

Let $(X_i,Y_i)$, $i=1,\dots,n$, be random pairs, $X_i$ a real $m_1\times m_2$ matrix and $Y_i$ a real number, satisfying the trace regression model

$$\mathbb E(Y_i\mid X_i)=\langle A_0,X_i\rangle,\qquad \langle A,B\rangle=\operatorname{tr}(A^\top B),$$

for an unknown matrix $A_0$. Let $\Pi_i$ be the law of $X_i$ and $\Pi=\frac1n\sum_i\Pi_i$. The $L_2(\Pi)$ inner product and semi-norm are

$$\langle A,B\rangle_{L_2(\Pi)}=\frac1n\sum_{i=1}^n\mathbb E\big(\langle A,X_i\rangle\langle B,X_i\rangle\big),\qquad \|A\|^2_{L_2(\Pi)}=\langle A,A\rangle_{L_2(\Pi)}.$$

For a matrix $A$ with singular values $\sigma_j(A)$, $\|A\|_1=\sum_j\sigma_j(A)$ is the nuclear norm, $\|A\|_2$ the Frobenius norm, and $\|A\|_\infty=\sigma_1(A)$ the operator norm. If $A=\sum_{j=1}^r\sigma_ju_jv_j^\top$ is a singular value decomposition, the pair $(S_1,S_2)=(\operatorname{span}\{u_j\},\operatorname{span}\{v_j\})$ is the support of $A$, and $P_S$ is the orthogonal projector onto $S$.

Given a set $\mathbb A$ of matrices and $\lambda>0$, the estimator is

$$\hat A^\lambda\in\operatorname*{argmin}_{A\in\mathbb A}L_n(A),\qquad L_n(A)=\|A\|^2_{L_2(\Pi)}-\Big\langle\frac2n\sum_{i=1}^nY_iX_i,A\Big\rangle+\lambda\|A\|_1 .$$

The random matrix

$$\mathbf M=\frac1n\sum_{i=1}^n\big(Y_iX_i-\mathbb E(Y_iX_i)\big)$$

carries all the noise. Assumption 1 asks for a constant $\mu>0$ with $\|A\|^2_{L_2(\Pi)}\ge\mu^{-2}\|A\|_2^2$ for all $A\in\mathbb A-\mathbb A$.

Formalization targets

Goal: Theorem 1

If $\lambda\ge2\|\mathbf M\|_\infty$, then for any set $\mathbb A$

$$\|\hat A^\lambda-A_0\|^2_{L_2(\Pi)}\le\inf_{A\in\mathbb A}\Big[\|A-A_0\|^2_{L_2(\Pi)}+2\lambda\|A\|_1\Big],\tag{2.3}$$

and if moreover $\mathbb A$ is convex and Assumption 1 holds,

$$\|\hat A^\lambda-A_0\|^2_{L_2(\Pi)}\le\inf_{A\in\mathbb A}\Big[\|A-A_0\|^2_{L_2(\Pi)}+\Big(\tfrac{1+\sqrt2}{2}\Big)^2\mu^2\lambda^2\operatorname{rank}(A)\Big],\tag{2.4}$$

and, for every $A\in\mathbb A$ with support $(S_1,S_2)$,

$$\|\hat A^\lambda-A_0\|^2_{L_2(\Pi)}+(\lambda-2\|\mathbf M\|_\infty)\|P_{S_1^\perp}\hat A^\lambda P_{S_2^\perp}\|_1\le\|A-A_0\|^2_{L_2(\Pi)}+\Big(\tfrac{1+\sqrt2}{2}\Big)^2\mu^2\lambda^2\operatorname{rank}(A).\tag{2.5}$$

The theorem is deterministic: it holds at every realization of the sample at which $\lambda\ge2\|\mathbf M\|_\infty$.

Milestones

The milestones follow the paper's proof: the subdifferential of the nuclear norm (2.1); the basic inequality of p. 7 and the slow-rate bound (2.3); the first-order condition (2.6); the identity (2.9) and the facts (2.10); the inequality (2.11); the decomposition bound (2.12)–(2.14); the bound on $\Lambda$ via (2.15); and the combined inequality (2.17). The rank bound (2.16) is included as a supporting statement (not a milestone).

Significance

Theorem 1 separates the statistical problem into a deterministic oracle inequality and a single probabilistic estimate, $\|\mathbf M\|_\infty\le\lambda/2$. Any concentration bound for $\|\mathbf M\|_\infty$ (matrix Bernstein for uniform sampling, Gaussian bounds for fixed designs) then gives a rate. The paper uses it to obtain matrix completion rates which its minimax lower bounds show to be optimal up to logarithmic factors on the class of matrices of rank at most $r$ with entries bounded by $a$. The leading constant $1$ means the bounds remain informative when $A_0$ is not low rank but only well approximated by low-rank matrices.

The result has been proved on paper since 2011; to our knowledge no machine-checked proof exists. A formal proof requires the subdifferential of the nuclear norm and its interplay with the singular-subspace projections, which are reusable for every nuclear-norm method (singular value thresholding, robust PCA, multi-task learning).

Difficulty

The slow-rate bound (2.3) is a short computation from the definition of a minimizer and trace duality. The fast-rate bounds (2.4)–(2.5) are not: a minimizer comparison alone gives only $\lambda\|\hat A^\lambda-A\|_1$ as remainder, which does not scale with $\operatorname{rank}(A)$. One needs the variational inequality (2.6) over the convex set $\mathbb A$, the exact description (2.1) of the nuclear-norm subdifferential at an arbitrary comparison matrix $A$, and a decomposition of $\langle\mathbf M,\hat A^\lambda-A\rangle$ along the support of $A$ in which the component orthogonal to the support is controlled in operator norm and the rest in Frobenius norm. Formally, (2.1) itself requires identifying the abstract singular values with a given decomposition and characterizing the operator-norm ball as the dual of the nuclear norm.

Formalization scope

Matrices are RealMatrix m₁ m₂ = Matrix (Fin m₁) (Fin m₂) ℝ, with the published MatrixCompletion definitions supplying the Frobenius inner product matrixInner, nuclearNorm (sum of Mathlib's singular values), spectralNorm (operator norm), frobeniusNorm, SVD data SVD A r and the projections twoSidedSingularProjection ($P_{S_1}\cdot P_{S_2}$), tangentProjection ($\mathcal P_A$) and normalProjection ($P_{S_1^\perp}\cdot P_{S_2^\perp}$). The sample lives on a probability space (Ω, P) with 0 < n; expectations of matrices are entrywise. Conventions committed to:

1. Realization-wise statements. $\omega$ is fixed; $\hat A$ is any matrix with $\hat A\in\mathbb A$ and $L_n(\hat A)\le L_n(A)$ for all $A\in\mathbb A$. Existence of a minimizer is not asserted.
2. Infima are stated as the bound for every $A\in\mathbb A$ (equivalent; no real sInf is used).
3. The model (1.1) is the conditional expectation of $Y_i$ given the $\sigma$-algebra generated by the entries of $X_i$.
4. Added regularity, not printed in the paper: every entry of $X_i$ is measurable and square integrable, $Y_i$ is measurable and integrable, and $Y_i(X_i)_{jk}$ is integrable. Without these, Lean's Bochner integral returns $0$ and $\|\cdot\|_{L_2(\Pi)}$ and $\mathbf M$ would be meaningless.
5. Independence of the pairs is not assumed; the proof does not use it.
6. Supports are given by SVD data; bounds use A.rank.
7. Corrected statement. The first fact of (2.10), $\|\sum_ju_jv_j^\top\|_\infty=1$, is false for $A=0$ (empty sum); the milestone assumes $r>0$.
8. Steps the paper states for $\hat A^\lambda$ or $\mathbf M$ but which hold for arbitrary matrices ((2.9), (2.10), (2.12)–(2.16)) are stated for arbitrary matrices.

Ruling out trivializations: the goal states (2.3)–(2.5) with the paper's constants and remainder terms, not the intermediate bound (2.17), and $\hat A$ is pinned down as a minimizer over $\mathbb A$, not an arbitrary matrix.

Welcome contributions: proofs of the nuclear-norm subdifferential (2.1) and of the projection facts, which are reusable well beyond this mission, and the measure-theoretic identity $\frac1n\sum_i\mathbb E(Y_iX_i)=\frac1n\sum_i\mathbb E(\langle A_0,X_i\rangle X_i)$ from the model.

Selected references

• V. Koltchinskii, K. Lounici, A. B. Tsybakov, Nuclear-norm penalization and optimal rates for noisy low-rank matrix completion, arXiv:1011.6256v4, 2016 (the source of this mission); Ann. Statist. 39(5), 2302–2329, 2011. https://arxiv.org/abs/1011.6256, https://doi.org/10.1214/11-AOS894
• G. A. Watson, Characterization of the subdifferential of some matrix norms, Linear Algebra Appl. 170, 33–45, 1992 (reference [28] of the source; the description (2.1) of the nuclear-norm subdifferential). https://doi.org/10.1016/0024-3795(92)90407-2
• E. J. Candès, Y. Plan, Matrix completion with noise, Proc. IEEE 98(6), 925–936, 2010. https://doi.org/10.1109/JPROC.2009.2035722
• A. Rohde, A. B. Tsybakov, Estimation of high-dimensional low-rank matrices, Ann. Statist. 39(2), 887–930, 2011. https://doi.org/10.1214/10-AOS860
• S. Negahban, M. J. Wainwright, Estimation of (near) low-rank matrices with noise and high-dimensional scaling, Ann. Statist. 39(2), 1069–1097, 2011. https://doi.org/10.1214/10-AOS850

Motivation

Online marketplaces, ad exchanges and real-estate platforms sell items that are each described by a vector of features and are rarely seen twice. A seller who prices such items cannot learn a demand curve item by item. It must learn how features map to values, while pricing, from accept/reject feedback alone. Cohen, Lobel and Paes Leme (Management Science, 2020; SSRN 2737045) model this as feature-based dynamic pricing with adversarial features and a linear valuation. They show that a direct multi-dimensional binary search (PolytopePricing) can have regret exponential in the dimension (their Theorem 1). Their EllipsoidPricing algorithm, a pricing variant of Khachiyan's ellipsoid method (Khachiyan 1979), has worst-case regret quadratic in the dimension and logarithmic in the horizon (their Theorem 2). This mission formalizes Theorem 2 and the chain of lemmas behind it.

Setting

Fix a dimension $d \ge 2$, a radius $R > 0$ and a horizon $T$. Nature picks an unknown parameter $\theta \in \mathbb{R}^d$ with Euclidean norm $\|\theta\| \le R$. In each period $t = 1, \dots, T$ a product arrives with a feature vector $x_t \in \mathbb{R}^d$, $\|x_t\| \le 1$, and market value $\theta' x_t$. The seller sees $x_t$, posts a price $p_t$, and a sale occurs iff $p_t \le \theta' x_t$, earning $p_t$. The regret (Eq. (1)) is

$$\mathrm{Regret} = \sum_{t=1}^{T} \big[\theta' x_t - p_t\,\mathbb{I}\{\theta' x_t \ge p_t\}\big],$$

and the worst-case regret of a policy is its maximum over $\theta$ and over nature's (possibly adaptive) choice of features.

An ellipsoid with center $a$ and positive definite shape matrix $A$ is $E(A,a) = \{\theta : (\theta - a)' A^{-1} (\theta - a) \le 1\}$. EllipsoidPricing with parameter $\epsilon > 0$ keeps an ellipsoid $E_t = E(A_t, a_t)$, starting from the ball $E_1 = B(0,R)$. In period $t$ it computes

$$\underline b_t = x_t' a_t - \sqrt{x_t' A_t x_t}, \qquad \bar b_t = x_t' a_t + \sqrt{x_t' A_t x_t},$$

the minimum and maximum of $\hat\theta' x_t$ over $E_t$.

• If $\bar b_t - \underline b_t \le \epsilon$, it exploits: it posts $p_t = \underline b_t$ and keeps $E_{t+1} = E_t$.
• Otherwise it explores: it posts $p_t = \tfrac12(\bar b_t + \underline b_t)$ and replaces $E_t$ by the ellipsoid of Eq. (4) that covers the half of $E_t$ consistent with the feedback. With $b = A_t x_t / \sqrt{x_t' A_t x_t}$, the new shape is $\tilde A = \frac{d^2}{d^2-1}\big(A_t - \frac{2}{d+1} b b'\big)$ and the new center is $a_t \pm \frac{1}{d+1} b$, with $+$ after a sale.

Write $\lambda_d(A)$ for the smallest eigenvalue of a symmetric matrix $A$.

Formalization targets

Goal: Theorem 2

There is a universal constant $C > 0$ such that for all $d \ge 2$, $R > 0$, $T \ge 2d$, $\|\theta\| \le R$ and $\|x_t\| \le 1$, EllipsoidPricing run with $\epsilon = R d^2 / T$ satisfies

$$\mathrm{Regret} \le C \, R \, d^2 \ln(T/d).$$

This is the paper's $O(R d^2 \ln(T/d))$ claim, with no constant fixed.

Milestones, in the order of the paper's argument

• the closed forms of $\underline b_t, \bar b_t$ (§5.2);
• the containment of each half-ellipsoid in the updated ellipsoid (Eq. (4), already proved on the platform);
• $\theta \in E_t$ and $A_t \succ 0$ along the run;
• the volume formula $\operatorname{Vol} E(A,a) = V_d \sqrt{\prod_i \lambda_i(A)}$ and the volume decrease $\operatorname{Vol} E(\tilde A) \le e^{-1/2d} \operatorname{Vol} E(A)$ (§5.1);
• Lemma 2: if $z < \lambda_d(A)$ and $\det(A - \beta b b' - zI) \ge 0$, then $\lambda_d(A - \beta b b') \ge z$;
• Lemma 3: $\lambda_d(\tilde A) \ge \frac{d^2}{(d+1)^2} \lambda_d(A)$;
• Lemma 4: if $\lambda_d(A) \le \epsilon^2/(400 d^2)$ and $x' A x > \epsilon^2/4$, then $\lambda_d(\tilde A) \ge \lambda_d(A)$;
• the eigenvalue floor $\lambda_d(A_t) \ge \epsilon^2 / (400 (d+1)^2)$;
• Lemma 1: at most $2 d^2 \ln(20 R (d+1)/\epsilon)$ exploration periods;
• an exploitation period sells and has regret at most $\epsilon$.

Significance

The result. Theorem 2 shows that contextual posted-price learning with adversarial features costs only polynomially many "probing" sales in the dimension. A direct cutting-plane search over the polytope of consistent parameters (PolytopePricing) cannot do this: its worst-case regret is exponential in $d$ (Theorem 1). The ellipsoid analysis via the smallest eigenvalue (Lemmas 2–4) is reused in the paper's noisy-valuation extension (ShallowPricing, §6) and in later work on contextual pricing and contextual search.

Formalizing it. No part of the paper is machine-checked. The Eq. (4) containment is already proved on the platform (Bertsimas–Tsitsiklis Theorem 8.1). The volume factor there is $e^{-1/(2(d+1))}$, weaker than the $e^{-1/2d}$ used here. The eigenvalue lemmas on rank-one perturbations (Lemmas 2–4) are new to the platform and reusable for any analysis of ellipsoid-type updates. A formal proof of the goal would also settle a gap in the printed proof, noted under the formalization scope.

Difficulty

The obvious argument is the textbook ellipsoid bound: volume shrinks by $e^{-1/2d}$ per exploration, so exploration must stop. This fails because the ellipsoid need not become small in every direction. The volume can go to zero while one axis stays long, and then a feature along that axis keeps triggering exploration. The paper replaces the volume argument by a lower bound on the smallest eigenvalue, which needs a sign analysis of the characteristic polynomial of a rank-one perturbation (Lemmas 2–4) together with the exploration test $x_t' A_t x_t > \epsilon^2/4$. The constant $k = 1/(400 d^2)$ in Lemma 4 is chosen to make a specific inequality hold for every $d \ge 2$.

The regret bound needs, in addition, a per-round bound for exploration periods. The printed proof (p. 16) uses "the trivial bound of regret $R$ per round". That bound is not immediate when an exploration price is accepted, since the center $a_t$ can leave $B(0,R)$ and the round's regret is then only bounded by $\sqrt{x_t' A_t x_t}$. This is why the goal is the $O$-form with an unspecified universal constant rather than the proof's explicit inequality.

Formalization scope

• Types. Vectors are Fin d → ℝ; $\theta' x$ is the dot product θ ⬝ᵥ x. Both norms are Euclidean, encoded as $x\cdot x \le 1$ and $\theta\cdot\theta \le R^2$; Mathlib's ‖·‖ on Fin d → ℝ is the sup norm and is never used. Ellipsoids, the ball, and the update (4) are the published LinearOptimization.ellipsoid, ellipsoidBall, ellipsoidUpdateCenter and ellipsoidUpdateMatrix.
• Eigenvalues and volume. $\lambda_d(A)$ is the infimum of the real spectrum, i.e. the minimum eigenvalue of a symmetric matrix. Volumes are Lebesgue measure on Fin d → ℝ in $[0, \infty]$. $\varphi_D(z)$ is $\det(D - zI)$ as printed, not Mathlib's charpoly.
• The algorithm. EllipsoidPricing is a deterministic recursion indexed from $0$ (Lean period $t$ is the paper's $t+1$), started from $E_1 = B(0,R)$, which the paper allows ("or in fact any ellipsoid that contains $K_1$", p. 11). The paper's "smallest ellipsoid containing $H_{t+1}$" is replaced by its closed form (4), which the paper gives on p. 14. Because the algorithm is deterministic, a closed-loop nature generates a fixed feature sequence, and the worst case is a universal quantifier over $\theta$ in the ball and over sequences.
• Added hypotheses, all disclosed in the items.
  • $d \ge 2$ everywhere, since (4) divides by $d^2 - 1$.
  • $T \ge 2d$ in the goal, since $\ln(T/d) \le 0$ for $T \le d$.
  • $\epsilon \le 20 R (d+1)$ in Lemma 1 and the eigenvalue floor: for larger $\epsilon$ the printed bound is negative.
  • $\|x\| \le 1$ in Lemma 4, the §3 normalization that its proof uses.
• Not taken from the page. E₁ is not the Löwner–John ellipsoid of a general $K_1$: the proof's "$\tilde E_1$ lies in the ball of radius $R$" fails for it. The proof's explicit inequality $\mathrm{Regret} \le NR + (T-N)\epsilon$ is not a milestone, because of the per-round gap above.
• Ruled out. The goal may not be trivialized by any of the following:
  • a constant $C$ that depends on $d$, $R$, $T$ or the instance;
  • regret measured against a price the algorithm never posts, or an exploit price that is not accepted;
  • features bounded in the sup norm;
  • an explore test or update different from (4);
  • a single fixed feature sequence.
• Contributions welcome. Proofs of the volume formula and the $e^{-1/2d}$ decrease, which are reusable for any ellipsoid-method development; the eigenvalue lemmas; and the per-round bound for accepted exploration prices that the goal needs.

Selected references

• M. C. Cohen, I. Lobel, R. Paes Leme, Feature-Based Dynamic Pricing, Management Science 66(11), 2020. https://doi.org/10.1287/mnsc.2019.3485 (authors' copy: https://ssrn.com/abstract=2737045)
• L. G. Khachiyan, Polynomial algorithms in linear programming, USSR Comput. Math. Math. Phys. 20(1), 1980. https://doi.org/10.1016/0041-5553(80)90061-0
• M. Grötschel, L. Lovász, A. Schrijver, Geometric Algorithms and Combinatorial Optimization, Springer, 1993. https://doi.org/10.1007/978-3-642-78240-4
• G. H. Golub, Some modified matrix eigenvalue problems, SIAM Review 15(2), 1973. https://doi.org/10.1137/1015032
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997 (Theorem 8.1, the platform's ellipsoid update).

Motivation

Extremal graph theory asks how many edges a graph on $n$ vertices can have without containing a fixed graph $F$. The answer, the Turán number $\mathrm{ex}(n,F)$, and the graphs attaining it, the set $\mathrm{Ex}(n,F)$ of extremal graphs, are known precisely only for special $F$; the Erdős–Stone–Simonovits theorem gives $\mathrm{ex}(n,F) = (1 - \frac{1}{\chi(F)-1} + o(1))\frac{n^2}{2}$, where $\chi(F)$ is the chromatic number.

Spectral extremal graph theory asks the same question with the number of edges replaced by the spectral radius $\lambda(G)$, the largest eigenvalue of the adjacency matrix. Since $\lambda(G) \ge 2e(G)/n$, a spectral bound implies an edge bound, and spectral extremal results are usually stronger than their edge versions. Nikiforov (Linear Algebra Appl. 427, 2007) showed that the Turán graph $T_{n,r}$ maximises $\lambda$ among $K_{r+1}$-free graphs, so for $F = K_{r+1}$ the spectral and the edge extremal graphs coincide. Whether this happens for other $F$ is the subject of the paper.

Timeline:

• 1941 Turán: $T_{n,r}$ is the unique extremal graph for $K_{r+1}$.
• 2003 Chen, Gould, Pfender, Wei (J. Combin. Theory Ser. B 89): $\mathrm{ex}(n, F_{k,r+1}) = e(T_{n,r}) + O(1)$ for $k$ copies of $K_{r+1}$ sharing one vertex.
• 2007 Nikiforov (Linear Algebra Appl. 427): spectral Turán theorem for $K_{r+1}$. 2009 Nikiforov (J. Graph Theory 62): spectral stability for large forbidden subgraphs, the source of Lemma 2.5.
• 2020 Cioabă, Feng, Tait, Zhang (Electron. J. Combin. 27): the spectral extremal graph for the friendship graph $F_k$ lies in $\mathrm{Ex}(n, F_k)$.
• 2022 Cioabă, Desai, Tait (European J. Combin. 99) conjecture: if the graphs in $\mathrm{Ex}(n,F)$ are Turán graphs plus $O(1)$ edges, then the spectral extremal graphs lie in $\mathrm{Ex}(n,F)$ for large $n$. Before the general proof it was known for $K_{r+1}$, the friendship graphs $F_k$, the graphs $H_{s,k}$ (Li, Peng) and the intersecting cliques $F_{k,r}$ (Desai, Kang, Li, Ni, Tait, Wang, arXiv:2108.03587).
• 2022/2023 Wang, Kang, Xue (arXiv:2203.10831; J. Combin. Theory Ser. B, 2023): the conjecture holds in general. This mission formalizes their Theorem 1.2.

Setting

All graphs are finite and simple. For a graph $G$ on $n$ vertices, $A(G)$ is its $0/1$ adjacency matrix and $\lambda(G)$ is the largest eigenvalue of $A(G)$. A graph $G$ is $F$-free if no subgraph of $G$ is isomorphic to $F$. The Turán number $\mathrm{ex}(n,F)$ is the maximum number of edges $e(G)$ over $F$-free graphs $G$ on $n$ vertices, and $\mathrm{Ex}(n,F)$ is the set of $F$-free $n$-vertex graphs with $\mathrm{ex}(n,F)$ edges. The Turán graph $T_{n,r}$ is the complete $r$-partite graph on $n$ vertices with parts of sizes $\lfloor n/r\rfloor$ or $\lceil n/r\rceil$.

The hypothesis on $F$ is: for fixed integers $r \ge 2$ and $a \ge 0$ and all large $n$, $\mathrm{ex}(n,F) = e(T_{n,r}) + a$ and every graph in $\mathrm{Ex}(n,F)$ contains a spanning copy of $T_{n,r}$, i.e. is $T_{n,r}$ plus $a$ edges. The paper states "adding $O(1)$ edges" and fixes the constant at the start of Section 3 (p. 4): "We may assume that the graphs in $\mathrm{Ex}(n,F)$ are obtained from $T_{n,r}$ by adding $a$ edges." The mission follows that reading. Examples: $K_{r+1}$ with $a = 0$, the friendship graphs, and the intersecting cliques $F_{k,r+1}$.

A graph $G$ is spectral extremal for $F$ if it is $F$-free and $\lambda(G) \ge \lambda(G')$ for every $F$-free $G'$ on the same $n$ vertices.

Formalization targets

Goal: Theorem 1.2

For $r \ge 2$, $a \ge 0$ and $F$ satisfying the hypothesis, there is $N$ such that for all $n \ge N$ every spectral extremal graph $G$ for $F$ on $n$ vertices satisfies

$$e(G) = \mathrm{ex}(n,F), \qquad\text{i.e.}\qquad G \in \mathrm{Ex}(n,F).$$

The statement contains no numerical constant, and $N$ depends only on $F$, $r$, $a$.

Milestones

The milestones follow the proof, in order: strict monotonicity of $\lambda$ under proper subgraphs of a connected graph (Lemma 2.3); connectivity of $G$ (Lemma 3.1); the bound $\lambda(G) \ge (1-\frac1r)n - \frac{r}{4n} + \frac{2a}{n}$ (Lemma 3.2); spectral stability for $\chi(F) = r+1$ (Corollary 2.6); for every maximum $r$-cut $V_1 \cup \dots \cup V_r$, $\sum_i e(V_i) \le \varepsilon n^2$ and $|V_i| = (\frac1r \pm 3\sqrt\varepsilon)n$ (Lemma 3.3); a counting inequality for intersections (Lemma 2.8); $e(G[V_i]) \le a$ and minimum degree above $(1 - \frac1r - 3r\varepsilon^{1/3})n$ (Lemma 3.6); at most $2a$ vertices of each part have a neighbour in that part, and all others see every other part completely (Lemma 3.7); Perron entries $x_u \ge 1 - 20a^2r^2/n$ for $a \ge 1$ (Lemma 3.8); $e(G_{in}) - e(G_{out}) \le a$ (Lemma 3.9); balancing two parts of a complete multipartite graph increases $\lambda$ (Lemma 2.7); and the maximum partition is balanced, $|n_i - n_j| \le 1$ (Lemma 3.10).

Significance

The theorem settles the Cioabă–Desai–Tait conjecture: for every $F$ whose extremal graphs are Turán graphs plus a bounded number of edges, the spectral extremal problem reduces to the edge extremal problem for large $n$. This recovers the earlier cases (friendship graphs, the graphs $H_{s,k}$, intersecting cliques) at once, and it turns any future determination of $\mathrm{Ex}(n,F)$ of this type into a spectral result with no further work.

The result is proved on paper; it has no machine-checked proof. Mathlib has Turán's theorem (extremalNumber_top, uniqueness of turanGraph) and the definition of extremalNumber, but no spectral extremal graph theory: no Perron–Frobenius theorem for graphs, no spectral Turán theorem, no stability theorem. The formalization would supply these, and the milestone statements are independently reusable: strict monotonicity of $\lambda$ (Lemma 2.3), the spectral comparison of complete multipartite graphs (Lemma 2.7) and spectral stability (Corollary 2.6) are standard tools of the area.

Difficulty

The natural first idea, comparing $G$ with an extremal graph $H$ by Rayleigh quotients, fails at the start: $\lambda(G) \ge \lambda(H)$ gives only $e(G) \ge e(T_{n,r}) - o(n^2)$, far from $\mathrm{ex}(n,F)$. Closing an additive gap of $O(1)$ edges requires control of the Perron vector to within $O(1/n)$ at every vertex and exact control of the part sizes. The second is the delicate step: an imbalance of one vertex between two parts costs $\Theta(1/n)$ in $\lambda$, while the $a$ extra edges contribute only $O(1/n^2)$ beyond the Turán graph, so the two effects must be compared at different scales. Further, the proof needs the deep spectral stability theorem of Nikiforov (Lemma 2.5), whose own proof is long.

Formalization scope

Graphs on $n$ vertices are SimpleGraph (Fin n), matching Mathlib's extremalNumber n F; $F$ is a graph on any finite type. $\lambda(G)$ is the largest eigenvalue of G.adjMatrix ℝ (index $0$ of Mathlib's decreasingly sorted eigenvalues₀), not an absolute value and not a norm. "$F$-free" is F.Free G (no copy of $F$, not necessarily induced). "Sufficiently large $n$" is ∃ N, ∀ n ≥ N with $N$ chosen after $F, r, a$ and before $G$; "sufficiently small $\varepsilon$" is ∃ ε₀ > 0, ∀ ε ∈ (0, ε₀). Partitions $V_1 \cup \dots \cup V_r$ are labellings Fin n → Fin r whose parts may be empty; the Section 3 lemmas hold for every partition maximising the number of crossing edges. Lemma 3.8 carries the extra hypothesis $a \ge 1$, because as printed it is false for $a = 0$ (for $F = K_{r+1}$ and $r \nmid n$ the Perron vector of $T_{n,r}$ has entries below $1$); the goal does not assume it.

Trivializing formalizations are ruled out: $\lambda$ is not defined from the edge count (which would make spectral and edge extremality the same), the hypothesis on $F$ does not contain the conclusion and is satisfiable (a sorry-free check for $F = K_{r+1}$, $a = 0$ was compiled), the conclusion is $e(G) = \mathrm{ex}(n,F)$ and not a weaker bound, and the threshold is not chosen after $G$.

A complete development needs the Perron–Frobenius theorem for irreducible nonnegative symmetric matrices, the Rayleigh quotient characterisation of $\lambda$, the spectrum of complete multipartite graphs, Nikiforov's spectral stability lemma, and max-cut partition arguments. All of these are reusable beyond this mission, and proofs of any milestone, of the cited Lemmas 2.1, 2.2 and 2.5, or of Nikiforov's spectral Turán theorem are welcome.

Selected references

• J. Wang, L. Kang, Y. Xue, On a conjecture of spectral extremal problems, J. Combin. Theory Ser. B, 2023; arXiv:2203.10831v1 (2022). https://arxiv.org/abs/2203.10831
• S. Cioabă, D. N. Desai, M. Tait, The spectral radius of graphs with no odd wheels, European J. Combin. 99 (2022) 103420.
• S. Cioabă, L. H. Feng, M. Tait, X. D. Zhang, The maximum spectral radius of graphs without friendship subgraphs, Electron. J. Combin. 27(4) (2020) P4.22.
• G. Chen, R. J. Gould, F. Pfender, B. Wei, Extremal graphs for intersecting cliques, J. Combin. Theory Ser. B 89 (2003) 159–171.
• V. Nikiforov, Bounds on graph eigenvalues II, Linear Algebra Appl. 427 (2007) 183–189.
• V. Nikiforov, Stability for large forbidden subgraphs, J. Graph Theory 62(4) (2009) 362–368.
• D. N. Desai, L. Kang, Y. Li, Z. Ni, M. Tait, J. Wang, Spectral extremal graphs for intersecting cliques, arXiv:2108.03587v2 (2021). https://arxiv.org/abs/2108.03587

Motivation

A max-XORSAT instance asks for a binary assignment that satisfies as many parity constraints as possible. A matrix specifies the parity check in each constraint, while a second binary vector specifies the desired parity. The objective can be written as the number of satisfied constraints minus the number violated, so an assignment with a high objective value is also a good approximate solution. Jordan and coauthors study decoded quantum interferometry (DQI), a way to sample candidate assignments by encoding a weighted superposition of error patterns and then decoding their syndromes. Their ideal-state analysis assumes that low-weight errors have distinct syndromes. Real decoders can succeed on many errors even when this uniqueness condition fails, which makes the theorem in this mission relevant to the algorithmic regime beyond the guaranteed decoding radius. Jordan et al., §§8.1 and 10.

The paper's 2024 preprint introduced DQI for linear constraint satisfaction and related optimization problems. Its revised 2025 version studies the effect of decoder failures on the measured objective in Theorem 10.1. This mission uses that revision, arXiv:2408.08292v5, and isolates the first inequality of equation (172). The same section supplies explicit identities for the norm of the postselected state and for its objective matrix, making the theorem a bounded campaign of finite combinatorics and linear algebra. Jordan et al., §10, pp. 35–43.

Setting

Fix integers $m,n\ge0$ and a binary matrix $B\in\mathbb F_2^{m\times n}$. Its $i$th row defines a parity $b_i\cdot x$ of an assignment $x\in\mathbb F_2^n$. For a binary vector $v\in\mathbb F_2^m$, the objective is

$$f_v(x)=\sum_{i=1}^{m}(-1)^{b_i\cdot x+v_i}.$$

An error pattern $y\in\mathbb F_2^m$ has syndrome $B^\top y$ and Hamming weight $|y|$. The weight-$k$ shell $E_k$ contains all errors with $|y|=k$. Choose $0\le\ell\le m$ and real weights $w_0,\ldots,w_\ell$. The ideal syndrome-space state in equation (140) sums $(-1)^{v\cdot y}|B^\top y\rangle$ over each $E_k$, multiplied by $w_k/\sqrt{\binom m k}$. Jordan et al., equations (140) and (171).

A deterministic decoder $\mathrm{dec}:\mathbb F_2^n\to\mathbb F_2^m$ guesses an error from its syndrome. It correctly identifies $y$ when $\mathrm{dec}(B^\top y)=y$. Write $D_k\subseteq E_k$ for the correctly identified errors and $F_k=E_k\setminus D_k$ for the failures. The shell failure rate is $\varepsilon_k=|F_k|/\binom m k$, and $\varepsilon=\max_{0\le k\le\ell}\varepsilon_k$. Postselecting successful decoding leaves the unnormalized state $\widetilde P_D(f)$ formed by replacing each $E_k$ in the ideal state with $D_k$. Apply the binary Hadamard transform, divide by the resulting norm, measure $x$, and evaluate $f_v(x)$. Denote this measured expectation by $\langle f_v\rangle$. Jordan et al., §10.3, pp. 39–40.

Formalization targets

Theorem 10.1: the averaged objective

Let $N=\sum_{k=0}^{\ell}w_k^2(1-\varepsilon_k)$ be the squared norm of the postselected state. The goal, for $N>0$ and uniform $v\in\mathbb F_2^m$, is

$$\mathbb E_v\langle f_v\rangle\ge \frac{w^\top A^{(m,\ell,0)}w-2\varepsilon(m+1)w^\top w}{N}.$$

The matrix $A^{(m,\ell,0)}$ is the symmetric tridiagonal matrix in equation (70): its diagonal is zero and its entries adjacent to the diagonal are $a_k=\sqrt{k(m-k+1)}$. This is the first inequality of (172), with the decoder's actual failure fractions in $N$ and the worst shell failure rate in the correction. It has no minimum-distance hypothesis. Jordan et al., Theorem 10.1, pp. 39–40.

Supporting targets

The milestone list includes the norm identity of Lemma 10.4, the ideal and postselected objective matrices of Lemmas 10.2 and 10.5, the normalized expectation identity in (179), the averaged matrix identities of Lemmas 10.3 and 10.6, and the error-matrix bound of Lemma 10.7. A separate companion item records the second comparison printed in (172) under an explicit sign condition; without that condition, the printed comparison can fail. Jordan et al., §10, pp. 36–43.

Significance

The result assigns a quantitative cost to decoding errors. It says how the measured max-XORSAT objective changes when some error patterns are lost during postselection, while permitting a code whose low-weight errors share syndromes. Consequently the theorem addresses the setting in which practical decoding succeeds often but exact distance-based uniqueness is unavailable. The denominator also records the survival probability of the weighted state, so the bound keeps the actual normalization visible. Jordan et al., §10, pp. 35 and 39–43.

A complete formalization would provide reusable definitions for binary syndrome decoding, shellwise failure rates, real-amplitude states, normalized measurement expectations, and finite objective matrices. The paper proves the result on paper; this mission asks for machine-checked proofs of the stated goal and its milestones. The formal development would also document exactly which part of equation (172) requires an additional sign assumption. No proof is claimed by the draft statements themselves.

Difficulty

When two errors have the same syndrome, the ideal syndrome state can combine their amplitudes, so its norm need not equal $w^\top w$. Postselection changes which errors remain, and the measured objective depends on the normalized state for each $v$. Replacing that normalized expectation with the objective of an average state would change the claim. The proof must keep the decoder fixed while $v$ varies and must control the error matrix uniformly over every real weight vector. The printed second inequality of (172) adds a separate sign issue: a smaller positive denominator reverses the expected comparison when the numerator is negative. Jordan et al., equations (161), (171)–(172), (179)–(182).

Formalization scope

Lean uses ZMod 2 for bits, Fin m and Fin n for zero-based coordinates, functions for binary vectors, and Matrix for $B$. The decoder is one function of the syndrome, independent of $v$. Hamming shells, correct and failed decoding sets, and $\varepsilon_k$ are computed from that function. Weights and amplitudes are real. The postselected state uses the factor $1/\sqrt{\binom m k}$; the Hadamard transform uses $1/\sqrt{2^n}$. The average over $v$ is the sum over all $2^m$ vectors divided by $2^m$. The tridiagonal entries compute $m-k$ in the reals, preserving the square-root formula at the boundary.

Two domain conditions are made explicit. The bound $\ell\le m$ rules out absent weight shells, for which Lean would otherwise assign zero to division by $\binom m k=0$. The condition $N>0$ rules out a zero postselected state, whose normalized expectation would likewise be assigned a meaningless zero by total real division. The goal ranges over every binary matrix, every fixed deterministic decoder, and every real weight vector satisfying those conditions. It states the expectation of the explicit postselected state after a Hadamard transform, rather than an unconstrained expectation variable.

The supporting development needs finite character sums, Hamming-shell cardinalities, matrix quadratic forms, and an operator bound for a symmetric real matrix. These components can serve other finite decoding and quantum-state calculations. Contributions proving the seven cited milestones or the goal are within scope. The circuit's resource accounting, asymptotic equation (173), and numerical decoder studies are outside this mission.

Selected references

• S. P. Jordan, N. Shutty, M. Wootters, A. Zalcman, A. Schmidhuber, R. King, S. V. Isakov, T. Khattar, and R. Babbush, Optimization by Decoded Quantum Interferometry, arXiv:2408.08292v5, 2025 revision of the 2024 preprint. arXiv

Motivation

Quantum error correction and quantum communication both ask the same question: after a known noise process $\mathcal A$ has acted on a quantum system, how well can its effect be undone? For a given noise model the best recovery is the solution of a semidefinite program, which gives a number but no structure and no formula. Barnum and Knill showed in 2000 that a single, explicit recovery map, built from $\mathcal A$ and the input state alone, is always close to the best one: its fidelity is at least the square of the optimal fidelity (arXiv:quant-ph/0004088). The map they use is now usually called the Petz recovery map or transpose channel; Petz had introduced it in operator-algebraic work on sufficiency (Petz 1986; Petz 1988). Near-optimality results of this kind underlie approximate quantum error correction and the later theory of recoverability in quantum information.

Timeline.

• 1986–1988, D. Petz: the map $\rho^{1/2}\mathcal A^\dagger(\mathcal A(\rho)^{-1/2}\,\cdot\,\mathcal A(\rho)^{-1/2})\rho^{1/2}$ characterizes when a channel can be reversed exactly on a family of states.
• 2002, Barnum and Knill (J. Math. Phys. 43, 2097; doi:10.1063/1.1459754): in the published version, the reversal operation achieves at least the square of the optimal entanglement fidelity for a single input state.
• arXiv v2 of the same paper (the source of this mission): the published Eq. (34) had dropped the ensemble weights; with that corrected, the bound holds for the average entanglement fidelity of any ensemble of commuting density matrices (Acknowledgments, p. 14).

Setting

A finite-dimensional quantum system is described by complex $n\times n$ matrices; $X^\dagger$ is the conjugate transpose, and a density matrix is a positive semidefinite matrix of trace one. A completely positive map $\mathcal A$ is given by a finite decomposition $\mathcal A\sim\{A_i\}_i$ of matrices and acts by

$$\mathcal A(X)=\sum_iA_iXA_i^\dagger .$$

It is trace-preserving if $\sum_iA_i^\dagger A_i=I$ and trace-nonincreasing if $\sum_iA_i^\dagger A_i\le I$ in the Loewner order. The composite $\mathcal R\mathcal A$ has decomposition $\{R_kA_i\}_{(k,i)}$.

For a state $\rho$ the paper defines the reversal operation

$$\mathcal R_{\mathcal A,\rho}\sim\{\rho^{1/2}A_i^\dagger\,\mathcal A(\rho)^{-1/2}\}_i,$$

under the standing assumption that $\mathcal A(\rho)$ has full support. Here $X^{-1/2}$ is the generalized inverse square root: invert the square roots of the non-zero eigenvalues and keep the zero eigenvalues.

Fidelities are measured by the entanglement fidelity $F_e(\rho,\mathcal K)=\sum_k|\operatorname{tr}K_k\rho|^2$ of a map $\mathcal K\sim\{K_k\}_k$ and, for an ensemble $E=\{p_l,\rho_l\}_l$ (weights $p_l\ge0$ summing to one, density matrices $\rho_l$), by the average entanglement fidelity

$$\bar F_e(E,\mathcal K)=\sum_lp_lF_e(\rho_l,\mathcal K).$$

When $\rho=\sum_ip_i|i\rangle\langle i|$ in an orthonormal eigenbasis, the classical fidelity is $F_{\mathrm{cl}}(\rho,\mathcal K)=\sum_ip_i\langle i|\mathcal K(|i\rangle\langle i|)|i\rangle$, the average entanglement fidelity of the ensemble of eigenstates.

Formalization targets

Goal: Theorem 3 (p. 7)

Let $\mathcal A$ be trace-preserving, $E=\{p_l,\rho_l\}_l$ an ensemble of pairwise commuting density matrices, $\rho=\sum_lp_l\rho_l$, and assume $\mathcal A(\rho)$ has full support. Then for every trace-preserving completely positive $\mathcal R$,

$$\bar F_e(E,\mathcal R_{\mathcal A,\rho}\mathcal A)\;\ge\;\bar F_e(E,\mathcal R\mathcal A)^2 .$$

Milestones

The milestones follow the paper's proof:

1. Lemma 1 (p. 7): $\mathcal R_{\mathcal A,\rho}$ depends only on the map $\mathcal A$, not on its decomposition.
2. (14)–(15) (p. 7): after replacing $R_k$ by $P_CR_k$ ($P_C$ the support projector of $\rho$), which leaves $\bar F_e$ unchanged and makes $\mathcal R$ trace-nonincreasing, each $R_k=\rho^{1/2}B_k^\dagger\mathcal A(\rho)^{-1/2}$, and $\mathcal B(\rho)\le\mathcal A(\rho)$.
3. (28)–(32) (p. 9): $\sum_lp_l\sum_i|\operatorname{tr}\rho_lR^l_iB^l_i|^2\le\sum_lp_l\sum_{i,j}\operatorname{tr}R^l_iB^l_j\rho_lB_j^{l\dagger}R_i^{l\dagger}$.
4. (33)–(34) (p. 9): that sum equals $\operatorname{tr}\mathcal R(\mathcal B(\rho))\le\operatorname{tr}\mathcal R(\mathcal A(\rho))\le1$.

Two companions are also posed: Proposition 2, $\mathcal R_{\mathcal A,\rho}(\mathcal A(\rho))=\rho$, and Corollary 4, $F_{\mathrm{cl}}(\rho,\mathcal R\mathcal A)\le\sqrt{F_{\mathrm{cl}}(\rho,\mathcal R_{\mathcal A,\rho}\mathcal A)}$ and $F_e(\rho,\mathcal R\mathcal A)\le\sqrt{F_e(\rho,\mathcal R_{\mathcal A,\rho}\mathcal A)}$.

Significance

The result. Theorem 3 says that the error $1-\bar F_e$ of the reversal operation is at most twice the optimal error, since $(1-\eta)^2\ge1-2\eta$. It gives a closed-form recovery whose performance is within a factor two in error of the semidefinite optimum, for every noise process and every commuting ensemble. Taking the ensemble of eigenstates of $\rho$ (Corollary 4) gives the same guarantee for classical information sent through a quantum channel; the companion mission (II of this series) applies the construction to state discrimination, where the reversal operation is the pretty good measurement.

Formalizing it. The result is proved on paper; none of it has a machine-checked proof that we know of. The mission asks for the full argument: the decomposition independence of the reversal map, the reduction to the support of $\rho$, the singular-value change of decomposition (17)–(18), the chain (19)–(26) of Cauchy–Schwarz inequalities, and the normalization (27)–(34). It also fixes in Lean the arXiv v2 statement (commuting ensembles), which is stronger than the published one.

Difficulty

The obvious approach is to compare $\mathcal R_{\mathcal A,\rho}$ with an optimal $\mathcal R$ term by term. That fails: the fidelity of $\mathcal R\mathcal A$ is a sum of squared traces mixing the decompositions of $\mathcal R$ and $\mathcal A$, and no termwise inequality relates it to the fidelity of $\mathcal R_{\mathcal A,\rho}\mathcal A$. The paper first rewrites every recovery in the shape of the reversal map, then chooses, for each ensemble member separately, new decompositions of $\mathcal A$ and $\mathcal B$ that diagonalize a coefficient matrix; making that choice legitimate needs the unitary freedom of Kraus decompositions, which Mathlib does not have. The commutation $[\rho,\rho_l]=0$ is used to move fractional powers of $\rho$ and $\rho_l$ past each other inside traces; without commutation the authors do not know whether the theorem holds (p. 10).

Formalization scope

• Matrices are Matrix n n ℂ over a finite type n with decidable equality; Loewner order, square roots and functional calculus come from Mathlib (open scoped MatrixOrder). The map $X\mapsto\sum_iA_iXA_i^\dagger$ is the published PeresTerno.krausUpdate, referenced, not redefined.
• Maps are unbundled Kraus families over arbitrary finite index types. The recovery $\mathcal R$ in Theorem 3 ranges over every finite family with $\sum_kR_k^\dagger R_k=I$.
• $X^{-1/2}$ is cfc (fun x => (Real.sqrt x)⁻¹) X, the generalized inverse; Mathlib's junk matrix inverse is not used. The support projector is the functional calculus of the indicator of $x\ne0$.
• $F_e$ is defined by the formula (8), which the paper derives from its purification definition. $F_{\mathrm{cl}}$ takes an orthonormal eigenbasis and weights as data, with $\rho=\sum_ip_i|i\rangle\langle i|$ as a hypothesis.
• Standing hypotheses, all from the paper: $\mathcal A$ trace-preserving (§II's noise model); $\mathcal A(\rho)$ positive definite (full support, p. 7); the ensemble is a probability vector of pairwise commuting density matrices with $\rho=\sum_lp_l\rho_l$.
• In (34) the page prints $\operatorname{tr}\mathcal R(\mathcal A(\rho))=1$; after the replacement $R_k\mapsto P_CR_k$ the map is only trace-nonincreasing, so the milestone states $\le1$.
• Trivializing encodings are ruled out: the reversal family is the literal formula (12) for the given $\mathcal A$ and the ensemble's own $\rho$, and the fidelity of a composite map is (8) applied to the composite decomposition $\{R_kA_i\}$, never the right-hand side of the proof's chain.
• Infrastructure a complete development needs, reusable beyond this mission: the unitary freedom of Kraus decompositions, the singular value decomposition of a complex square matrix, the trace Cauchy–Schwarz inequality for Hilbert–Schmidt products, and functional-calculus identities such as $\rho^{1/2}\rho^{-1/2}=P_C$. Contributions of any of these as separate theorems are welcome. The pure-state, measurement form $P_{\mathrm{opt}}^2\le P_{\mathrm{PGM}}\le P_{\mathrm{opt}}$ is already posed on the platform as QAlgorithms.Arunachalam.barnumKnill and is not repeated here.

Selected references

• H. Barnum, E. Knill, Reversing quantum dynamics with near-optimal quantum and classical fidelity, arXiv:quant-ph/0004088v2. https://arxiv.org/abs/quant-ph/0004088
• H. Barnum, E. Knill, same title, J. Math. Phys. 43, 2097 (2002). https://doi.org/10.1063/1.1459754
• D. Petz, Sufficient subalgebras and the relative entropy of states of a von Neumann algebra, Commun. Math. Phys. 105, 123–131 (1986). https://doi.org/10.1007/BF01212345
• D. Petz, Sufficiency of channels over von Neumann algebras, Quart. J. Math. 39, 97–108 (1988). https://doi.org/10.1093/qmath/39.1.97
• B. Schumacher, Sending entanglement through noisy quantum channels, Phys. Rev. A 54, 2614 (1996). https://doi.org/10.1103/PhysRevA.54.2614
• R. A. Horn, C. R. Johnson, Matrix Analysis, Cambridge University Press (1985), §7.3. https://doi.org/10.1017/CBO9780511810817