Information Theory

Motivation

Lower bounds on the regret of stochastic multi-armed bandit strategies say how often any reasonable strategy must sample an arm that is not the best one. They are the benchmark against which upper bounds for UCB, KL-UCB and Thompson sampling are judged optimal. The classical bounds of Lai and Robbins (1985) and Burnetas and Katehakis (1996) were proved by changes of measure on carefully chosen events, combined with Markov–Chernoff estimates of their probabilities.

Garivier, Ménard and Stoltz (arXiv:1602.07182v3), published in Mathematics of Operations Research in 2019, replace those arguments with one inequality, which they call the fundamental inequality of their article, inequality (6), p. 6. Every lower bound in the paper follows from it: the asymptotic Lai–Robbins / Burnetas–Katehakis bound for an arbitrary model (Theorem 1), the non-asymptotic bounds for small horizons (Theorems 2–4), and the non-asymptotic logarithmic bound for large horizons (Theorem 5). The same inequality, in the form of Lemma 1 of Kaufmann, Cappé and Garivier (2016), underlies lower bounds for best-arm identification. This mission formalizes the inequality and the lemma that carries its proof.

Setting

A bandit problem with $K$ arms is a family $\underline\nu=(\nu_a)_{a=1,\dots,K}$ of probability distributions on $\mathbb R$, each with a finite expectation. A strategy $\psi$ plays for $T$ rounds. In round $t+1$ it picks an arm $A_{t+1}$ as a measurable function of $I_t=(U_0,Y_1,U_1,\dots,Y_t,U_t)$, where the $U_t$ are independent uniforms on $[0,1]$. It then observes a reward $Y_{t+1}$ drawn from $\nu_{A_{t+1}}$ and a fresh independent uniform $U_{t+1}$. The strategy together with the problem determines the law $\mathbb P_{\underline\nu}$ of $I_T$; $\mathbb E_{\underline\nu}$ is its expectation. The number of draws of arm $a$ is

$$N_{\psi,a}(T)=\sum_{t=1}^T\mathbb I\{A_t=a\}.$$

$\mathrm{KL}(P,Q)\in[0,+\infty]$ is the Kullback–Leibler divergence between two probability measures: $\int\ln\frac{\mathrm dP}{\mathrm dQ}\,\mathrm dP$ when $P$ is absolutely continuous with respect to $Q$ and the integral exists, and $+\infty$ otherwise. The binary divergence $\mathrm{kl}(p,q)$, for $p,q\in[0,1]$, is the Kullback–Leibler divergence between the Bernoulli distributions of parameters $p$ and $q$. For $q\in(0,1)$ it is given by (5):

$$\mathrm{kl}(p,q)=p\ln\frac pq+(1-p)\ln\frac{1-p}{1-q}.$$

It equals $+\infty$ for $q\in\{0,1\}$ and $p\ne q$.

The Lean development builds on the published StochasticBandit K, which holds the arm laws ν.P a. The local FullStrategy K implements the paper's measurable strategy on $I_t$; fullHistoryMeasure ν ψ T is the law of $I_T$, fullPullCount ψ a is $N_{\psi,a}(T)$, and fullExpPulls ν ψ T a is its expectation. The published BanditPolicy K describes the observed-history kernel model used by the two referenced chain-rule results. The shared definitions supply the Bernoulli law and klBer p q for $\mathrm{kl}(p,q)$.

Formalization targets

Goal: the fundamental inequality (6), p. 6

For every strategy $\psi$, every pair of bandit problems $\underline\nu,\underline\nu'$, every horizon $T$, and every $\sigma(I_T)$-measurable statistic $Z$ with values in $[0,1]$:

$$\sum_{a=1}^K\mathbb E_{\underline\nu}\big[N_{\psi,a}(T)\big]\,\mathrm{KL}(\nu_a,\nu'_a)\ \ge\ \mathrm{kl}\big(\mathbb E_{\underline\nu}[Z],\ \mathbb E_{\underline\nu'}[Z]\big),$$

in $[0,+\infty]$, with $0\cdot(+\infty)=0$. The arm laws have the finite expectations required in §1.1; their divergences may be infinite.

Milestones, in the order of the proof (§2.1, pp. 7–8)

1. (9), p. 7: the one-round chain rule. Under finite arm divergences, the divergence between the observed-history laws after round $t+1$ is the divergence after round $t$ plus $\mathbb E_{\underline\nu}\big[\sum_a\mathrm{KL}(\nu_a,\nu'_a)\,\mathbb I\{A_{t+1}=a\}\big]$. The observed-history kernel version is proved on the platform.
2. Equality in (8), p. 7: $\sum_a\mathbb E_{\underline\nu}[N_{\psi,a}(T)]\,\mathrm{KL}(\nu_a,\nu'_a)=\mathrm{KL}(\mathbb P_{\underline\nu}^{I_T},\mathbb P_{\underline\nu'}^{I_T})$. The platform has the observed-history kernel version under finite arm divergences; relating it to the full information law is part of the goal's work.
3. Lemma 1, first display, p. 8: $\mathrm{KL}(\mathbb P_1,\mathbb P_2)=\mathrm{KL}(\mathbb P_1\otimes\lambda,\mathbb P_2\otimes\lambda)$, with $\lambda$ the Lebesgue measure on $[0,1]$.
4. Lemma 1, second display, p. 8: $\mathrm{KL}(\mathbb P_1,\mathbb P_2)\ge\mathrm{kl}\big((\mathbb P_1\otimes\lambda)(E),(\mathbb P_2\otimes\lambda)(E)\big)$ for every measurable $E\subseteq\Gamma\times[0,1]$.
5. Lemma 1, last display, p. 8: $(\mathbb P\otimes\lambda)\{(\gamma,x):x\le Z(\gamma)\}=\mathbb E[Z]$.
6. Lemma 1, p. 8: for probability measures $\mathbb P_1,\mathbb P_2$ on any measurable space and any measurable $Z$ with values in $[0,1]$, $\mathrm{KL}(\mathbb P_1,\mathbb P_2)\ge\mathrm{kl}(\mathbb E_1[Z],\mathbb E_2[Z])$.

Significance

The result. Inequality (6) turns a lower bound on the number of draws into a choice of an alternative problem $\underline\nu'$ and a statistic $Z$, usually $Z=N_{\psi,a}(T)/T$. The binary divergence then contains expected numbers of draws directly, and no event or concentration estimate is needed. In the paper this gives a few-line proof of the Lai–Robbins / Burnetas–Katehakis bound $\liminf_T\mathbb E[N_{\psi,a}(T)]/\ln T\ge 1/\mathcal K_{\inf}$ for any model. It also gives the non-asymptotic bounds showing that the regret grows almost linearly while $T$ is below a divergence-determined threshold. Each of these is a separate mission of this series, and each applies (6) once.

The formalization. The paper calls the equality in (8) standard and re-proves it for completeness; the inequality half, Lemma 1, is its own contribution. Observed-history kernel versions of the equality in (8) and the one-round step (9) are already formalized on the platform, under the hypothesis that every arm divergence is finite. Lemma 1 and the full-information inequality (6) itself are proved in the paper but not formalized. A machine-checked (6), stated with no divergence-finiteness hypothesis, would make every downstream lower bound in the series a matter of calculus with the binary divergence.

Difficulty

Two points need care. First, Lemma 1 is stated for an arbitrary $[0,1]$-valued $Z$. The data-processing inequality only gives it directly for indicators of events, and pushing $\mathbb P_j$ forward by $Z$ gives a law on $[0,1]$, not a Bernoulli law. The paper's route enlarges the space by an independent uniform variable, which needs the product with Lebesgue measure, the invariance of the divergence under that product, and Tonelli's theorem. Second, the goal has no finiteness hypothesis on the arm divergences, while the published chain-rule results assume it. When $\mathrm{KL}(\nu_a,\nu'_a)=+\infty$ for an arm that is drawn with positive probability, the left side is $+\infty$ and there is nothing to prove. When such an arm is never drawn, its term is $0\cdot(+\infty)=0$. The divergence between the history laws must then be shown to be finite and equal to the remaining sum, which the published decomposition does not cover.

Formalization scope

• Arms are Fin K, indexed from $0$. The horizon $T$ is a natural number; at $T=0$ both sides are $0$. For $K=0$ no policy exists, so $K\ge1$ needs no hypothesis.
• Strategies are FullStrategy K, measurable functions of the paper's $I_t$. The same strategy runs under $\underline\nu$ and $\underline\nu'$. The local history law includes every auxiliary uniform, so $Z$ may depend on any of them.
• Both bandit problems satisfy Integrable id for each arm, expressing §1.1's finite-expectation condition. The published StochasticBandit structure supplies only the probability-law condition.
• The binary divergence is the $[0,+\infty]$-valued Kullback–Leibler divergence of two Bernoulli laws, klBer, never a real formula. A real formula would return a finite junk value at $q\in\{0,1\}$, where (5) is $+\infty$, and would make the goal trivially true there. A version with a finiteness hypothesis on the arm divergences, or with a real-valued binary divergence restricted to $q\in(0,1)$, would be a weaker theorem and is not the target.
• In Lemma 1 and its displays, the "distributions" are probability measures on an arbitrary measurable space. $\lambda$ is the volume on Mathlib's unitInterval. $Z$ is real-valued and measurable, with values in $[0,1]$.
• Builds on the published definitions StochasticBandit and BanditPolicy and on Mathlib's InformationTheory.klDiv. The goal uses a local explicit auxiliary-uniform strategy; the published chain-rule references use observed-history kernel policies and are related proof tools. Other tools are data processing (klDiv_map_le), the chain rule for klDiv and composition products, and Tonelli. The tensorization identity for products of probability measures is Proved on the platform as Tensorization.klDiv_prod_eq_add. Lemma 1 is reusable well beyond bandits, wherever a divergence must be compared with the means of a bounded statistic. Proofs of the milestones, and an extension of the chain rule to infinite arm divergences, are welcome.

Selected references

• A. Garivier, P. Ménard, G. Stoltz, Explore First, Exploit Next: The True Shape of Regret in Bandit Problems, Mathematics of Operations Research 44(2), 2019; arXiv:1602.07182v3. https://arxiv.org/abs/1602.07182v3, https://doi.org/10.1287/moor.2017.0928
• T. L. Lai, H. Robbins, Asymptotically efficient adaptive allocation rules, Advances in Applied Mathematics 6, 1985. https://doi.org/10.1016/0196-8858(85)90002-8
• A. N. Burnetas, M. N. Katehakis, Optimal adaptive policies for sequential allocation problems, Advances in Applied Mathematics 17, 1996. https://doi.org/10.1006/aama.1996.0007
• E. Kaufmann, O. Cappé, A. Garivier, On the complexity of best-arm identification in multi-armed bandit models, Journal of Machine Learning Research 17, 2016. https://jmlr.org/papers/v17/kaufman16a.html
• T. Lattimore, C. Szepesvári, Bandit Algorithms, Cambridge University Press, 2020. https://doi.org/10.1017/9781108571401

Motivation

Light carries information in electromagnetic field modes. At optical frequencies, photon statistics affect the capacities of thermal-noise and broadcast communication channels. Bounds on these capacities depend on identifying the smallest entropy that a beam splitter can produce under specified input conditions. Guha, Erkmen, and Shapiro explain why two such minimum output entropy claims matter: their first supports the proposed thermal-noise channel capacity, and their second supports the proposed bosonic broadcast capacity region. The paper states both as conjectures and shows that they follow from its Entropy Photon-Number Inequality (EPnI).

The authors model the EPnI on the classical entropy power inequality, but its quantum version concerns density operators rather than probability densities. Their 2007 paper does not prove the EPnI. A later platform theorem, sourced from an OpenAI mathematics preprint codebase, is marked Proved for finite-energy inputs. It supplies this mission's referenced first milestone. The statements here express the paper's two consequences in that same model; their Lean proofs are still open in this proposal.

Setting

A bosonic mode has number states $|m\rangle$ indexed by $m\in\mathbb N$. An $n$-mode state $\rho$ is a positive density operator on the full Fock space indexed by $\mathbb N^n$, with trace one. Its von Neumann entropy is $S(\rho)=-\operatorname{tr}(\rho\log\rho)$. All logarithms are natural. A thermal state with average photon number $N\ge0$ per mode has weights $N^m/(N+1)^{m+1}$ in the number basis; for $n$ modes the state is the product of these single-mode distributions. At $N=0$ this is the vacuum, with zero photons in every mode. A pure state is a projector onto a unit Fock vector. A state has zero mean field when the expectation of the annihilation operator is zero for each mode.

Two independent input states $\rho_a$ and $\rho_b$ enter a lossless beam splitter with transmissivity $\eta\in[0,1]$. For each mode its retained output has annihilation operator $\hat c=\sqrt{\eta}\,\hat a+\sqrt{1-\eta}\,\hat b$; the other output is discarded. The retained density operator is $\rho_c$. Independence means that the joint input is $\rho_a\otimes\rho_b$; correlations among modes inside either input are allowed. The thermal entropy per mode is

$$g(N)=(N+1)\log(N+1)-N\log N,$$

with the continuous convention at $N=0$. The entropy photon-number of an $n$-mode state is $g^{-1}(S(\rho)/n)$. Eq. (13) of the paper asserts that the output entropy photon-number is at least $\eta$ times that of the first input plus $1-\eta$ times that of the second. The source paper gives the definitions in §II.B, p. 2.

Formalization targets

The first target fixes the second input to a thermal product state of mean $K\ge0$, while the first ranges over zero-mean-field pure states. The second fixes the first input to the vacuum, while the second ranges over states with entropy $n g(K)$. For each class, the claimed lower bound and attained minimum are

$$S(\rho_c)\ge n\,g((1-\eta)K),\qquad \min S(\rho_c)=n\,g((1-\eta)K).$$

For the first class the vacuum first input attains equality. For the second, the product thermal second input attains equality. The goal states both claims together, including the existence of an attaining input and output. The shared attack path contains the EPnI, Eq. (13), the scalar properties of $g$ and its inverse, thermal state existence and entropy, zero entropy of pure states, the beam splitter's thermal output for vacuum and thermal inputs, and the inequalities of Eqs. (16)–(17). Each milestone uses the statement on pp. 2–3 of the paper.

Significance

An attained minimum gives the precise noise floor for the two input classes. In the paper's capacity arguments, the first class concerns the thermal-noise channel and the second the bosonic broadcast channel. The mission records the exact optimizer and the output entropy, including the endpoints $\eta=0,1$ and $K=0$. Without the optimizer's output value, a lower bound alone would not identify the minimum.

The referenced EPnI is marked Proved on Prove2Me under finite-energy assumptions. This mission's thermal-state, pure-state, and beam-splitter statements are draft targets and have no machine-checked proofs here. Closing them would connect the platform's general inequality to the two applications explicitly worked through by Guha, Erkmen, and Shapiro. The thermal-state and entropy facts can also serve other bosonic-channel formalizations using the same Fock-space interface.

Difficulty

The EPnI supplies an entropy photon-number bound, but converting it into an attained output-entropy minimum requires more than substituting a pure input. One must justify that the inverse thermal entropy behaves as expected on nonnegative entropies, that thermal product states really exist in the chosen infinite-dimensional state space, and that vacuum mixed with thermal noise produces the specified thermal output. The last claim is a statement about the full beam-splitter matrix and its partial trace, not just a scalar entropy comparison. Infinite sums also demand care: a formal expression that defaults to zero when it diverges would give a spurious entropy value.

Formalization scope

The development reuses OAI.EntropyPhotonNumber.State n, its number-basis matrix entries, real-valued entropy, $g$, the infimum definition of $g^{-1}$, and the beam-splitter output relation. The new definitions express thermal, vacuum, pure, and zero-mean-field states on that same carrier. The thermal state uses Eq. (10)'s number-basis formula; Eq. (9)'s coherent-state integral is outside this mission. The beam splitter uses the sign convention in the published definition, which yields the paper's retained output $\hat c$. The zero-mean-field condition includes convergence of each annihilation expectation.

There is at least one mode, $n\ge1$, since Eq. (11) divides entropy by $n$. Inputs to which the EPnI is applied have finite energy. This assumption is additional to the paper's phrasing: it is required by the referenced platform theorem and prevents the real-valued infinite-series entropy from taking a default zero on a divergent input. The first optimized input is therefore a finite-energy pure state; the second is a finite-energy state of entropy $n g(K)$. The thermal and vacuum witnesses themselves have finite energy. These conditions are disclosed in the theorem statements and are not assertions that the unrestricted conjectures have been settled here.

The goal quantifies over every feasible input and corresponding output, states equality for every output from the named optimizer, and asserts that the optimizer and an output exist. This rules out a vacuous result from an empty thermal-state class or a bound that omits attainment. Contributions to the scalar $g$ lemmas, thermal-state construction, pure-state entropy, and the beam-splitter output calculation are all within scope. Infrastructure for summable Fock-space matrix entries and operator entropy should remain reusable beyond this mission.

Selected references

• S. Guha, B. I. Erkmen, and J. H. Shapiro, The Entropy Photon-Number Inequality and its Consequences, arXiv:0710.5666v2, 2007. arXiv
• OpenAI, EntropyPhotonNumber Lean development, September 2026, unreviewed preprint code. Source; Prove2Me theorem.

Motivation

A quantum LDPC code is a CSS code whose two check matrices $H_X$ and $H_Z$ have rows and columns of bounded weight, so that every check measures only a few qubits. Such codes are the main candidates for fault-tolerant quantum memories, because their checks are local, but a code is only useful together with a decoder: an efficient procedure that recovers the error, up to stabilizers, from its syndrome. For classical LDPC codes built from expander graphs, Sipser and Spielman showed in 1996 that a simple bit-flipping algorithm corrects a constant fraction of the minimum distance in linear time (Sipser–Spielman 1996). In the quantum setting the obvious analogue fails, and before this work no family of quantum LDPC codes was known to admit an efficient decoder correcting a number of adversarial errors proportional to its minimum distance.

Timeline.

• 1996: Sipser and Spielman, expander codes and their linear-time bit-flipping decoder.
• 2009: Tillich and Zémor introduce the hypergraph product, giving quantum LDPC codes of positive rate and minimum distance of order $\sqrt n$ (arXiv:0903.0566).
• 2015: Leverrier, Tillich and Zémor take the hypergraph product of an expanding biregular graph with itself and prove that a greedy generator-flipping decoder corrects every error of weight up to a constant fraction of the minimum distance (arXiv:1504.00822, FOCS 2015). This mission formalizes that result.

Setting

Let $G = (A \cup B, \mathcal E)$ be a finite bipartite graph, $n_A = |A|$, $n_B = |B|$, with $n_B \le n_A$, and write $a \sim b$ for adjacency. $G$ is $(\Delta_A, \Delta_B)$-biregular if every vertex of $A$ has $\Delta_A$ neighbours and every vertex of $B$ has $\Delta_B$. For $S \subseteq A$ let $\Gamma(S)$ be its neighbourhood. $G$ is $(\gamma_A, \delta_A)$-left-expanding if $|\Gamma(S)| \ge (1 - \delta_A)\Delta_A |S|$ for every $S \subseteq A$ with $|S| \le \gamma_A n_A$; right expansion is the same on the $B$ side, and left-right expanding means both. $\Gamma_u(S)$ denotes the unique neighbours of $S$, adjacent to exactly one vertex of $S$.

Let $H$ be the $n_B \times n_A$ binary biadjacency matrix of $G$. The quantum code $\mathcal Q_G$ has $n = n_A^2 + n_B^2$ qubits, indexed by $A^2 \cup B^2$ (written $\alpha a$ and $b\beta$), and check matrices

$$H_X = (\mathbb 1_{n_A} \otimes H,\ H^T \otimes \mathbb 1_{n_B}), \qquad H_Z = (H \otimes \mathbb 1_{n_A},\ \mathbb 1_{n_B} \otimes H^T),$$

with rows indexed by $A \times B$ and $B \times A$. The row $ba$ of $H_Z$ has support the Z-generator $g_{ba} = \{\alpha a : \alpha \sim b\} \cup \{b\beta : \beta \sim a\}$. An $X$ error is $e \in \mathbb F_2^{A^2 \cup B^2}$, its syndrome is $\sigma_X(e) = H_X e^T$, and $\mathcal C_Z^\perp$ is the space of sums of Z-generators. The weight $w(e_X, e_Z)$ of a quantum error counts the qubits where $e_X$ or $e_Z$ is nonzero.

The decoder. On a syndrome $s$, one iteration picks a vector $e_1$ whose support lies in some generator $g_{ba}$, such that $s_1 = s + \sigma_X(e_1)$ has $|s_1| < |s|$ and the ratio $(|s| - |s_1|)/|e_1|$ is maximal among all such vectors. It iterates on the current syndrome, fails if it gets stuck at a nonzero syndrome, and otherwise outputs the sum $e_O$ of the flipped vectors. The $Z$ decoder is the same with $H_X$ and $H_Z$ exchanged.

Formalization targets

Goal: Theorem 2

Assume $G$ is $(\Delta_A, \Delta_B)$-biregular and $(\gamma_A, \delta_A, \gamma_B, \delta_B)$-left-right expanding with

$$\delta_A < \tfrac16, \qquad \delta_B < \tfrac16,$$

and let $(e_X, e_Z)$ be a quantum error with

$$w(e_X, e_Z) < w_0 = \frac{1}{3(1 + \Delta_B)} \min(\gamma_A n_A, \gamma_B n_B).$$

Then on every run, the $X$ decoder on input $\sigma_X(e_X)$ never outputs a failure and its output satisfies $e_O + e_X \in \mathcal C_Z^\perp$. The $Z$ decoder on $\sigma_Z(e_Z)$ behaves symmetrically, with $e_O + e_Z \in \mathcal C_X^\perp$.

Milestones

In the paper's order of proof:

• Lemma 3, $|\Gamma_u(S_A)| \ge (1 - 2\delta_A)\Delta_A |S_A|$;
• Proposition 4, distance at least $\gamma_A n_A$ for the classical code;
• the distance half of eq. (3), $d_Q \ge \min(d, d^T)$, already posed on the platform;
• Corollary 5, $d_Q \ge \min(\gamma_A n_A, \gamma_B n_B)$;
• the column-weight bound $|\sigma_X(e)| \le \Delta_B |e|$;
• Lemma 7, existence of a critical generator;
• the displays (19), (22), (23), (24) of Appendix B;
• Lemma 8, a step of ratio at least $1/3$ inside a critical generator;
• Lemma 10, the $X$ half of the goal.

Significance

The result. Theorem 2 gives the first family of quantum LDPC codes with an efficient decoder that corrects a number of adversarial errors proportional to the minimum distance. Here that number is of order $\sqrt n$. The same analysis yields a robustness property: low-weight errors have syndromes of proportional weight (Corollary 9 of the paper). Later work on quantum expander codes builds on this analysis, for example on their decoding under random noise (arXiv:1711.08351) and on fault tolerance with constant overhead (arXiv:1808.03821).

Formalizing it. The result is proved on paper. As far as is known, it has no machine-checked proof. The mission produces a formal statement of the decoder and its correctness, and it also produces reusable pieces:

• unique-neighbour expansion;
• the distance of expander codes;
• the distance of hypergraph product codes, tied to an open item of the Tillich–Zémor mission;
• a generic formalization of greedy syndrome-weight decoding.

Difficulty

The obvious quantum analogue of Sipser–Spielman flips single qubits that lower the syndrome weight. It fails because of degeneracy: an error and its sum with a generator have the same syndrome. A small error can therefore look locally like a large one, and no single qubit need be worth flipping. The paper's decoder instead flips arbitrary patterns inside one generator. The difficulty is to show that some pattern always lowers the syndrome weight by a constant fraction of its size. The proof needs a combinatorial structure, the critical generator, whose existence uses unique-neighbour expansion on both sides of the graph, and a case analysis on its six parts. A second difficulty is that the decoder minimizes the syndrome weight, not the error weight, so the intermediate error can grow. Bounding that growth is what limits the guarantee to $w_0$ rather than the distance.

Formalization scope

• The graph is a relation adj : A → B → Prop on finite types, and $H$ = bipMatrix adj : Matrix B A (ZMod 2).
• The published TillichZemor.HGP.Setting is reused. The paper's $H_X$ is TillichZemor.HGP.hz H H and its $H_Z$ is hx H H; the X/Z names are swapped relative to the 2009 paper, and this is checked against eq. (5) in a sanity file.
• Qubits are (A × A) ⊕ (B × B), weights are hammingNorm, and $\mathcal C_Z^\perp$ is CodingTheory.dualCode of ker H_Z.
• Expansion constants are real and cardinalities are compared in $\mathbb R$. Distance statements are per-vector, so no $\infty$-valued minimum distance is cast to a real number.
• The decoder is defined once (Candidate, Step, Reach, DecodesCorrectly), generic in the syndrome and generator matrices. Its ratio is computed in $\mathbb Q$.
• Reach contains every state reachable under any tie-breaking. Correctness requires, at every reachable state, a further step while the syndrome is nonzero, and $e_O + e$ in the row space of the generator matrix once it is zero. Termination is automatic, because each step lowers a natural number.

Additions and omissions.

• The hypothesis $\Delta_A \ge 1$ is added throughout. With $\Delta_A = 0$ the expansion conditions are vacuous, $H = 0$, and every error is invisible.
• In Lemma 8 the vector $e_1$ is required to be nonzero. With $e_1 = 0$ the printed inequality reads $0 \ge 0$.
• Lemma 8 is posed in its first assertion only. The critical generator is taken with respect to a minimum-weight representative of the coset, as in Appendix B.
• The clauses "runs in time linear in the code length" and "letting $\Delta_A$, $\Delta_B$ be fixed and allowing $n_A, n_B$ to grow" are not formalized. The goal holds for every finite graph meeting the hypotheses.

Trivializing formalizations ruled out. The goal names the paper's own decoder, not "there exists a decoder", which a brute-force coset decoder would satisfy. It quantifies over every run, not a single favourable one. It asserts both never-failing and correctness, not partial correctness alone. It uses $H_X$ = hz H H, not the swapped matrix.

Welcome contributions. Proofs of the counting milestones (Lemma 3, Proposition 4, the column-weight bound, (19), (22)–(24)) are independent of one another. The distance bound of Tillich–Zémor, open on the platform, is the deepest dependency. Unique-neighbour expansion and the hypergraph-product distance bound are useful beyond this mission.

Selected references

• A. Leverrier, J.-P. Tillich, G. Zémor, Quantum expander codes, FOCS 2015; arXiv:1504.00822v1 (2015). https://arxiv.org/abs/1504.00822
• J.-P. Tillich, G. Zémor, Quantum LDPC codes with positive rate and minimum distance proportional to the square root of the blocklength, IEEE Trans. Inf. Theory 60(2), 2014; arXiv:0903.0566. https://arxiv.org/abs/0903.0566
• M. Sipser, D. A. Spielman, Expander codes, IEEE Trans. Inf. Theory 42(6), 1996. https://doi.org/10.1109/18.556667
• O. Fawzi, A. Grospellier, A. Leverrier, Efficient decoding of random errors for quantum expander codes, STOC 2018; arXiv:1711.08351. https://arxiv.org/abs/1711.08351
• O. Fawzi, A. Grospellier, A. Leverrier, Constant overhead quantum fault-tolerance with quantum expander codes, FOCS 2018; arXiv:1808.03821. https://arxiv.org/abs/1808.03821

Why noisy secrets need sketches

Biometric readings, physical unclonable functions and typed passphrases share two defects as cryptographic keys: they are not uniformly distributed, and they are never reproduced exactly. Dodis, Ostrovsky, Reyzin and Smith (SIAM J. Comput. 38(1), 2008; preprint arXiv:cs/0602007v4) introduced the secure sketch to handle the second defect without destroying what entropy the secret has. A secure sketch publishes a string $s$ from which any reading close to the original recovers the original exactly, while the original keeps a guaranteed amount of min-entropy given $s$. Many sources of noise are not substitutions but insertions and deletions: keystroke sequences, sequenced DNA, and any reading whose alignment drifts. For these the relevant distance is the edit distance, and §7 of the paper gives a secure sketch for it.

This mission formalizes that construction: Theorem 7.5 (p. 27), together with the results it is assembled from, PinSketch for set difference (Theorem 6.3, p. 23, with the BCH decoding argument of Appendix E) and the shingling embedding (Lemma 7.3, p. 25), glued by Lemma 4.7 (p. 15).

Setting

All logarithms are base 2. A random variable is identified with its distribution. The min-entropy of $W$ is $\mathbf H_\infty(W) = -\log \max_w \Pr[W = w]$, and the average min-entropy of $W$ given $I$ is $\tilde{\mathbf H}_\infty(W \mid I) = -\log \sum_i \max_w \Pr[W = w \wedge I = i]$.

Let $\mathcal M$ be a set with an integer-valued distance $\mathrm{dis}$. An average-case $(\mathcal M, m, \tilde m, t)$-secure sketch is a pair of randomized procedures $(\mathsf{SS}, \mathsf{Rec})$ such that $\mathsf{Rec}(w', \mathsf{SS}(w)) = w$ whenever $\mathrm{dis}(w, w') \le t$, and $\tilde{\mathbf H}_\infty(W \mid \mathsf{SS}(W), I) \ge \tilde m$ for every pair $(W, I)$ with $\tilde{\mathbf H}_\infty(W \mid I) \ge m$. The difference $m - \tilde m$ is the entropy loss.

Three spaces occur.

1. $\mathrm{Edit}_{\mathcal F}(n)$: strings of length $n$ over a finite alphabet $\mathcal F$ of $F$ letters, with distance the smallest number of character insertions and deletions turning one string into the other.
2. $\mathrm{SDif}(\mathcal U)$: all subsets of a finite universe $\mathcal U$, with distance $|w \triangle w'|$.
3. For PinSketch, $\mathcal U = GF(2^\mu)^*$, of size $n = 2^\mu - 1$. A subset $w$ has syndrome entries $s_i(w) = \sum_{x \in w} x^i$, computed in the field. PinSketch publishes $(s_1, s_3, \dots, s_{2t-1})$.

A $c$-shingle of a string is a length-$c$ consecutive substring, and the $c$-shingling $\mathrm{SH}_c(w) \subseteq \mathcal F^c$ is the set of all of them. A map $f : \mathcal M_1 \to \mathcal M_2$ is a $(t_1, t_2, \lambda)$-biometric embedding with recovery information $g$ if it maps distance $\le t_1$ to distance $\le t_2$, $g$ takes at most $2^\lambda$ values, and $w$ is determined by $(f(w), g(w))$.

Formalization targets

Goal: Theorem 7.5

For every finite alphabet $\mathcal F$ with $F$ letters, all $n, c, t \in \mathbb N$ with $1 \le c \le n$ and every real $m$, there is an average-case secure sketch

$$\Big(\mathrm{Edit}_{\mathcal F}(n),\ m,\ m - \big\lceil \tfrac nc \big\rceil \log_2(n - c + 1) - (2c - 1)\,t\,\lceil \log(F^c + 1) \rceil,\ t\Big).$$

Milestones

1. Set difference. Theorem 6.3: PinSketch is an average-case $(\mathrm{SDif}(\mathcal U), m, m - t\log(n+1), t)$ secure sketch. On the way:
   • the Appendix E identity $s_{2i} = s_i^2$;
   • the key equation $S(z)\sigma(z) \equiv \omega(z) \bmod z^\delta$;
   • the uniqueness of $\omega/\sigma$ among low-degree solutions;
   • Lemma 6.2: a word of weight $\le (\delta - 1)/2$ is determined by its first $\delta - 1$ syndromes;
   • step 4 of Construction 6: decoding returns $w \triangle w'$.
2. Edit distance into set difference. Lemma 7.3: $\mathrm{SH}_c$ is an average-case $(t_1, (2c-1)t_1, m_1, m_1 - \lceil n/c \rceil \log_2(n - c + 1))$ biometric embedding. Its strengthening: $\mathrm{SH}_c$ has recovery information $g_c$ with $\lambda = \lceil n/c \rceil \log_2(n - c + 1)$.
3. Composition. Lemma 4.7: an embedding with recovery information turns an average-case sketch on $\mathcal M_2$ for entropy $m_1 - \lambda$ into one on $\mathcal M_1$ for entropy $m_1$, with the same residual entropy.

Significance

Theorem 7.5 gives a secure sketch for the edit metric whose entropy loss is, for a good choice of $c$, about $2.38\,(t \log F)^{1/3}(n \log n)^{2/3}$ (p. 26). This is sublinear in $n$ for $t$ up to nearly linear, and for large $t$ it improves on the low-distortion embedding approach of §7.1. Combined with a strong extractor it yields fuzzy extractors for edit distance (Theorem 7.4). PinSketch is itself the standard set-difference sketch, and Lemma 4.7 is a general transfer principle between metrics.

All results here are proved in the paper. None has a machine-checked proof that we know of. A complete development would also formalize a fragment of BCH decoding over $GF(2^\mu)$, the syndrome-uniqueness theorem for binary BCH codes, and a combinatorial lemma on how insertions and deletions act on shingle sets. Each is reusable outside this mission.

Difficulty

There are two hard steps.

The first is Lemma 6.2. That a low-weight word is determined by $\delta - 1$ power sums is a statement about Vandermonde systems in characteristic 2, where the even power sums carry no new information. Newton's identities, the usual characteristic-zero route from power sums to elementary symmetric functions, fail there because they divide by integers that vanish in characteristic 2. The paper argues through the error-locator and error-evaluator polynomials instead.

The second is the distance clause of Lemma 7.3. An edit path between two strings of length $n$ passes through strings of other lengths, so a per-step bound on the shingle sets must hold for strings of every length, including lengths below $c$.

The entropy statements involve average min-entropy over arbitrary auxiliary variables, and each needs the chain-rule bound of Lemma 2.2(b) in average-case form.

Formalization scope

• Laws and kernels. Random variables are PMFs, and randomized procedures are kernels M → PMF S. The auxiliary variable of every average-case statement ranges over every ι : Type, not only finite types. Average min-entropy uses the joint form above. "Min-entropy $m$" means $\ge m$, and $m$ is real.
• The field. The paper's $GF(2^m)$ is any finite field K of characteristic 2, and its degree is renamed $\mu$ because $m$ denotes min-entropy. Appendix E's large field $\mathcal F$ is this K, distinct from §7's alphabet $\mathcal F$. Only binary words are formalized, as subsets (Finset Kˣ); the $q$-ary generality of Lemma E.1 is not.
• The key equation. $\omega(z)$ is written without division, congruence mod $z^\delta$ is divisibility by $X^\delta$, and the ratio identity is cross-multiplied.
• Edit distance. It reuses the published weighted edit distance MasekPaterson.Shared.editDist with cost 1 per insertion or deletion and 2 per replacement, which equals the insertion/deletion count.
• Shingling and $g_c$. Shingling is defined for strings of all lengths. $g_c$ is the concrete function of the proof, with 0-based indices.
• Explicit hypotheses.
  • The Appendix E uniqueness statement takes the BCH designed distance to satisfy $1 \le \delta$; at $\delta=0$ its congruence is vacuous and the conclusion can fail.
  • $1 \le c \le n$, which the paper leaves implicit, is assumed in Lemma 7.3 and Theorem 7.5.
  • $\epsilon$ is dropped from Theorem 7.5, where it does not occur in the conclusion.
  • $\lceil \log(F^c + 1) \rceil$ is Nat.clog 2 (F ^ c + 1).
• Misprints, read as corrected.
  • In Definition 7, $f(w_2)$ is read as $f(w_1')$.
  • In Lemma 4.7, $\mathsf{Rec}(w', s)$ is read as $\mathsf{Rec}(f(w'), s)$.
  • In Appendix E, $w'(z)$ is read as $\omega'(z)$.
• Efficiency. Every claim of efficiency or running time (Lemma 6.2, Theorem 6.3, Theorem 7.5) is dropped: Mathlib has no complexity substrate, and no vacuous substitute is used.
• Excluded trivializations. The distance is the insertion/deletion distance, not the Hamming distance on length-$n$ strings (a different and easier problem). It is not a degenerate cost that is identically 0: insertion and deletion each cost 1.
• Not posed here. Lemma 2.2(b) and Lemma 3.1 are posed in the companion mission on Hamming fuzzy extractors. Proofs that need them may restate them.

Contributions are welcome on any milestone. The BCH part (Appendix E, Lemma 6.2) and the shingling part (Lemma 7.3) are independent.

Selected references

• Y. Dodis, R. Ostrovsky, L. Reyzin, A. Smith, Fuzzy Extractors: How to Generate Strong Keys from Biometrics and Other Noisy Data, SIAM J. Comput. 38(1):97–139, 2008. https://doi.org/10.1137/060651380 ; arXiv:cs/0602007v4, https://arxiv.org/abs/cs/0602007
• J. H. van Lint, Introduction to Coding Theory, 2nd ed., Springer, 1992 (BCH codes and their decoding; the reference [vL92] of Appendix E).
• A. Z. Broder, On the resemblance and containment of documents, Compression and Complexity of Sequences, IEEE, 1997 (shingling). https://doi.org/10.1109/SEQUEN.1997.666900
• W. J. Masek, M. S. Paterson, A faster algorithm computing string edit distances, J. Comput. System Sci. 20(1):18–31, 1980 (the weighted edit distance reused here). https://doi.org/10.1016/0022-0000(80)90002-1

Minimum discrimination information under moment constraints

Given a reference probability distribution $R$ and a set $\mathcal E$ of probability distributions, the minimum discrimination information problem asks for the member of $\mathcal E$ closest to $R$ in Kullback–Leibler divergence. It is the basis of Kullback's information-theoretic approach to statistics (Kullback 1959), of the maximum-entropy principle of statistical physics (Jaynes 1957), and of large-deviation theory, where Sanov's theorem identifies the rate function of an empirical distribution with exactly this minimum. The most common constraint sets are defined by prescribed expectations $\int f_i\,dP = a_i$, and the classical answer is that the minimizer is an exponential family member, with density $c\exp\sum_i t_i f_i$ with respect to $R$.

That answer was usually justified by Lagrange multipliers, which presuppose that a minimizer exists. Csiszár's paper (Ann. Probab. 1975) treats the problem geometrically, with I-divergence in the role of squared Euclidean distance, and its last result, Theorem 3.3, proves existence and the exponential form at once for unbounded constraint functions, under a hypothesis on the exponential moments of the $f_i$.

Timeline:

• 1959: Kullback formulates the minimum discrimination information theorem: an element of $\mathcal E$ of exponential form is the minimizer (a sufficient condition).
• 1966: Kullback and Khairat (Ann. Math. Statist. 37, 1966) refine the sufficient condition.
• 1972: Čencov proves existence of exponential-form minimizers under general conditions (Statistical Decision Rules and Optimal Inference, Theorem 23.1).
• 1975: Csiszár proves Theorem 3.3 by the minimizing-sequence method of his Theorem 2.1; a first version of the paper assumed $T_R = E^k$, weakened to "$T_R$ open" after Čencov's work.

Setting

All distributions (PD's) live on one measurable space $(X,\mathcal X)$. The I-divergence of $P$ from $Q$ is

$$I(P\|Q)=\int \log p_Q\,dP\ \text{ if } P\ll Q,\qquad I(P\|Q)=+\infty\ \text{ otherwise},$$

where $p_Q$ is the density of $P$ with respect to $Q$; it takes values in $[0,\infty]$ and vanishes only for $P=Q$. The variation distance is $|P-Q|=\int|p_R-q_R|\,dR$ for any PD $R$ dominating both. If $\mathcal E$ is a convex set of PD's containing some $P$ with $I(P\|R)<\infty$, a $Q\in\mathcal E$ with

$$I(Q\|R)=\min_{P\in\mathcal E} I(P\|R)$$

is the I-projection of $R$ on $\mathcal E$.

Fix real-valued measurable functions $f_1,\dots,f_k$ on $X$. For $a=(a_1,\dots,a_k)\in E^k$ (Euclidean $k$-space) the moment set $\mathcal E(a)$ is the set of PD's $P$ with $\int f_i\,dP=a_i$, $i=1,\dots,k$. Further:

• $A_R$ is the set of $a\in E^k$ for which $\mathcal E(a)$ contains some $P$ with $I(P\|R)<\infty$;
• $T_R=\{t\in E^k:\ \exp\sum_i t_i f_i \text{ is } R\text{-integrable}\}$, (3.16);
• $F(a)=\inf_{P\in\mathcal E(a)} I(P\|R)$, (3.18), the optimal value as a function of the constraint levels.

Formalization targets

Goal: Theorem 3.3

If $T_R$ is open in $E^k$, then for every point $a$ of the interior of $A_R$ the I-projection $Q$ of $R$ on $\mathcal E(a)$ exists and

$$q_R(x)=c\exp\sum_{i=1}^k t_i f_i(x)\qquad R\text{-a.e.},$$

for some constant $c$ and some $t\in E^k$.

Milestones

1. (2.2), the parallelogram identity: $I(P_m\|R)+I(P_n\|R)=2I(\tfrac{P_m+P_n}2\|R)+I(P_m\|\tfrac{P_m+P_n}2)+I(P_n\|\tfrac{P_m+P_n}2)$.
2. (2.4): a minimizing sequence $P_n$ in a convex set converges in variation to a PD $Q\ll R$ (closedness of the set is not used).
3. Lemma 3.1: if $e^{tf}$ is $Q$-integrable for small $|t|$, then $I(P_n\|Q)\to0$ implies $\int f\,dP_n\to\int f\,dQ$.
4. (3.18): $A_R$ is convex and $F$ is finite and convex on $A_R$.
5. (3.19): at an interior point $a$ of $A_R$ there is $t$ with $F(b)\ge F(a)+\sum_i t_i(b_i-a_i)$ for all $b\in A_R$.
6. Remark, p. 158: $F$ is differentiable at interior points of $A_R$, and $\operatorname{grad}F(a)=t$, the parameter vector of the I-projection.

Significance

Theorem 3.3 gives existence of maximum-entropy (minimum discrimination information) distributions under finitely many moment constraints with unbounded constraint functions, which covers the usual exponential families of statistics (normal, gamma, Poisson moment constraints) where boundedness fails. It identifies the minimizer's form without assuming a minimizer exists, and the Remark identifies the natural parameters as the gradient of the optimal value, the sensitivity interpretation of Lagrange multipliers. These facts underlie the duality between moment and natural parameters of exponential families and the rate functions of Cramér and Sanov type.

The result is proved, in this paper and (under a slightly weaker hypothesis) by Čencov. None of it is formalized: Mathlib has the Kullback–Leibler divergence of measures (InformationTheory.klDiv) and tilted measures, but no I-projection, no existence theorem for constrained minimizers of KL divergence and no exponential-form characterization. The mission produces a machine-checked version of the existence and form theorem, together with the general steps it uses (the parallelogram identity, convergence of minimizing sequences in variation, continuity of exponential-moment expectations under KL convergence).

Difficulty

The obvious argument fails at the first step: the moment set $\mathcal E(a)$ is convex but not closed in variation when the $f_i$ are unbounded, since $\int f_i\,dP$ is not continuous in variation. A minimizing sequence therefore converges in variation to some $Q$ (as in Theorem 2.1), but nothing places $Q$ in $\mathcal E(a)$: mass can escape to where $|f_i|$ is large. Ruling this out needs quantitative control of $I(P_n\|Q)$, which in turn requires knowing the form of $Q$ before knowing $Q$ is feasible; the interplay with the convexity of $F$ and the openness of $T_R$ is where the work lies. A Lagrange-multiplier argument is not available: it presupposes a minimizer and differentiability that are part of the conclusion.

Formalization scope

• Probability distributions are Measure X with IsProbabilityMeasure; the I-divergence is Mathlib's klDiv : ℝ≥0∞, which for probability measures equals (1.1) with the conventions $\log 0=-\infty$, $\log\frac a0=+\infty$, $0\cdot(\pm\infty)=0$.
• The variation distance uses $P+Q$ as dominating measure (the page allows any dominating PD; the value is the same).
• The I-projection carries $I(Q\|R)<\infty$ explicitly: the page defines it only when $\mathcal E$ meets $\{P: I(P\|R)<\infty\}$.
• $\mathcal E(a)$ requires $P$-integrability of every $f_i$, so the constraint integrals are genuine. $E^k$ is Fin k → ℝ with its product (Euclidean) topology; "inner point" is the topological interior. $k=0$ is allowed.
• $F$ is an infimum in $[0,\infty]$ (equal to $\infty$ outside $A_R$); statements use its real value only on $A_R$, where it is finite. (3.18) prints $I(P\|Q)$; the reference measure is $R$, as the definition of $A_R$ and the proof show. (3.16) prints $(t_1,\dots,t_n)$ for $(t_1,\dots,t_k)$.
• Densities are Radon–Nikodym derivatives and the form (3.2) is an $R$-almost-everywhere identity with no exceptional set of positive measure.
• Lemma 3.1 asserts that $f$ is $P_n$-integrable for large $n$ as well as the convergence, so that $\int f\,dP_n$ is not a default value.
• Trivializing readings are excluded: the goal asserts existence of the I-projection rather than assuming it, $T_R$ is an integrability set (not a set where a junk integral is finite), and the infimum is never a real sInf over a possibly empty set.

A complete development needs: Radon–Nikodym calculus for klDiv (the identity (2.6) $I(P\|R)-I(P\|Q)=\int\log q_R\,dP$), Pinsker's inequality (available on the platform as a reference item), lower semicontinuity of klDiv under convergence in variation, completeness of the space of PD's in variation, and supporting hyperplanes of finite-dimensional convex functions. The KL parallelogram identity, Lemma 3.1 and the variation-distance facts are reusable well beyond this mission. Contributions on any milestone, and on these infrastructure lemmas, are welcome.

Selected references

• I. Csiszár, I-divergence geometry of probability distributions and minimization problems, Ann. Probab. 3(1), 146–158, 1975. https://doi.org/10.1214/aop/1176996454
• S. Kullback, Information Theory and Statistics, Wiley, 1959.
• S. Kullback and M. A. Khairat, A note on minimum discrimination information, Ann. Math. Statist. 37, 279–280, 1966.
• E. T. Jaynes, Information theory and statistical mechanics, Phys. Rev. 106, 620–630, 1957. https://doi.org/10.1103/PhysRev.106.620
• N. N. Čencov, Statistical Decision Rules and Optimal Inference (Russian), Nauka, 1972; English translation, American Mathematical Society, 1982.
• I. N. Sanov, On the probability of large deviations of random variables (Russian), Mat. Sbornik 42, 11–44, 1957.

Why count copies of a quantum state

A mixed state of a $D$-dimensional quantum system is a $D\times D$ positive semidefinite matrix $\rho$ of trace $1$. Writing $\rho$ down takes about $D^2$ real numbers, and $D$ is exponential in the number of qubits, so learning $\rho$ in full is expensive. Holevo's theorem and the random access code bounds of Ambainis, Nayak, Ta-Shma and Vazirani say that an $n$-qubit state carries far fewer usable classical bits than its $2^n$ amplitudes suggest. Shadow tomography, introduced by S. Aaronson (arXiv:1711.01053), makes this quantitative: given $M$ known two-outcome measurements $E_1,\dots,E_M$, how many copies of an unknown $\rho$ are needed to estimate every acceptance probability $\operatorname{Tr}(E_i\rho)$ to within $\varepsilon$?

Aaronson shows that $\widetilde O(\log^4 M\cdot\log D/\varepsilon^4)$ copies suffice, polylogarithmic in $M$ and $D$. The question this mission addresses is the converse: how many copies are necessary. Section 6 of the paper proves two lower bounds. Theorem 16 gives $\Omega(\min\{D,\log M\}/\varepsilon^2)$ even when $\rho$ and the $E_i$ are diagonal (a classical distribution). Theorem 19, the goal here, strengthens the dimension term to $D^2$ for genuinely quantum states.

Timeline:

• 2016: full tomography of a $D$-dimensional state to trace-distance accuracy $\varepsilon$ needs $\Theta(D^2/\varepsilon^2)$ copies up to logarithmic factors, with upper and lower bounds by O'Donnell and Wright (arXiv:1508.01907) and Haah, Harrow, Ji, Wu and Yu (arXiv:1508.01797).
• 2017–2018: Aaronson poses shadow tomography (Problem 1), proves the polylogarithmic upper bound (Theorem 2), and proves the lower bounds of Theorems 16 and 19.
• 2020 onward: classical shadows (Huang, Kueng and Preskill, arXiv:2002.08953) and later shadow-tomography algorithms study the same estimation task with other measurement models and improved upper bounds.

Setting

Fix a dimension $D$. A two-outcome measurement is a $D\times D$ Hermitian matrix $E$ with $0\preceq E\preceq I$; it accepts $\rho$ with probability $\operatorname{Tr}(E\rho)$. The tensor power $\rho^{\otimes k}$ is the $D^k\times D^k$ matrix of $k$ independent copies. A strategy using $k$ copies is a measurement of $\rho^{\otimes k}$ with finitely many outcomes $\omega\in\Omega$, given by positive semidefinite matrices $\Pi_\omega$ with $\sum_\omega\Pi_\omega = I$, together with outputs $b(\omega)=(b_1(\omega),\dots,b_M(\omega))$. It succeeds on $\rho$ when, with probability at least $2/3$ over $\omega$, $|b_i(\omega)-\operatorname{Tr}(E_i\rho)|\le\varepsilon$ for every $i\in[M]$.

The proof works with these further objects, all defined in the mission:

• an orthogonal projection $\mathbb P$ onto an $N/2$-dimensional subspace of $\mathbb C^N$ (Hermitian, idempotent, trace $N/2$);
• $\rho_{\mathbb P} := \tfrac2N\mathbb P$, the maximally mixed state on that subspace;
• $\sigma_{\mathbb P,\varepsilon} := (1-6\varepsilon)\,\mathbb I/N + 6\varepsilon\,\rho_{\mathbb P}$;
• the von Neumann entropy in bits, $S(\rho) = -\sum_x\lambda_x\log_2\lambda_x$ over the eigenvalues of $\rho$;
• for states $\sigma_1,\dots,\sigma_K$ and $\zeta := \tfrac1K\sum_i\sigma_i^{\otimes T}$, the quantum mutual information with the classical index, $I(\zeta;i) := S(\zeta) - \tfrac1K\sum_i S(\sigma_i^{\otimes T})$.

Formalization targets

Goal: Theorem 19 (p. 23)

There are a universal constant $c>0$ and a threshold $N_0$ such that for all $D\ge N_0$, all $M$ with $\log_2 M\ge N_0^2$ and all $0<\varepsilon\le\tfrac16$, some measurements $E_1,\dots,E_M$ on $\mathbb C^D$ force every strategy that succeeds on every mixed state to use

$$k \;\ge\; c\,\frac{\min\{D^2,\ \log_2 M\}}{\varepsilon^2}$$

copies. The goal fixes only the shape $\Omega(\min\{D^2,\log M\}/\varepsilon^2)$, not a constant, so a sharper constant does not invalidate it.

Milestones (pp. 23–24)

The milestones follow the proof, which sets $N:=\lfloor\min\{D,\sqrt{\log_2 M}\}\rfloor$ and $K:=\lfloor c^{N^2}\rfloor$:

1. Eq. (2): for some $c\in(1,2)$ and all large even $N$ there are $K$ projections $\mathbb P_i$ of rank $N/2$ with $|\operatorname{Tr}(\mathbb P_i\rho_j)-\tfrac12|\le\tfrac1{12}$ for all $i\ne j$.
2. $\operatorname{Tr}(\mathbb P_i\sigma_i) = \tfrac12+3\varepsilon$.
3. $|\operatorname{Tr}(\mathbb P_j\sigma_i)-\tfrac12| = 6\varepsilon|\operatorname{Tr}(\mathbb P_j\rho_i)-\tfrac12|\le\tfrac\varepsilon2$ for $i\neq j$.
4. The exact entropy $S(\sigma_i) = \log_2 N - [1-h(\tfrac12+3\varepsilon)]$, with $h$ the binary entropy, and the bound $S(\sigma_i)\ge\log_2 N - C\varepsilon^2$.
5. $I(\zeta;i)\le T(\log_2 N - S(\sigma_i))$ when all $\sigma_i$ have equal entropy.

Significance

Theorem 19 shows that the $\log M$ dependence of shadow tomography cannot be removed, and that for $M\ge 2^{D^2}$ shadow tomography is as hard as full tomography: as $M$ grows the bound becomes the $\Omega(D^2/\varepsilon^2)$ tomography lower bound, which it therefore contains. Compared with the classical Theorem 16, it shows that quantum states need quadratically more copies in the dimension term. The $1/\varepsilon^2$ factor matches the upper bound of Proposition 20 for the decision version, so the $\varepsilon$-dependence of the lower bound is tight in that setting.

The results are proved in the paper; none of them has a machine-checked proof that we know of. Formalizing the argument requires von Neumann entropy and its additivity on tensor products, the bound $S\le\log_2(\text{dimension})$, a Holevo-plus-Fano step that turns successful estimation into mutual information, and the existence of many nearly orthogonal half-dimensional subspaces. Each is reusable well beyond this mission.

Difficulty

The obvious attempt adapts the classical argument of Theorem 16, which hides $K$ subsets of $[N]$ in a biased distribution. Quantum states allow $\exp(\Omega(N^2))$ hidden subspaces instead of $\exp(\Omega(N))$ subsets, which is where $D^2$ comes from, but two steps change character. First, the hiding family must be shown to exist: Eq. (2) is a concentration statement for random subspaces, and the lemma the paper cites for it (Lemma 18) is misstated, as explained below. Second, the information bound must be carried out for quantum states: the step "learning $i$ from $\zeta$ requires $I(\zeta;i)\ge\log_2 K$" needs Holevo's bound and Fano's inequality, adjusted for success probability $2/3$ rather than certainty.

Formalization scope

Matrices are Matrix n n ℂ over a finite index type; the goal uses $n=\texttt{Fin } D$. Conventions committed to:

• A mixed state is the published WildeQIT.IsDensityOperator (positive semidefinite, trace $1$), reused as a reference item.
• A strategy is a finite-outcome POVM on $\rho^{\otimes k}$, indexed by Fin k → Fin D, with deterministic outputs $b(\omega)\in\mathbb R^M$; classical randomness can be absorbed into the outcome set.
• Probabilities and traces are real parts of complex traces. Entropies use $\log_2$; Lean's $\log_2 0 = 0$ gives $0\log 0=0$, and vnEntropy returns $0$ on non-Hermitian matrices, which no statement uses.
• Added to the goal: the threshold $N_0$ on $D$ and $\sqrt{\log_2 M}$ (for $D=1$, $k=0$ succeeds) and $\varepsilon\le\tfrac16$ (for $\varepsilon\ge\tfrac12$, the output $b_i=\tfrac12$ succeeds with $k=0$). Problem 1's $b_i\in[0,1]$ is dropped, an equivalent statement under clipping.
• The measurements are chosen before the strategy (for every strategy, the same $E$), which is the meaning of a lower bound.

A trivializing formalization is ruled out: the goal does not mention $N$, $K$, $\mathbb P_i$, $\sigma_i$ or $\zeta$, the success condition quantifies over all mixed states rather than a vacuous class, and the measurements are fixed before the strategy.

Not drafted:

• Lemma 18 (pp. 22–23) is false as printed. Since $\mathbb E_S[\rho_S] = \mathbb I/N$, $\operatorname{Tr}(\mathbb P_T\rho_S)$ concentrates at $1/2$, not $1/4$. The proof needs only Eq. (2), which is centred correctly and is a milestone.
• Eq. (2) is stated as existence, not as "probability $1-o(1)$ over Haar-random subspaces", because Mathlib has no Haar measure on the unitary group or the Grassmannian; existence is what the proof uses.
• "$I(\zeta;i)$ must be at least $\log_2 K$" is not drafted: as stated it is imprecise for success probability $2/3$, and the correct Holevo–Fano form is left to the solver.
• The final combination $I(\zeta;i)=O(T\varepsilon^2)$, $T=\Omega(N^2/\varepsilon^2)$ is the goal's last step.

Contributions welcome: proofs of the milestones; a Haar-measure version of Eq. (2); von Neumann entropy infrastructure (additivity, the dimension bound, concavity); Holevo's bound and Fano's inequality for finite-dimensional states.

Selected references

• S. Aaronson, Shadow Tomography of Quantum States, arXiv:1711.01053v2, 2018; STOC 2018. https://arxiv.org/abs/1711.01053
• P. Hayden, D. Leung, A. Winter, Aspects of generic entanglement, Comm. Math. Phys. 265, 2006. https://arxiv.org/abs/quant-ph/0407049
• R. O'Donnell, J. Wright, Efficient quantum tomography, STOC 2016. https://arxiv.org/abs/1508.01907
• J. Haah, A. W. Harrow, Z. Ji, X. Wu, N. Yu, Sample-optimal tomography of quantum states, IEEE Trans. Inf. Theory 63, 2017. https://arxiv.org/abs/1508.01797
• A. Ambainis, A. Nayak, A. Ta-Shma, U. Vazirani, Dense quantum coding and quantum finite automata, J. ACM 49, 2002. https://arxiv.org/abs/quant-ph/9804043
• H.-Y. Huang, R. Kueng, J. Preskill, Predicting many properties of a quantum system from very few measurements, Nature Physics 16, 2020. https://arxiv.org/abs/2002.08953

Motivation

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

$$H(A|BC)_\rho \le H(A|B)_\rho .$$

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

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

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

Setting

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

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

$$H_{\min}(A|B)_\rho=\max\{\lambda\in\mathbb R : \exists\,\sigma_B\in S_=(\mathcal H_B),\ \rho_{AB}\le 2^{-\lambda}\,\mathbb 1_A\otimes\sigma_B\}.$$

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

$$H^\varepsilon_{\min}(A|B)_\rho=\max_{\rho'\in\mathcal B^\varepsilon(\rho_{AB})}H_{\min}(A|B)_{\rho'} .$$

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

Formalization targets

Goal: the von Neumann entropy DPI (Theorem 3)

$$H(A|BC)_\rho\le H(A|B)_\rho\qquad(\rho\in S_=(\mathcal H_{ABC})).$$

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

The smooth min-entropy DPI (Theorem 1)

$$H^\varepsilon_{\min}(A|BC)_\rho\le H^\varepsilon_{\min}(A|B)_\rho .$$

The QAEP (Theorem 2)

$$\lim_{\varepsilon\to0}\lim_{n\to\infty}\frac1n H^\varepsilon_{\min}(A^n|B^n)_{\rho^{\otimes n}}=H(A|B)_\rho ,$$

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

Significance

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

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

Difficulty

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

Formalization scope

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

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

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

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

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

Selected references

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