Information Theory

Motivation

Distributionally robust optimization evaluates a decision against a set of plausible probability laws rather than against a single estimated law. A common way to specify that set is to choose a nominal law $P_0$ and allow every law $P$ whose discrepancy from $P_0$ is below a radius $\varepsilon$. Different discrepancies produce different ambiguity sets, so comparing them tells a modeler what one constraint guarantees about another. Rahimian and Mehrotra collect such constructions in their survey and state a chain of comparisons among variation, Hellinger, Kullback–Leibler, and J-divergences in Lemma 5.4 (arXiv:1908.05659v1, pp. 31, 34–35). The chain connects four common ways of controlling model error without requiring a finite outcome space or a common density chosen in advance.

The source is the 2019 arXiv v1 preprint of a survey. Its proof of Lemma 5.4 cites earlier work rather than giving a full derivation. The preprint also prints an additional J-to-$\chi^2$ comparison that is false; this mission isolates the part that holds for every pair of probability measures. The distinction matters when an ambiguity set is used to certify a bound under a different divergence: an inclusion based on the false link can certify laws that are outside the intended set.

Setting

Let $(\Xi,\mathcal F)$ be a measurable space, and let $\mathfrak M(\Xi,\mathcal F)$ be its probability measures. Given $P_1,P_2\in\mathfrak M(\Xi,\mathcal F)$, a $\phi$-divergence $\mathfrak D^\phi(P_1,P_2)$ compares their densities using a function $\phi:[0,\infty)\to[0,\infty]$ with $\phi(1)=0$. The paper assumes $\phi$ is convex. To account for measures that are not mutually absolutely continuous, take the common dominating measure $\nu=P_1+P_2$ and write $p=dP_1/d\nu$ and $q=dP_2/d\nu$. The integrand is $q\phi(p/q)$ when $q>0$ and $p\phi'(\infty)$ when $q=0$, where $\phi'(\infty)=\lim_{t\to\infty}\phi(t)/t$; a point with $p=q=0$ contributes zero (§5.1.2, p. 31).

Table 1 gives four generators used here:

$$\phi_v(t)=|t-1|,\qquad \phi_h(t)=(\sqrt t-1)^2,\qquad \phi_{\mathrm{kl}}(t)=t\log t-t+1,\qquad \phi_j(t)=(t-1)\log t.$$

The first two divergences are the full $L^1$ variation discrepancy and the unhalved squared Hellinger discrepancy. In particular, $\mathfrak D^{\phi_v}=2d_{\mathrm{TV}}$, where $d_{\mathrm{TV}}$ is the total variation distance defined later in the paper. The J generator has $\phi_j(0)=+\infty$, understood as its limit at zero; $\phi_{\mathrm{kl}}(0)=1$ under $0\log0=0$. The recession slopes of the four generators, in the displayed order, are $1,1,+\infty,+\infty$ (Table 1, p. 31; §5.1.3, p. 35).

For a nominal probability measure $P_0$ and a nonnegative radius $\varepsilon$, equation (5.9) defines the ambiguity ball

$$\mathcal P^\phi(P_0;\varepsilon) =\{P\in\mathfrak M(\Xi,\mathcal F):\mathfrak D^\phi(P,P_0)\le\varepsilon\}.$$

Formalization targets

The three milestone comparisons are the valid initial part of (5.10), for every $P,P_0\in\mathfrak M(\Xi,\mathcal F)$:

$$\frac14\bigl(\mathfrak D^{\phi_v}(P,P_0)\bigr)^2 \le\mathfrak D^{\phi_h}(P,P_0) \le\mathfrak D^{\phi_{\mathrm{kl}}}(P,P_0) \le\mathfrak D^{\phi_j}(P,P_0).$$

The middle comparison is also stated in footnote 18. The mission goal is the corrected Lemma 5.4: it joins these three comparisons to the resulting valid part of (5.11), for every nominal $P_0$ and radius $\varepsilon$:

$$\mathcal P^{\phi_j}(P_0;\varepsilon) \subseteq\mathcal P^{\phi_{\mathrm{kl}}}(P_0;\varepsilon) \subseteq\mathcal P^{\phi_h}(P_0;\varepsilon) \subseteq\mathcal P^{\phi_v}(P_0;2\sqrt\varepsilon).$$

Each inclusion has the direction induced by the preceding divergence inequality: a stronger divergence constraint gives a smaller ball. The first comparison retains the paper's factor $1/4$, and the final ball retains its radius $2\sqrt\varepsilon$ (Lemma 5.4, p. 34).

Significance

The result allows a J-divergence or KL-divergence ambiguity model to carry a simultaneous bound in Hellinger and full variation divergence. A Hellinger radius $\varepsilon$ yields the explicit variation radius $2\sqrt\varepsilon$; this makes the scale change visible when comparing two models built with different discrepancies. Without a general-measure statement, a finite-outcome approximation does not itself cover continuous laws or pairs with a singular component.

The paper presents the inequalities as known and cites sources for them. A finite-alphabet TV–Hellinger–KL chain and a general-measure KL–affinity bound already have machine-checked results in the platform catalog. The work here is to formalize the four generators with one shared general-measure divergence, close the remaining inequalities in that representation, and connect them to the ambiguity-ball inclusions. This also provides reusable definitions for other distributionally robust models that use the same divergence convention.

Difficulty

Writing the density ratio only with respect to $P_0$ loses the part of $P$ singular to $P_0$. That would change both variation and Hellinger divergence and make the stated chain an unreliable comparison of the paper's objects. At the opposite boundary, $P$ can vanish on a set that $P_0$ charges. There the J generator must be infinite, although a direct use of a total real logarithm at zero can assign it an incorrect finite value. These two edge cases make an apparently routine pointwise comparison insufficient for the full measurable-space theorem.

Formalization scope

Lean represents $P$ and $P_0$ as ProbabilityMeasure Ξ on an arbitrary MeasurableSpace Ξ. It computes Radon–Nikodym densities relative to $P+P_0$, evaluates the divergence with an extended nonnegative Lebesgue integral, and represents both divergence values and radii in ENNReal. The generic definition computes the recession slope as a limsup; for the four Table 1 generators this is the limit in the paper. The formal ambiguity ball contains probability measures only. A top radius is allowed by the type; the finite nonnegative radii are the paper's intended model parameters. The generic operation does not take a convexity certificate, but the four named generators are the only ones used in the theorem.

The formalization must not turn a nondominated pair into divergence zero or assign $\phi_j(0)=0$: either choice changes the claimed chain. It must also retain the full variation divergence, without the half factor used for total variation distance. The definitions of the common-measure divergence, its four generators, and the ambiguity ball are intended for reuse. Contributions establishing properties of the recession slopes, comparison lemmas on arbitrary measurable spaces, and their ambiguity-set consequences are within scope.

The paper's final inequality in (5.10), $\mathfrak D^{\phi_j}\le\mathfrak D^{\phi_{\mathrm{ca}^2}}$, and the associated first inclusion in (5.11) are removed. They are false even on a two-point space: with $P_0=(1/2,1/2)$ and $P=(0,1)$, J-divergence is $+\infty$ while the order-two $\chi$-divergence is $1$. Thus $P$ lies in the latter ball of radius $1$ but outside the J ball of that radius. The source's footnote 18 separately notes an error in a cited Hellinger–KL comparison; the corrected Hellinger–KL inequality is retained (pp. 34–35).

Selected references

• H. Rahimian and S. Mehrotra, Distributionally Robust Optimization: A Review, arXiv preprint arXiv:1908.05659v1, 2019. Preprint.

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

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

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

Draw $n$ independent fair bits $X$, compute a one-bit summary $f(X)$, and send the bits through independent binary symmetric channels with crossover probability $\varepsilon$, producing $Y$. Which summary tells the receiver the most about $Y$? Kumar and Courtade conjectured that a single coordinate, $f(X)=X_1$, is optimal: $I(f(X);Y)\le 1-h_2(\varepsilon)$ bits for every Boolean $f$, in every dimension and at every noise level (ISIT 2013; IEEE Trans. Inf. Theory 2014). The Courtade–Kumar (most informative Boolean function) conjecture is a basic question about how noise destroys information on the discrete cube, connecting information theory with Boolean Fourier analysis and hypercontractivity.

This mission asks for a formal proof of a sharp contraction theorem for arbitrary randomized binary summaries, whose Boolean case is the Courtade–Kumar conjecture, as stated in an OpenAI preprint dated September 24, 2026 (source). The preprint has not been peer reviewed and its claims have not been independently verified; on the platform the Lean goal is open.

Background

• 1970–1976 — Hypercontractivity on the cube (Bonami, Ann. Inst. Fourier 1970; Gross, Amer. J. Math. 1975; Beckner, Annals 1975); Mrs. Gerber's lemma (Wyner–Ziv, IEEE TIT 1973).
• 2013–2014 — Kumar and Courtade pose the conjecture and prove a coordinatewise sum bound.
• 2016 — High-noise results: Ordentlich, Shayevitz and Weinstein for balanced functions (ISIT 2016); Samorodnitsky for all Boolean functions in a dimension-independent high-noise range (IEEE TIT 2016).
• 2018 — Pichler, Piantanida and Matz prove coordinate optimality when the observation is also reduced to one bit (Ann. Appl. Probab. 2018).
• 2020–2023 — Barnes–Özgür's symmetrized reformulation (ISIT 2020); Li–Médard on fixed-mean optimizers (IEEE TIT 2021); Yu's $\Phi$-stability (PTRF 2023).
• 2025–2026 — Chen, Gohari and Nair's differential (entropy-production) approach; independent preprints announcing proofs by Chen, Gohari, Javanmard, Lin, Mirrokni, Nair and Woodruff (arXiv:2609.24931), Ky and Tran (arXiv:2609.24184), Mahdavifar and Beirami (arXiv:2609.26444), and a bias-retaining finite-noise bound by Kramer and Saglam.
• September 2026 — The OpenAI preprint (Theorems 1.1 and 1.3, Corollary 1.2, pp. 1–4).

Setting

Let $\Omega_n=\{-1,1\}^n$ with uniform measure; information is in nats unless stated. For $r\in[-1,1]$ put

$$L=\log2,\quad H(r)=-\tfrac{1+r}2\log\tfrac{1+r}2-\tfrac{1-r}2\log\tfrac{1-r}2,\quad \psi(r)=L-H(r),$$

with $0\log0=0$; $\psi^{-1}$ is the increasing branch $[0,L]\to[0,1]$. A soft channel is $u:\Omega_n\to[-1,1]$, the conditional mean of an auxiliary sign $U$ given $X$; its information is $I(u)=H(\mathbb Eu)-\mathbb EH(u)=I(U;X)$. For $\rho\in[-1,1]$ let $Y_i=X_iZ_i$ with independent signs $\mathbb EZ_i=\rho$, and let $T_\rho u(y)=\mathbb E[u(X)\mid Y=y]$, so $I(T_\rho u)=I(U;Y)$. For an interior field $g:\Omega_n\to(-1,1)$ with $m=\mathbb Eg$, the production is $D(g)=\mathbb E[\operatorname{atanh}(g)\,Ng]$ with $Ng=\frac12\sum_i(g-g\circ\mathrm{flip}_i)$; the rate $F$ is defined by $F(\psi(r))=r\operatorname{atanh}r$; $S(I)=F(I)-2I$ (zero for $I<0$); $B_m(I)=2I+(1-m^2)S\bigl(L-\frac{H(m)-I}{1-m^2}\bigr)$.

Formalization targets

Milestone: Courtade–Kumar inequality in bits (Corollary 1.2, p. 2)

For $n\ge1$, $0\le\varepsilon\le\frac12$ and every Boolean $f$ on $\{0,1\}^n$,

$$I_2(f(X);Y)\le 1-h_2(\varepsilon),$$

with equality for every coordinate $x\mapsto x_i$ and its complement.

Goal: the soft contraction package (Theorem 1.1, p. 1; Corollary 1.2, p. 2; Theorem 1.3, p. 4)

The goal OAI.SoftChannel204.fullMain is the conjunction of:

1. Theorem 1.1. For all $n$, $u:\Omega_n\to[-1,1]$, $\rho\in[-1,1]$:

$$I(T_\rho u)\le\psi\bigl(|\rho|\,\psi^{-1}(I(u))\bigr),$$

with equality for every soft coordinate $u(x)=a x_i$, $|a|\le1$; and $I(U;Y)=I(T_\rho u)$ for the joint law of $(U,Y)$. 2. Corollary 1.2. For Boolean $f$ with $m=\mathbb Ef$ and $r_m=\psi^{-1}(H(m))$: $I(f(X);Y)\le\psi(|\rho|r_m)\le\psi(|\rho|)$, strictly below $\psi(|\rho|)$ when $0<|m|<1$ and $0<|\rho|$; coordinates and their negations attain $\psi(|\rho|)$; and the bits conversion $\psi(1-2\varepsilon)/L=1-h_2(\varepsilon)$. 3. Theorem 1.3. For every interior $g$: $D(g)\ge\max\{B_m(I(g)),F(I(g))\}\ge F(I(g))$.

Significance

The result itself. It settles the Courtade–Kumar conjecture and strengthens it in two directions: to randomized summaries at fixed initial information, and to a bias-dependent bound that is strictly better for nonconstant biased outputs. Theorem 1.3 is a mean-dependent entropy-production inequality, stronger than the scalar rate needed for Theorem 1.1. Several independent proofs of the Boolean conjecture were announced in the same period; the preprint compares its production profile with that of Chen et al. in Section 8.

Formalizing it. All objects are finite sums over $\{-1,1\}^n$, so the statements are elementary to state in Lean. The proof requires an explicit three-point optimizer for a joining problem, convexity facts about $F$ and $S$ (Lemmas 2.2–2.4, pp. 5–6), dimension induction and integration along the noise semigroup. A formal proof would give a checked solution of a conjecture with several competing announced proofs, some computer-assisted.

Difficulty

The local-to-global method of Chen, Gohari and Nair needs a local inequality to pass from the two halves of the cube to the whole. The natural information-only profile $\Phi_m(I)=F(I)$ fails the corresponding local comparison for some coupled pair laws, so the induction must carry the mean $m$ as well. The preprint uses the maximum of two profiles, $B_m$ and $F$; it must solve the minimization of the joining cost exactly (Section 3), pay the interior pair with a variance-refined one-bit inequality (Lemma 4.1, p. 12), and control the common-output corners by a thinning argument (Theorem 6.1, p. 17). The linear bound $D(g)\ge2I(g)$ from the log-Sobolev inequality does not suffice; the nonlinear surplus above $2I$ is where the difficulty lies.

Formalization scope

• Cube n = Fin n → Bool, averages are finite sums divided by $2^n$, logs are natural; sign maps Bool to $\pm1$.
• psiInv is Function.invFunOn psi (Icc 0 1); since $\psi$ is strictly increasing on $[0,1]$ and $I(u)\in[0,L]$, this is the paper's branch.
• noise ρ u y = ∑ x, kernel ρ y x * u x with kernel the product of $(1\pm\rho)/2$, which is $T_\rho$. Mutual information is the finite sum over the joint table, with terms omitted where the joint probability is $0$.
• F is stated as psiInv s * artanh (psiInv s) and is only used on $[0,L)$; for interior $g$, $|m|<1$ and $0\le I(g)<H(m)\le L$, so reserve and hybrid are evaluated in their source domain.
• All results hold for every $n\ge0$; the attainment statements quantify over i : Fin n. The milestone (separate definition file) uses the crossover form with bits.

Selected references

• OpenAI, Sharp binary-information contraction on the discrete cube, OpenAI Math Release preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Sharp-binary-information-contraction-on-the-discrete-cube-September-24-2026/main.pdf
• T. A. Courtade, G. R. Kumar, Which Boolean functions maximize mutual information on noisy inputs?, IEEE Trans. Inf. Theory 60 (2014). https://doi.org/10.1109/TIT.2014.2326877
• G. R. Kumar, T. A. Courtade, Which Boolean functions are most informative?, ISIT 2013. https://doi.org/10.1109/ISIT.2013.6620221
• A. Samorodnitsky, On the entropy of a noisy function, IEEE Trans. Inf. Theory (2016). https://doi.org/10.1109/TIT.2016.2584625
• O. Ordentlich, O. Shayevitz, O. Weinstein, An improved upper bound for the most informative Boolean function conjecture, ISIT 2016. https://doi.org/10.1109/ISIT.2016.7541349
• G. Pichler, P. Piantanida, G. Matz, Dictator functions maximize mutual information, Ann. Appl. Probab. (2018). https://doi.org/10.1214/18-AAP1384
• L. Yu, On the $\Phi$-stability and related conjectures, Probab. Theory Relat. Fields (2023). https://doi.org/10.1007/s00440-023-01209-5
• A. Gohari, C. Nair, Outer bounds for multiuser settings: the auxiliary receiver approach, IEEE Trans. Inf. Theory (2022). https://doi.org/10.1109/TIT.2021.3128136
• Z. Chen, A. Gohari, A. Javanmard, et al., A proof of the most informative Boolean function conjecture, arXiv:2609.24931 (2026). https://arxiv.org/abs/2609.24931
• V. K. Ky, T. Tran, Dictators are most informative, arXiv:2609.24184 (2026). https://arxiv.org/abs/2609.24184
• H. Mahdavifar, A. Beirami, The most informative bit and beyond, arXiv:2609.26444 (2026). https://arxiv.org/abs/2609.26444
• S. G. Bobkov, P. Tetali, Modified logarithmic Sobolev inequalities in discrete settings, J. Theoret. Probab. (2006). https://doi.org/10.1007/s10959-006-0016-3

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